# HG changeset patch
# User oheimb
# Date 991068508 -7200
# Node ID ad8061b2da6ce363872ffafbdc84e2bc6fcf7586
# Parent  956ec01b46e09134c7ff1996ec22f697a0b98f58
improved handling of space before/after parentheses

diff -r 956ec01b46e0 -r ad8061b2da6c lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Tue May 22 15:15:16 2001 +0200
+++ b/lib/scripts/convert.pl	Mon May 28 18:48:28 2001 +0200
@@ -58,7 +58,8 @@
   s/\( /\(/g; s/ \)/\)/g; # remove leading and trailing space inside parentheses
   s/\[ /\[/g; s/ \]/\]/g; # remove leading and trailing space inside sq brackets
   s/ ?\( ?\)/\(\)/g;      # remove space before and inside empty tuples
-  s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples
+  s/([^ ])\(/$1 \(/g;     # possibly add space before opening parentheses
+  s/\)([^ ])/\) $1/g;     # possibly add space after  closing parentheses
 
   s/EVERY *\[(.*?)\]/$1/;
   if(s/EVERY\' ?\[(.*?)\] *(\d+)/$1 $2/) {
@@ -92,10 +93,10 @@
   s/^Force_tac (\d+)/{$prefer="prefer $1 "; "force"}/e;
   s/Clarsimp_tac 1/clarsimp/g;
 
-  s/auto_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\)/auto $1 $2/g;
-  s/force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) 1/force $1 $2/g;
-  s/^force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) (\d+)/{$prefer="prefer $3 "; "force $1 $2"}/e;
-  s/clarsimp_tac \(claset\(*\) (.*?), *simpset\(\) (.*?)\) 1/clarsimp $1 $2/g;
+  s/auto_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\)/auto $1 $2/g;
+  s/force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) 1/force $1 $2/g;
+  s/^force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) (\d+)/{$prefer="prefer $3 "; "force $1 $2"}/e;
+  s/clarsimp_tac \(claset \(*\) (.*?), *simpset \(\) (.*?)\) 1/clarsimp $1 $2/g;
 
   s/Asm_full_simp_tac 1/simp/g;
   s/Full_simp_tac 1/simp (no_asm_use)/g;
@@ -106,14 +107,14 @@
   s/ALLGOALS Asm_simp_tac/simp_all (no_asm_simp)/g;
   s/ALLGOALS Simp_tac/simp_all (no_asm)/g;
 
-  s/asm_full_simp_tac \(simpset\(\) (.*?)\) 1/simp $1/g;
-  s/full_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_use) $1/g;
-  s/asm_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_simp) $1/g;
-  s/simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm) $1/g;
-  s/ALLGOALS \(asm_full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all $1/g;
-  s/ALLGOALS \(full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_use) $1/g;
-  s/ALLGOALS \(asm_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_simp) $1/g;
-  s/ALLGOALS \(simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm) $1/g;
+  s/asm_full_simp_tac \(simpset \(\) (.*?)\) 1/simp $1/g;
+  s/full_simp_tac \(simpset \(\) (.*?)\) 1/simp (no_asm_use) $1/g;
+  s/asm_simp_tac \(simpset \(\) (.*?)\) 1/simp (no_asm_simp) $1/g;
+  s/simp_tac \(simpset \(\) (.*?)\) 1/simp (no_asm) $1/g;
+  s/ALLGOALS \(asm_full_simp_tac \(simpset \(\) (.*?)\) \)/simp_all $1/g;
+  s/ALLGOALS \(full_simp_tac \(simpset \(\) (.*?)\) \)/simp_all (no_asm_use) $1/g;
+  s/ALLGOALS \(asm_simp_tac \(simpset \(\) (.*?)\) \)/simp_all (no_asm_simp) $1/g;
+  s/ALLGOALS \(simp_tac \(simpset \(\) (.*?)\) \)/simp_all (no_asm) $1/g;
 
   s/a(ssume_)?tac 1/assumption/g;
   s/^a(ssume_)?tac (\d+)/{$prefer="prefer $2 "; "assumption"}/e;
@@ -139,7 +140,7 @@
   s/ORELSE/|/g;
   subst_RS();
 
-  s/\(\"(.*?)\" *, *(\".*?\")\) *, */$1 = $2 and /g; # instantiations
+  s/\(\"(.*?)\" *, *(\".*?\")\) , */$1 = $2 and /g; # instantiations
   s/\(\"(.*?)\" *, *(\".*?\")\)/$1 = $2/g;       # last instantiation
 
   s/rewtac ([\w\'\. \[,\]]+)/unfold $1/g;