equal
deleted
inserted
replaced
12 function usage() |
12 function usage() |
13 { |
13 { |
14 echo |
14 echo |
15 echo "Usage: isabelle $PRG [FILES|DIRS...]" |
15 echo "Usage: isabelle $PRG [FILES|DIRS...]" |
16 echo |
16 echo |
17 echo " Recursively find .thy/.ML files, removing unreadable symbol names." |
17 echo " Recursively find .thy/.ML files and remove symbols that are unreadably" |
|
18 echo " in plain text (e.g. \<Longrightarrow>)." |
|
19 echo |
18 echo " Note: this is an ad-hoc script; there is no systematic way to replace" |
20 echo " Note: this is an ad-hoc script; there is no systematic way to replace" |
19 echo " symbols independently of the inner syntax of a theory!" |
21 echo " symbols independently of the inner syntax of a theory!" |
20 echo |
22 echo |
21 echo " Renames old versions of FILES by appending \"~~\"." |
23 echo " Old versions of files are preserved by appending \"~~\"." |
22 echo |
24 echo |
23 exit 1 |
25 exit 1 |
24 } |
26 } |
25 |
27 |
26 |
28 |
31 SPECS="$@"; shift "$#" |
33 SPECS="$@"; shift "$#" |
32 |
34 |
33 |
35 |
34 ## main |
36 ## main |
35 |
37 |
36 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \ |
38 find $SPECS \( -name \*.ML -o -name \*.thy \) -print0 | \ |
37 xargs "$ISABELLE_HOME/lib/scripts/unsymbolize" |
39 xargs -0 "$ISABELLE_HOME/lib/scripts/unsymbolize" |