# HG changeset patch
# User haftmann
# Date 1251815945 -7200
# Node ID 236fa33784de6dd44f4c9151394e143a6906a382
# Parent  711d1a43d7542d019d65a2b5ce6ce3f24e3a7715
code generator is now a separate component

diff -r 711d1a43d754 -r 236fa33784de etc/components
--- a/etc/components	Tue Sep 01 16:00:59 2009 +0200
+++ b/etc/components	Tue Sep 01 16:39:05 2009 +0200
@@ -11,6 +11,7 @@
 src/LCF
 src/Sequents
 #misc components
+src/Tools/Code
 src/HOL/Tools/ATP_Manager
 src/HOL/Tools/Mirabelle
 src/HOL/Library/Sum_Of_Squares
diff -r 711d1a43d754 -r 236fa33784de lib/Tools/codegen
--- a/lib/Tools/codegen	Tue Sep 01 16:00:59 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Florian Haftmann, TUM
-#
-# DESCRIPTION: issue code generation from shell
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG IMAGE THY CMD"
-  echo
-  echo "  Issues code generation using image IMAGE,"
-  echo "  theory THY,"
-  echo "  with Isar command 'export_code CMD'"
-  echo
-  exit 1
-}
-
-
-## process command line
-
-[ "$#" -lt 2 -o "$1" = "-?" ] && usage
-
-IMAGE="$1"; shift
-THY="$1"; shift
-CMD="$1"
-
-
-## main
-
-CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
-CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
-FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
-
-"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1
diff -r 711d1a43d754 -r 236fa33784de src/Tools/Code/etc/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/etc/settings	Tue Sep 01 16:39:05 2009 +0200
@@ -0,0 +1,2 @@
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
diff -r 711d1a43d754 -r 236fa33784de src/Tools/Code/lib/Tools/codegen
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/lib/Tools/codegen	Tue Sep 01 16:39:05 2009 +0200
@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+#
+# Author: Florian Haftmann, TUM
+#
+# DESCRIPTION: issue code generation from shell
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG IMAGE THY CMD"
+  echo
+  echo "  Issues code generation using image IMAGE,"
+  echo "  theory THY,"
+  echo "  with Isar command 'export_code CMD'"
+  echo
+  exit 1
+}
+
+
+## process command line
+
+[ "$#" -lt 2 -o "$1" = "-?" ] && usage
+
+IMAGE="$1"; shift
+THY="$1"; shift
+CMD="$1"
+
+
+## main
+
+CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
+CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
+
+"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1