# HG changeset patch
# User wenzelm
# Date 1373632099 -7200
# Node ID 42e02ddd1568daed5ce1f2461b7587cda899450b
# Parent  3ac2878764f9adc681826f90e6ceeed202778dc8
allow spaces in file names;
tuned;

diff -r 3ac2878764f9 -r 42e02ddd1568 lib/Tools/unsymbolize
--- 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"
diff -r 3ac2878764f9 -r 42e02ddd1568 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 $!;
         }