lib/Tools/fixgreek
changeset 14171 0cab06e3bbd0
child 14981 e73f8140af78
equal deleted inserted replaced
14170:edd5a2ea3807 14171:0cab06e3bbd0
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # $Id$
       
     4 # Author: Sebastian Skalberg, TU Muenchen
       
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
       
     6 #
       
     7 # DESCRIPTION: fix problems with greek and other foreign letters
       
     8 
       
     9 
       
    10 ## diagnostics
       
    11 
       
    12 PRG="$(basename "$0")"
       
    13 
       
    14 function usage()
       
    15 {
       
    16   echo
       
    17   echo "Usage: $PRG [FILES|DIRS...]"
       
    18   echo
       
    19   echo "  Recursively find .thy files, fixing parse problems stemming"
       
    20   echo "  from the classification change of greek and other foreign"
       
    21   echo "  letters from symbols to letters."
       
    22   echo
       
    23   echo "  Renames old versions of FILES by appending \"~~\"."
       
    24   echo
       
    25   exit 1
       
    26 }
       
    27 
       
    28 
       
    29 ## process command line
       
    30 
       
    31 [ "$#" -eq 0 -o "$1" = "-?" ] && usage
       
    32 
       
    33 SPECS="$@"; shift "$#"
       
    34 
       
    35 
       
    36 ## main
       
    37 
       
    38 #set by configure
       
    39 AUTO_PERL=perl
       
    40 
       
    41 find $SPECS -name \*.thy -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
       
    42 find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"