# HG changeset patch
# User oheimb
# Date 988625725 -7200
# Node ID 165405d911f162c9207aa8366bf5601f93f1af75
# Parent  b2a1d9c20df7e11fff9db4ea8cd8ddf8e500af62
minor bugfix for newlines with Goalw

diff -r b2a1d9c20df7 -r 165405d911f1 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;