author  wenzelm 
Tue, 13 Jun 2006 23:41:39 +0200  
changeset 19876  11d447d5d68c 
parent 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 
15847
c05c7670f166
restored AUTO_BASH/PERL  beware of ./configure!
wenzelm
parents:
15574
diff
changeset

38 
AUTO_PERL=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" 