tuned;

--- a/lib/Tools/fixdots	Thu Oct 09 18:01:27 1997 +0200
+++ b/lib/Tools/fixdots	Fri Oct 10 14:51:58 1997 +0200
@@ -17,6 +17,8 @@
   echo "  Recursively find .thy/.ML files, patching them to ensure that"
   echo "  dots in formulas are followed by non-idents."
   echo
+  echo "  Renames old versions of FILES by appending \"~~\"."
+  echo
   exit 1
 }
 

--- a/lib/scripts/fixdots.pl	Thu Oct 09 18:01:27 1997 +0200
+++ b/lib/scripts/fixdots.pl	Fri Oct 10 14:51:58 1997 +0200
@@ -3,40 +3,52 @@
 #
 # fixdots.pl - ensure that dots in formulas are followed by non-idents
 #
+# tries to be smart; may produce garbage if nested comments and
+# solitary quotes (") are intermixed badly;
+#
+
+sub fixdots {
+    my ($file) = @_;
+
+    open (FILE, $file) || die $!;
+    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
+    close FILE || die $!;
+
+
+    $result = "";
+    $rest = $text;
+
+    while (1) {
+	$_ = $rest;
+	($pre, $str, $rest) =
+	    m/^((?: \(\*.*?\*\) | [^"] )*)     # pre: text or (non-nested!) comments
+            "((?: [^"\\] | \\\S | \\\s+\\ )*)"  # quoted string
+            (.*)$/sx;                          # rest of file
+	if ($str) {
+	    $_ = $str;
+	    if (!m/^[a-zA-Z0-9_\/\.]*$/s && !m/\.ML/s && !m/\.thy/s) {   # exclude filenames!
+		s/([a-zA-Z][a-zA-Z0-9_']*)\.([a-zA-Z])/$1\. $2/sg;
+	    }
+            $result = $result . $pre . '"' . $_ . '"';
+        } else {
+ 	    $result = $result . $_;
+    	    last;
+	}
+    }
+
+    if ($text ne $result) {
+	print STDERR "fixing $file\n";
+	rename $file, "$file~~" || die $!;
+	open (FILE, "> $file") || die $!;
+	print FILE $result;
+	close FILE || die $!;
+    }
+}
+
+
+## main
 
 foreach $file (@ARGV) {
-
-    if (open (FILE, $file)) {
-	undef $/;
-	$text = <FILE>;
-	close FILE;
-
-	$result = "";
-	$rest = $text;
-
-	while (1) {
-	    $_ = $rest;
-	    ($pre, $str, $rest) = m/^([^"]*)"((?:[^"\\]|\\.)*)"(.*)$/s;
-	    if ($str) {
-		$_ = $str;
-		if (!m/^[a-zA-Z0-9_\/\.]*$/s && !m/\.ML$/s && !m/\.thy/) {     # Exclude filenames!
-		    s/([a-zA-Z][a-zA-Z0-9_']*)\.([a-zA-Z])/$1\. $2/g;
-	        }
-                $result = $result . $pre . '"' . $_ . '"';
-            } else {
- 	        $result = $result . $_;
-    	        last;
-	    }
-        }
-
-        if ($text ne $result) {
-	    print STDERR "fixing $file\n";
-	    open (FILE, "> $file") || die $!;
-	    print FILE $result;
-	    close FILE || die $!;
-        }
-
-    } else {
-        print STDERR "Can't open file $file: $!\n";
-    }
+  eval { &fixdots($file); };
+  if ($@) { print STDERR "*** fixdots $file: ", $@, "\n"; }
 }