tuned;
authorwenzelm
Fri Oct 10 14:51:58 1997 +0200 (1997-10-10)
changeset 38260caedb36900d
parent 3825 478461d77e88
child 3827 c13504a27d8e
tuned;
lib/Tools/fixdots
lib/scripts/fixdots.pl
     1.1 --- a/lib/Tools/fixdots	Thu Oct 09 18:01:27 1997 +0200
     1.2 +++ b/lib/Tools/fixdots	Fri Oct 10 14:51:58 1997 +0200
     1.3 @@ -17,6 +17,8 @@
     1.4    echo "  Recursively find .thy/.ML files, patching them to ensure that"
     1.5    echo "  dots in formulas are followed by non-idents."
     1.6    echo
     1.7 +  echo "  Renames old versions of FILES by appending \"~~\"."
     1.8 +  echo
     1.9    exit 1
    1.10  }
    1.11  
     2.1 --- a/lib/scripts/fixdots.pl	Thu Oct 09 18:01:27 1997 +0200
     2.2 +++ b/lib/scripts/fixdots.pl	Fri Oct 10 14:51:58 1997 +0200
     2.3 @@ -3,40 +3,52 @@
     2.4  #
     2.5  # fixdots.pl - ensure that dots in formulas are followed by non-idents
     2.6  #
     2.7 +# tries to be smart; may produce garbage if nested comments and
     2.8 +# solitary quotes (") are intermixed badly;
     2.9 +#
    2.10 +
    2.11 +sub fixdots {
    2.12 +    my ($file) = @_;
    2.13 +
    2.14 +    open (FILE, $file) || die $!;
    2.15 +    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
    2.16 +    close FILE || die $!;
    2.17 +
    2.18 +
    2.19 +    $result = "";
    2.20 +    $rest = $text;
    2.21 +
    2.22 +    while (1) {
    2.23 +	$_ = $rest;
    2.24 +	($pre, $str, $rest) =
    2.25 +	    m/^((?: \(\*.*?\*\) | [^"] )*)     # pre: text or (non-nested!) comments
    2.26 +            "((?: [^"\\] | \\\S | \\\s+\\ )*)"  # quoted string
    2.27 +            (.*)$/sx;                          # rest of file
    2.28 +	if ($str) {
    2.29 +	    $_ = $str;
    2.30 +	    if (!m/^[a-zA-Z0-9_\/\.]*$/s && !m/\.ML/s && !m/\.thy/s) {   # exclude filenames!
    2.31 +		s/([a-zA-Z][a-zA-Z0-9_']*)\.([a-zA-Z])/$1\. $2/sg;
    2.32 +	    }
    2.33 +            $result = $result . $pre . '"' . $_ . '"';
    2.34 +        } else {
    2.35 + 	    $result = $result . $_;
    2.36 +    	    last;
    2.37 +	}
    2.38 +    }
    2.39 +
    2.40 +    if ($text ne $result) {
    2.41 +	print STDERR "fixing $file\n";
    2.42 +	rename $file, "$file~~" || die $!;
    2.43 +	open (FILE, "> $file") || die $!;
    2.44 +	print FILE $result;
    2.45 +	close FILE || die $!;
    2.46 +    }
    2.47 +}
    2.48 +
    2.49 +
    2.50 +## main
    2.51  
    2.52  foreach $file (@ARGV) {
    2.53 -
    2.54 -    if (open (FILE, $file)) {
    2.55 -	undef $/;
    2.56 -	$text = <FILE>;
    2.57 -	close FILE;
    2.58 -
    2.59 -	$result = "";
    2.60 -	$rest = $text;
    2.61 -
    2.62 -	while (1) {
    2.63 -	    $_ = $rest;
    2.64 -	    ($pre, $str, $rest) = m/^([^"]*)"((?:[^"\\]|\\.)*)"(.*)$/s;
    2.65 -	    if ($str) {
    2.66 -		$_ = $str;
    2.67 -		if (!m/^[a-zA-Z0-9_\/\.]*$/s && !m/\.ML$/s && !m/\.thy/) {     # Exclude filenames!
    2.68 -		    s/([a-zA-Z][a-zA-Z0-9_']*)\.([a-zA-Z])/$1\. $2/g;
    2.69 -	        }
    2.70 -                $result = $result . $pre . '"' . $_ . '"';
    2.71 -            } else {
    2.72 - 	        $result = $result . $_;
    2.73 -    	        last;
    2.74 -	    }
    2.75 -        }
    2.76 -
    2.77 -        if ($text ne $result) {
    2.78 -	    print STDERR "fixing $file\n";
    2.79 -	    open (FILE, "> $file") || die $!;
    2.80 -	    print FILE $result;
    2.81 -	    close FILE || die $!;
    2.82 -        }
    2.83 -
    2.84 -    } else {
    2.85 -        print STDERR "Can't open file $file: $!\n";
    2.86 -    }
    2.87 +  eval { &fixdots($file); };
    2.88 +  if ($@) { print STDERR "*** fixdots $file: ", $@, "\n"; }
    2.89  }