lib/Tools/unsymbolize
author wenzelm
Thu Nov 30 20:10:29 2000 +0100 (2000-11-30)
changeset 10555 2323ec838401
parent 10511 efb3428c9879
child 14981 e73f8140af78
permissions -rwxr-xr-x
/usr/bin/env bash;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: remove unreadable symbol names from sources
     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/.ML files, removing unreadable symbol names."
    20   echo "  Note: this is an ad-hoc script; there is no systematic way to replace"
    21   echo "  symbols independently of the inner syntax of a theory!"
    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 \*.ML -o -name \*.thy \) -print | \
    42   xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/unsymbolize.pl"