1.1 --- a/lib/Tools/codegen	Tue Sep 01 16:00:59 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,40 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Author: Florian Haftmann, TUM
     1.7 -#
     1.8 -# DESCRIPTION: issue code generation from shell
     1.9 -
    1.10 -
    1.11 -## diagnostics
    1.12 -
    1.13 -PRG="$(basename "$0")"
    1.14 -
    1.15 -function usage()
    1.16 -{
    1.17 -  echo
    1.18 -  echo "Usage: isabelle $PRG IMAGE THY CMD"
    1.19 -  echo
    1.20 -  echo "  Issues code generation using image IMAGE,"
    1.21 -  echo "  theory THY,"
    1.22 -  echo "  with Isar command 'export_code CMD'"
    1.23 -  echo
    1.24 -  exit 1
    1.25 -}
    1.26 -
    1.27 -
    1.28 -## process command line
    1.29 -
    1.30 -[ "$#" -lt 2 -o "$1" = "-?" ] && usage
    1.31 -
    1.32 -IMAGE="$1"; shift
    1.33 -THY="$1"; shift
    1.34 -CMD="$1"
    1.35 -
    1.36 -
    1.37 -## main
    1.38 -
    1.39 -CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
    1.40 -CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
    1.41 -FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
    1.42 -
    1.43 -"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1