equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # Author: Florian Haftmann, TUM |
4 # Author: Florian Haftmann, TUM |
5 # |
5 # |
6 # DESCRIPTION: migrates theory header (of new-style theories) to non-deprecated syntax |
6 # DESCRIPTION: turn Isar theory headers into imports-uses-begin format |
7 |
7 |
8 |
8 |
9 ## diagnostics |
9 ## diagnostics |
10 |
10 |
11 PRG="$(basename "$0")" |
11 PRG="$(basename "$0")" |
13 function usage() |
13 function usage() |
14 { |
14 { |
15 echo |
15 echo |
16 echo "Usage: $PRG [FILES|DIRS...]" |
16 echo "Usage: $PRG [FILES|DIRS...]" |
17 echo |
17 echo |
18 echo " Recursively find .thy files, patching them to ensure that" |
18 echo " Recursively find .thy files, turning Isar theory headers into" |
19 echo " theory headers (of new-style theories) are in non-deprecated format." |
19 echo " imports-uses-begin format." |
20 echo |
20 echo |
21 echo " Renames old versions of FILES by appending \"~~\"." |
21 echo " Renames old versions of FILES by appending \"~~\"." |
22 echo |
22 echo |
23 exit 1 |
23 exit 1 |
24 } |
24 } |
34 ## main |
34 ## main |
35 |
35 |
36 #set by configure |
36 #set by configure |
37 AUTO_PERL=perl |
37 AUTO_PERL=perl |
38 |
38 |
39 find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \ |
39 find $SPECS -name \*.thy -print | \ |
40 xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixheaders.pl" |
40 xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixheaders.pl" |