lib/Tools/codegen
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 30494 c150e6fa4e0d
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Florian Haftmann, TUM
     4 #
     5 # DESCRIPTION: issue code generation from shell
     6 
     7 
     8 ## diagnostics
     9 
    10 PRG="$(basename "$0")"
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: isabelle $PRG IMAGE THY CMD"
    16   echo
    17   echo "  Issues code generation using image IMAGE,"
    18   echo "  theory THY,"
    19   echo "  with Isar command 'export_code CMD'"
    20   echo
    21   exit 1
    22 }
    23 
    24 
    25 ## process command line
    26 
    27 [ "$#" -lt 2 -o "$1" = "-?" ] && usage
    28 
    29 IMAGE="$1"; shift
    30 THY="$1"; shift
    31 CMD="$1"
    32 
    33 
    34 ## main
    35 
    36 CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
    37 CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
    38 FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
    39 
    40 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1