author | wenzelm |
Mon, 08 May 2000 20:58:49 +0200 | |
changeset 8839 | 31da5b9790c0 |
parent 6082 | 590f9e3bf4d8 |
child 9788 | df671fa2562a |
permissions | -rwxr-xr-x |
5213
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
1 |
#!/bin/bash |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
2 |
# |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
3 |
# $Id$ |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
4 |
# |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
5 |
# DESCRIPTION: adapt theories and proof scripts to new datatype package |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
6 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
7 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
8 |
## diagnostics |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
9 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
10 |
PRG=$(basename $0) |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
11 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
12 |
function usage() |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
13 |
{ |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
14 |
echo |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
15 |
echo "Usage: $PRG [FILES|DIRS...]" |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
16 |
echo |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
17 |
echo " Recursively find .thy/.ML files, adapting them to" |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
18 |
echo " the new datatype package" |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
19 |
echo |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
20 |
echo " Renames old versions of FILES by appending \"~~\"." |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
21 |
echo |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
22 |
exit 1 |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
23 |
} |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
24 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
25 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
26 |
## process command line |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
27 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
28 |
[ $# -eq 0 -o "$1" = "-?" ] && usage |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
29 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
30 |
SPECS="$@"; shift $# |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
31 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
32 |
|
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
33 |
## main |
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
34 |
|
6082 | 35 |
#set by configure |
36 |
AUTO_PERL=perl |
|
37 |
||
5213
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset
|
38 |
find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \ |
6082 | 39 |
xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixdatatype.pl |