| author | wenzelm | 
| Tue, 20 Apr 2010 17:07:53 +0200 | |
| changeset 36238 | 344377ce2e0a | 
| parent 35022 | c844b93dd147 | 
| child 52617 | 42e02ddd1568 | 
| permissions | -rwxr-xr-x | 
| 10555 | 1  | 
#!/usr/bin/env bash  | 
| 10026 | 2  | 
#  | 
3  | 
# Author: Markus Wenzel, TU Muenchen  | 
|
4  | 
#  | 
|
5  | 
# DESCRIPTION: remove unreadable symbol names from sources  | 
|
6  | 
||
7  | 
||
8  | 
## diagnostics  | 
|
9  | 
||
| 10511 | 10  | 
PRG="$(basename "$0")"  | 
| 10026 | 11  | 
|
12  | 
function usage()  | 
|
13  | 
{
 | 
|
14  | 
echo  | 
|
| 28650 | 15  | 
echo "Usage: isabelle $PRG [FILES|DIRS...]"  | 
| 10026 | 16  | 
echo  | 
17  | 
echo " Recursively find .thy/.ML files, removing unreadable symbol names."  | 
|
18  | 
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!"  | 
|
20  | 
echo  | 
|
21  | 
echo " Renames old versions of FILES by appending \"~~\"."  | 
|
22  | 
echo  | 
|
23  | 
exit 1  | 
|
24  | 
}  | 
|
25  | 
||
26  | 
||
27  | 
## process command line  | 
|
28  | 
||
29  | 
[ "$#" -eq 0 -o "$1" = "-?" ] && usage  | 
|
30  | 
||
31  | 
SPECS="$@"; shift "$#"  | 
|
32  | 
||
33  | 
||
34  | 
## main  | 
|
35  | 
||
36  | 
find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \  | 
|
| 
35022
 
c844b93dd147
modernized perl scripts: prefer standalone executables;
 
wenzelm 
parents: 
29143 
diff
changeset
 | 
37  | 
xargs "$ISABELLE_HOME/lib/scripts/unsymbolize"  |