minor bugfix for newlines with Goalw
authoroheimb
Mon, 30 Apr 2001 12:15:25 +0200
changeset 11272 165405d911f1
parent 11271 b2a1d9c20df7
child 11273 673783831234
minor bugfix for newlines with Goalw
lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Mon Apr 30 11:57:10 2001 +0200
+++ b/lib/scripts/convert.pl	Mon Apr 30 12:15:25 2001 +0200
@@ -60,7 +60,7 @@
   s/ ?\( ?\)/\(\)/g;      # remove space before and inside empty tuples
   s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples
 
-  if(s/^\(EVERY\'\[(.*?)\]\s*(\d+)\)$/\($1 $2\)/) {
+  if(s/^\(EVERY\'\[(.*?)\] *(\d+)\)$/\($1 $2\)/) {
     $goal = $2;
     s/,/ $goal,/g;
   }
@@ -252,6 +252,7 @@
     goto nlc;
   }
   $_=$line;
+  if(!($head =~ m/^\n/)) { $head = "\n$head"; }
   s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\. \[,\]]+) *(.+)/
     "lemma ".lemmaname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
   s/^Goal *(.+)/"lemma ".lemmaname().": $1"/se;