collapse category "schematic goal" in keyword table -- Proof General does not know about this;
authorwenzelm
Fri, 23 Apr 2010 22:39:49 +0200
changeset 36316 f9b45eac4c60
parent 36315 e859879079c8
child 36317 506d732cb522
collapse category "schematic goal" in keyword table -- Proof General does not know about this;
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);
     }
   }