Add ruleset rewriter tests

GraphSubst tests are insufficient, as we need to test all the renaming
malarky in the matching process as well.
Remove redundant normalisation calls
Properly remove edges in target graph

When substituting into a graph, we need to make sure all edges in the
match are removed; previously, we assumed that edges would be removed
when the vertices were.  This does not work when there was a bare wire
in the pattern graph, though.
Add (commented out) tests that fail for issue #108
Matching: when extending wires, avoid vertex names in the pattern

We can't touch the names of boundary vertices in the rule when we merge
in the RHS.  We get around this by renaming the target away from the
rule boundary before matching.  However, matching can introduce new
vertices when there are bare wires in the pattern.  Previously, it was
possible for these new vertices to have the same names as one of the
rule boundary vertices.  This commit prevents that.

fixes #108
Show which vertices were *actually* (un-)banged in GUI

The core does not allow you to construct a graph with non-open !-boxes.
If you try to (when either adding vertices to or removing vertices from
a !-box), it will extend the !-boxes as far as necessary to make them
open again.

This means that if you have a bare wire, for example, and bang one end,
the other end will be banged as well.  If you then try to unbang just
one end, nothing will happen.

The information about exactly which vertices were (un-)banged is now
returned in the protocol, and this is used by the GUI.  Note that in the
case of unbanging, we actually just refresh the graph.

Closes #82
Do not open more than one copy of a rule in the GUI

Closes #100
Check !-box nesting structure when creating rules

Rule.mk now fails if the two graphs do not have the same !-box-parent
relation.

Closes #83
Rule context menu improvements

Add enable/disable rules entries, and hide entries that only operate on
a single rule when multiple rules are selected.

Closes #104
Complain if dot is not found

Closes #12
Only do as much renaming is strictly necessary in rename_apart

Closes #98
Try to deal with duplicate names in arguments gracefully
Fix highlight and rewrite weirdness

The underlying cause of much of the strange behaviour (including
highlighting not working properly, and strange things during rewrites)
seems to be down to bad parsing of attached rewrites: the new graph was
never parsed out properly.

Of course, fixing this exposed a slew of other bugs.  Things *mostly*
seem to behave sensibly now.  It is possible that this will fix
issue #109, but I can't reliably reproduce it any more, so I'm not
certain of that.
Fix position update on paste

Fixes #107
Remove dotfile directory

It does not appear to have any purpose.
Try to make graph_iso.ML and bang_graph_iso.ML as similar as possible

These have almost-duplicated code; it's useful to be able to see if
there is a fix that hasn't been propagated.
Test that found matches are valid
Comment out forget_all() in make_bin.ML

Maybe this will give us better stack traces?
Tidy up RULE signature

BASIC_RULE is dead, RULE now refers to string graphs, and
BANG_GRAPH_RULE is introduced for !-graphs.  Similarly, there is now a
BANG_GRAPH_RULESET.
Introduce a Rewriter structure, to replace GraphSubst

This incorporates the low-level rule-only code from RulesetRewriter.