lib/Tools/fixdatatype
author berghofe
Thu Jul 30 15:49:18 1998 +0200 (1998-07-30)
changeset 5213 0aa62210e67c
child 6082 590f9e3bf4d8
permissions -rwxr-xr-x
Script that adapts theories and proof scripts to new datatype package.
berghofe@5213
     1
#!/bin/bash
berghofe@5213
     2
#
berghofe@5213
     3
# $Id$
berghofe@5213
     4
#
berghofe@5213
     5
# DESCRIPTION: adapt theories and proof scripts to new datatype package
berghofe@5213
     6
berghofe@5213
     7
berghofe@5213
     8
## diagnostics
berghofe@5213
     9
berghofe@5213
    10
PRG=$(basename $0)
berghofe@5213
    11
berghofe@5213
    12
function usage()
berghofe@5213
    13
{
berghofe@5213
    14
  echo
berghofe@5213
    15
  echo "Usage: $PRG [FILES|DIRS...]"
berghofe@5213
    16
  echo
berghofe@5213
    17
  echo "  Recursively find .thy/.ML files, adapting them to"
berghofe@5213
    18
  echo "  the new datatype package"
berghofe@5213
    19
  echo
berghofe@5213
    20
  echo "  Renames old versions of FILES by appending \"~~\"."
berghofe@5213
    21
  echo
berghofe@5213
    22
  exit 1
berghofe@5213
    23
}
berghofe@5213
    24
berghofe@5213
    25
berghofe@5213
    26
## process command line
berghofe@5213
    27
berghofe@5213
    28
[ $# -eq 0 -o "$1" = "-?" ] && usage
berghofe@5213
    29
berghofe@5213
    30
SPECS="$@"; shift $#
berghofe@5213
    31
berghofe@5213
    32
berghofe@5213
    33
## main
berghofe@5213
    34
berghofe@5213
    35
find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
berghofe@5213
    36
  xargs perl -w $ISABELLE_HOME/lib/scripts/fixdatatype.pl