# HG changeset patch # User wenzelm # Date 1272055189 -7200 # Node ID f9b45eac4c60108dcbd6a17cbf3ab3e71298eae9 # Parent e859879079c817af50d9c122cfc1f6c1bf0dac62 collapse category "schematic goal" in keyword table -- Proof General does not know about this; diff -r e859879079c8 -r f9b45eac4c60 lib/scripts/keywords --- a/lib/scripts/keywords Fri Apr 23 21:00:28 2010 +0200 +++ b/lib/scripts/keywords Fri Apr 23 22:39:49 2010 +0200 @@ -39,6 +39,7 @@ elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) { my $name = $1; my $kind = $2; + if ($kind eq "theory-schematic-goal") { $kind = "theory-goal"; } &set_keyword($name, $kind); } }