# HG changeset patch
# User haftmann
# Date 1285658077 -7200
# Node ID c0099428ca7b919322562bb2ddc1583f6b14351a
# Parent  a727e1dab1627a3621e596a3dc0020142ff17227
consider quick_and_dirty option before loading theory

diff -r a727e1dab162 -r c0099428ca7b src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Sep 28 08:35:00 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Tue Sep 28 09:14:37 2010 +0200
@@ -55,7 +55,7 @@
   val add_reserved: string -> string -> theory -> theory
   val add_include: string -> string * (string * string list) option -> theory -> theory
 
-  val codegen_tool: string (*theory name*) -> bool -> string (*export_code expr*) -> unit
+  val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
 end;
 
 structure Code_Target : CODE_TARGET =
@@ -692,10 +692,9 @@
 
 (** external entrance point -- for codegen tool **)
 
-fun codegen_tool thyname qnd cmd_expr =
+fun codegen_tool thyname cmd_expr =
   let
     val thy = Thy_Info.get_theory thyname;
-    val _ = quick_and_dirty := qnd;
     val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
       (filter Token.is_proper o Outer_Syntax.scan Position.none);
   in case parse cmd_expr
diff -r a727e1dab162 -r c0099428ca7b src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Tue Sep 28 08:35:00 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Tue Sep 28 09:14:37 2010 +0200
@@ -55,9 +55,9 @@
   handle _ => OS.Process.exit OS.Process.failure;"
 
 ACTUAL_CMD="val thyname = \"$THYNAME\"; \
-  val qnd = $QUICK_AND_DIRTY; \
+  val _ = quick_and_dirty := $QUICK_AND_DIRTY; \
   val cmd_expr = \"$CODE_EXPR\"; \
-  val ml_cmd = \"Code_Target.codegen_tool thyname qnd cmd_expr\"; \
+  val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
   $FORMAL_CMD"
 
 "$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1