# HG changeset patch # User haftmann # Date 1285658253 -7200 # Node ID 7ead9d0f2e84414fe4251fd7e85fb27dd9bbba95 # Parent fa94799e3a3b90790aa1fd42e4b52186e17270b3# Parent c0099428ca7b919322562bb2ddc1583f6b14351a merged diff -r fa94799e3a3b -r 7ead9d0f2e84 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Sep 28 08:38:20 2010 +0200 +++ b/src/Tools/Code/code_target.ML Tue Sep 28 09:17:33 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 fa94799e3a3b -r 7ead9d0f2e84 src/Tools/Code/lib/Tools/codegen --- a/src/Tools/Code/lib/Tools/codegen Tue Sep 28 08:38:20 2010 +0200 +++ b/src/Tools/Code/lib/Tools/codegen Tue Sep 28 09:17:33 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