author | wenzelm |
Sun, 05 Jun 2005 21:32:37 +0200 | |
changeset 16285 | 75954ae8b247 |
parent 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
3824
9fdde15e3215
ensure that dots in formulas are followed by non-idents;
wenzelm
parents:
diff
changeset
|
1 |
# |
9fdde15e3215
ensure that dots in formulas are followed by non-idents;
wenzelm
parents:
diff
changeset
|
2 |
# $Id$ |
9789 | 3 |
# Author: Markus Wenzel, TU Muenchen |
3824
9fdde15e3215
ensure that dots in formulas are followed by non-idents;
wenzelm
parents:
diff
changeset
|
4 |
# |
9fdde15e3215
ensure that dots in formulas are followed by non-idents;
wenzelm
parents:
diff
changeset
|
5 |
# fixdots.pl - ensure that dots in formulas are followed by non-idents |
9fdde15e3215
ensure that dots in formulas are followed by non-idents;
wenzelm
parents:
diff
changeset
|
6 |
# |
3826 | 7 |
# tries to be smart; may produce garbage if nested comments and |
8 |
# solitary quotes (") are intermixed badly; |
|
9 |
# |
|
10 |
||
11 |
sub fixdots { |
|
12 |
my ($file) = @_; |
|
13 |
||
14 |
open (FILE, $file) || die $!; |
|
15 |
undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file |
|
16 |
close FILE || die $!; |
|
17 |
||
18 |
||
19 |
$result = ""; |
|
20 |
$rest = $text; |
|
21 |
||
22 |
while (1) { |
|
23 |
$_ = $rest; |
|
24 |
($pre, $str, $rest) = |
|
3838 | 25 |
m/^((?: \(\*.*?\*\) | [^"] )*) # pre: text or (non-nested!) comments |
3826 | 26 |
"((?: [^"\\] | \\\S | \\\s+\\ )*)" # quoted string |
3838 | 27 |
(.*)$/sx; # rest of file |
3826 | 28 |
if ($str) { |
29 |
$_ = $str; |
|
30 |
if (!m/^[a-zA-Z0-9_\/\.]*$/s && !m/\.ML/s && !m/\.thy/s) { # exclude filenames! |
|
31 |
s/([a-zA-Z][a-zA-Z0-9_']*)\.([a-zA-Z])/$1\. $2/sg; |
|
32 |
} |
|
33 |
$result = $result . $pre . '"' . $_ . '"'; |
|
34 |
} else { |
|
35 |
$result = $result . $_; |
|
36 |
last; |
|
37 |
} |
|
38 |
} |
|
39 |
||
40 |
if ($text ne $result) { |
|
41 |
print STDERR "fixing $file\n"; |
|
4076 | 42 |
if (! -f "$file~~") { |
43 |
rename $file, "$file~~" || die $!; |
|
44 |
} |
|
3826 | 45 |
open (FILE, "> $file") || die $!; |
46 |
print FILE $result; |
|
47 |
close FILE || die $!; |
|
48 |
} |
|
49 |
} |
|
50 |
||
51 |
||
52 |
## main |
|
3824
9fdde15e3215
ensure that dots in formulas are followed by non-idents;
wenzelm
parents:
diff
changeset
|
53 |
|
9fdde15e3215
ensure that dots in formulas are followed by non-idents;
wenzelm
parents:
diff
changeset
|
54 |
foreach $file (@ARGV) { |
3826 | 55 |
eval { &fixdots($file); }; |
56 |
if ($@) { print STDERR "*** fixdots $file: ", $@, "\n"; } |
|
3824
9fdde15e3215
ensure that dots in formulas are followed by non-idents;
wenzelm
parents:
diff
changeset
|
57 |
} |