# HG changeset patch
# User haftmann
# Date 1423137672 -3600
# Node ID 61d6d5cbbcd3b820205eee4b2b4f684ea564a3bb
# Parent  b36379a730f48fa9b766e486bd0417e3206ad3cd
dropped obsolete external entrance point

diff -r b36379a730f4 -r 61d6d5cbbcd3 NEWS
--- a/NEWS	Thu Feb 05 13:01:12 2015 +0100
+++ b/NEWS	Thu Feb 05 13:01:12 2015 +0100
@@ -68,6 +68,11 @@
 
 *** HOL ***
 
+* Discontinued old-fashioned "codegen" tool.  Code generation can always
+be externally triggered using an appropriate ROOT file plus a corresponding
+theory.  Parametrization is possible using environment variables, or
+ML snippets in the most extreme cases.  Minor INCOMPATIBILITY.
+
 * Add NO_MATCH-simproc, allows to check for syntactic non-equality
 
 * Generalized and consolidated some theorems concerning divsibility:
diff -r b36379a730f4 -r 61d6d5cbbcd3 etc/components
--- a/etc/components	Thu Feb 05 13:01:12 2015 +0100
+++ b/etc/components	Thu Feb 05 13:01:12 2015 +0100
@@ -1,5 +1,4 @@
 #hard-wired components
-src/Tools/Code
 src/Tools/jEdit
 src/Tools/Graphview
 src/HOL/Mirabelle
diff -r b36379a730f4 -r 61d6d5cbbcd3 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Feb 05 13:01:12 2015 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Feb 05 13:01:12 2015 +0100
@@ -53,8 +53,6 @@
   val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
     -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
-
-  val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
 end;
 
 structure Code_Target : CODE_TARGET =
@@ -661,18 +659,4 @@
   Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
     (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
 
-
-(** external entrance point -- for codegen tool **)
-
-fun codegen_tool thyname cmd_expr =
-  let
-    val thy = Thy_Info.get_theory thyname;
-    val ctxt = Proof_Context.init_global thy;
-    val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
-      (filter Token.is_proper o Token.explode (Thy_Header.get_keywords thy) Position.none);
-  in case parse cmd_expr
-   of SOME f => (writeln "Now generating code..."; f ctxt)
-    | NONE => error ("Bad directive " ^ quote cmd_expr)
-  end;
-
 end; (*struct*)
diff -r b36379a730f4 -r 61d6d5cbbcd3 src/Tools/Code/etc/settings
--- a/src/Tools/Code/etc/settings	Thu Feb 05 13:01:12 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-
diff -r b36379a730f4 -r 61d6d5cbbcd3 src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Thu Feb 05 13:01:12 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Florian Haftmann, TUM
-#
-# DESCRIPTION: issue code generation from shell
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD"
-  echo
-  echo "  Options are:"
-  echo "    -q    run in quick_and_dirty mode"
-  echo
-  echo "  Issues code generation using image IMAGE,"
-  echo "  theory THYNAME,"
-  echo "  with Isar command 'export_code CMD'"
-  echo
-  exit 1
-}
-
-
-## process command line
-
-QUICK_AND_DIRTY="false"
-
-while getopts "q" OPT
-do
-  case "$OPT" in
-    q)
-      QUICK_AND_DIRTY="true"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-[ "$#" -ne 3 ] && usage
-
-IMAGE="$1"; shift
-THYNAME="$1"; shift
-CODE_EXPR=$(echo "$1" | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
-
-
-## invoke code generation
-
-FORMAL_CMD="Runtime.toplevel_program (fn () => (use_thy thyname; ML_Context.eval_source_in \
-    (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) \
-    ML_Compiler.flags \
-    {delimited=true, text=ml_cmd, pos=Position.none})) \
-  handle _ => exit 1;"
-
-ACTUAL_CMD="val thyname = \"$THYNAME\"; \
-  val cmd_expr = \"$CODE_EXPR\"; \
-  val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
-  $FORMAL_CMD"
-
-"$ISABELLE_PROCESS" -r -q -o "quick_and_dirty=$QUICK_AND_DIRTY" -e "$ACTUAL_CMD" "$IMAGE" || exit 1