author  skalberg 
Thu, 28 Aug 2003 01:56:40 +0200  
changeset 14171  0cab06e3bbd0 
child 14981  e73f8140af78 
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 
# License: GPL (GNU GENERAL PUBLIC LICENSE) 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
diff
changeset

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

7 
# 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

8 

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

9 

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

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

11 

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

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

13 

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

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

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

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

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

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

19 
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

20 
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

21 
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

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

23 
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

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

25 
exit 1 
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 

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

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

30 

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

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

32 

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

33 
SPECS="$@"; shift "$#" 
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 

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

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

37 

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

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

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

40 

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

41 
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

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