author  skalberg 
Fri, 04 Mar 2005 15:07:34 +0100  
changeset 15574  b1d1b5bfc464 
parent 14981  e73f8140af78 
child 15847  c05c7670f166 
permissions  rwxrxrx 
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

1 
#!/usr/bin/env bash 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

2 
# 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

3 
# $Id$ 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

4 
# Author: Sebastian Skalberg, TU Muenchen 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

5 
# 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

6 
# DESCRIPTION: fix problems with greek and other foreign letters 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

7 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

8 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

9 
## diagnostics 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

10 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

11 
PRG="$(basename "$0")" 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

12 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

13 
function usage() 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

14 
{ 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

15 
echo 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

16 
echo "Usage: $PRG [FILESDIRS...]" 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

17 
echo 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

18 
echo " Recursively find .thy files, fixing parse problems stemming" 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

19 
echo " from the classification change of greek and other foreign" 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

20 
echo " letters from symbols to letters." 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

21 
echo 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

22 
echo " Renames old versions of FILES by appending \"~~\"." 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

23 
echo 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

24 
exit 1 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

25 
} 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

26 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

27 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

28 
## process command line 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

29 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

30 
[ "$#" eq 0 o "$1" = "?" ] && usage 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

31 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

32 
SPECS="$@"; shift "$#" 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

33 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

34 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

35 
## main 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

36 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

37 
#set by configure 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
14981
diff
changeset

38 
AUTO_PERL=/usr/bin/perl 
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

39 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

40 
find $SPECS name \*.thy print  xargs "$AUTO_PERL" w "$ISABELLE_HOME/lib/scripts/fixgreek.pl" 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

41 
find $SPECS name \*.ML print  xargs "$AUTO_PERL" w "$ISABELLE_HOME/lib/scripts/fixgreek.pl" 