--- a/lib/Tools/unsymbolize Wed Jul 10 16:25:26 2013 +0200
+++ b/lib/Tools/unsymbolize Fri Jul 12 14:28:19 2013 +0200
@@ -14,11 +14,13 @@
echo
echo "Usage: isabelle $PRG [FILES|DIRS...]"
echo
- echo " Recursively find .thy/.ML files, removing unreadable symbol names."
+ echo " Recursively find .thy/.ML files and remove symbols that are unreadably"
+ echo " in plain text (e.g. \<Longrightarrow>)."
+ echo
echo " Note: this is an ad-hoc script; there is no systematic way to replace"
echo " symbols independently of the inner syntax of a theory!"
echo
- echo " Renames old versions of FILES by appending \"~~\"."
+ echo " Old versions of files are preserved by appending \"~~\"."
echo
exit 1
}
@@ -33,5 +35,5 @@
## main
-find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
- xargs "$ISABELLE_HOME/lib/scripts/unsymbolize"
+find $SPECS \( -name \*.ML -o -name \*.thy \) -print0 | \
+ xargs -0 "$ISABELLE_HOME/lib/scripts/unsymbolize"
--- a/lib/scripts/unsymbolize Wed Jul 10 16:25:26 2013 +0200
+++ b/lib/scripts/unsymbolize Fri Jul 12 14:28:19 2013 +0200
@@ -2,8 +2,7 @@
#
# Author: Markus Wenzel, TU Muenchen
#
-# unsymbolize.pl - remove unreadable symbol names from sources
-#
+# unsymbolize - remove unreadable symbol names from sources
use warnings;
use strict;
@@ -46,7 +45,7 @@
my $result = $_;
if ($text ne $result) {
- print STDERR "fixing $file\n";
+ print STDERR "changing $file\n";
if (! -f "$file~~") {
rename $file, "$file~~" || die $!;
}