1.1 --- a/etc/components	Tue Sep 01 16:00:59 2009 +0200
     1.2 +++ b/etc/components	Tue Sep 01 16:39:05 2009 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  src/LCF
     1.5  src/Sequents
     1.6  #misc components
     1.7 +src/Tools/Code
     1.8  src/HOL/Tools/ATP_Manager
     1.9  src/HOL/Tools/Mirabelle
    1.10  src/HOL/Library/Sum_Of_Squares

     2.1 --- a/lib/Tools/codegen	Tue Sep 01 16:00:59 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,40 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# Author: Florian Haftmann, TUM
     2.7 -#
     2.8 -# DESCRIPTION: issue code generation from shell
     2.9 -
    2.10 -
    2.11 -## diagnostics
    2.12 -
    2.13 -PRG="$(basename "$0")"
    2.14 -
    2.15 -function usage()
    2.16 -{
    2.17 -  echo
    2.18 -  echo "Usage: isabelle $PRG IMAGE THY CMD"
    2.19 -  echo
    2.20 -  echo "  Issues code generation using image IMAGE,"
    2.21 -  echo "  theory THY,"
    2.22 -  echo "  with Isar command 'export_code CMD'"
    2.23 -  echo
    2.24 -  exit 1
    2.25 -}
    2.26 -
    2.27 -
    2.28 -## process command line
    2.29 -
    2.30 -[ "$#" -lt 2 -o "$1" = "-?" ] && usage
    2.31 -
    2.32 -IMAGE="$1"; shift
    2.33 -THY="$1"; shift
    2.34 -CMD="$1"
    2.35 -
    2.36 -
    2.37 -## main
    2.38 -
    2.39 -CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
    2.40 -CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
    2.41 -FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
    2.42 -
    2.43 -"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/Code/etc/settings	Tue Sep 01 16:39:05 2009 +0200
     3.3 @@ -0,0 +1,2 @@
     3.4 +
     3.5 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/Code/lib/Tools/codegen	Tue Sep 01 16:39:05 2009 +0200
     4.3 @@ -0,0 +1,40 @@
     4.4 +#!/usr/bin/env bash
     4.5 +#
     4.6 +# Author: Florian Haftmann, TUM
     4.7 +#
     4.8 +# DESCRIPTION: issue code generation from shell
     4.9 +
    4.10 +
    4.11 +## diagnostics
    4.12 +
    4.13 +PRG="$(basename "$0")"
    4.14 +
    4.15 +function usage()
    4.16 +{
    4.17 +  echo
    4.18 +  echo "Usage: isabelle $PRG IMAGE THY CMD"
    4.19 +  echo
    4.20 +  echo "  Issues code generation using image IMAGE,"
    4.21 +  echo "  theory THY,"
    4.22 +  echo "  with Isar command 'export_code CMD'"
    4.23 +  echo
    4.24 +  exit 1
    4.25 +}
    4.26 +
    4.27 +
    4.28 +## process command line
    4.29 +
    4.30 +[ "$#" -lt 2 -o "$1" = "-?" ] && usage
    4.31 +
    4.32 +IMAGE="$1"; shift
    4.33 +THY="$1"; shift
    4.34 +CMD="$1"
    4.35 +
    4.36 +
    4.37 +## main
    4.38 +
    4.39 +CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
    4.40 +CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
    4.41 +FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
    4.42 +
    4.43 +"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1