lib/Tools/convert
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 11001 6754fa0f2af7
child 15574 b1d1b5bfc464
permissions -rwxr-xr-x
Merged in license change from Isabelle2004
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     2
#
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     3
# $Id$
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     4
# Author: David von Oheimb, TU Muenchen
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     5
#
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     6
# DESCRIPTION: convert legacy tactic scripts to Isabelle/Isar tactic emulation
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     7
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     8
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     9
## diagnostics
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    10
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    11
PRG="$(basename "$0")"
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    12
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    13
function usage()
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    14
{
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    15
  echo
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    16
  echo "Usage: $PRG [FILES|DIRS...]"
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    17
  echo
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    18
  echo "  Recursively find .ML files, converting legacy tactic scripts to"
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    19
  echo "  Isabelle/Isar tactic emulation."
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    20
  echo "  Note: conversion is only approximated, based on some heuristics."
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    21
  echo
11001
6754fa0f2af7 corrected file name suffixes
oheimb
parents: 10939
diff changeset
    22
  echo "  Renames old versions of FILES by appending \"~0~\"."
6754fa0f2af7 corrected file name suffixes
oheimb
parents: 10939
diff changeset
    23
  echo "  Creates new versions of FILES by appending \".thy\"."
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    24
  echo
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    25
  exit 1
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    26
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    27
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    28
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    29
## process command line
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    30
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    31
[ "$#" -eq 0 -o "$1" = "-?" ] && usage
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    32
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    33
SPECS="$@"; shift "$#"
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    34
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    35
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    36
## main
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    37
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    38
#set by configure
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    39
AUTO_PERL=perl
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    40
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    41
find $SPECS \( -name \*.ML \) -print | \
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    42
  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl"