# HG changeset patch
# User haftmann
# Date 1283260902 -7200
# Node ID d9ac9dee764d12e276008453f7df161a4dccf4bd
# Parent  0e6f54c9d201aca7788e7c2b42bed7970065475b
distinguish code production and code presentation

diff -r 0e6f54c9d201 -r d9ac9dee764d doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Tue Aug 31 15:08:04 2010 +0200
+++ b/doc-src/more_antiquote.ML	Tue Aug 31 15:21:42 2010 +0200
@@ -127,10 +127,9 @@
   (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
   (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
     let val thy = ProofContext.theory_of ctxt in
-      Code_Target.produce_code thy (mk_cs thy)
+      Code_Target.present_code thy (mk_cs thy)
         (fn naming => maps (fn f => f thy naming) mk_stmtss)
         target NONE (SOME "Example") []
-      |> fst
       |> typewriter
     end);
 
diff -r 0e6f54c9d201 -r d9ac9dee764d src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Tue Aug 31 15:08:04 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Tue Aug 31 15:21:42 2010 +0200
@@ -30,7 +30,7 @@
     val struct_name = if struct_name_hint = "" then eval_struct_name
       else struct_name_hint;
     val (ml_code, target_names) = Code_Target.produce_code_for thy
-      target NONE (SOME struct_name) [] naming program (consts' @ tycos', []);
+      target NONE (SOME struct_name) [] naming program (consts' @ tycos');
     val (consts'', tycos'') = chop (length consts') target_names;
     val consts_map = map2 (fn const => fn NONE =>
         error ("Constant " ^ (quote o Code.string_of_const thy) const
@@ -58,7 +58,7 @@
               Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
           |> fold (curry Graph.add_edge value_name) deps;
         val (value_code, [SOME value_name']) = Code_Target.produce_code_for thy
-          (the_default target some_target) NONE (SOME "") [] naming program ([value_name], []);
+          (the_default target some_target) NONE (SOME "") [] naming program [value_name];
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ Long_Name.base_name value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
       in ML_Context.evaluate ctxt false reff sml_code end;
diff -r 0e6f54c9d201 -r d9ac9dee764d src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Aug 31 15:08:04 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Tue Aug 31 15:21:42 2010 +0200
@@ -12,14 +12,18 @@
   val export_code_for: theory -> Path.T option -> string -> int option -> string option -> Token.T list
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
   val produce_code_for: theory -> string -> int option -> string option -> Token.T list
-    -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string * string option list
+    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
+  val present_code_for: theory -> string -> int option -> string option -> Token.T list
+    -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
   val check_code_for: theory -> string -> bool -> Token.T list
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
 
   val export_code: theory -> string list
     -> (((string * string option) * Path.T option) * Token.T list) list -> unit
-  val produce_code: theory -> string list -> (Code_Thingol.naming -> string list)
+  val produce_code: theory -> string list
     -> string -> int option -> string option -> Token.T list -> string * string option list
+  val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
+    -> string -> int option -> string option -> Token.T list -> string
   val check_code: theory -> string list
     -> ((string * bool) * Token.T list) list -> unit
 
@@ -65,17 +69,19 @@
 
 (** abstract nonsense **)
 
-datatype destination = File of Path.T option | String of string list;
+datatype destination = Export of Path.T option | Produce | Present of string list;
 type serialization = int -> destination -> (string * string option list) option;
 
-fun stmt_names_of_destination (String stmt_names) = stmt_names
+fun stmt_names_of_destination (Present stmt_names) = stmt_names
   | stmt_names_of_destination _ = [];
 
-fun serialization output _ content width (File some_path) = (output width some_path content; NONE)
-  | serialization _ string content width (String _) = SOME (string width content);
+fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
+  | serialization _ string content width Produce = SOME (string width content)
+  | serialization _ string content width (Present _) = SOME (string width content);
 
-fun file some_path f = (f (File some_path); ());
-fun string stmt_names f = the (f (String stmt_names));
+fun export some_path f = (f (Export some_path); ());
+fun produce f = the (f Produce);
+fun present stmt_names f = fst (the (f (Present stmt_names)));
 
 
 (** theory data **)
@@ -353,10 +359,13 @@
 in
 
 fun export_code_for thy some_path target some_width some_module_name args naming program names =
-  file some_path (mount_serializer thy target some_width some_module_name args naming program names);
+  export some_path (mount_serializer thy target some_width some_module_name args naming program names);
 
-fun produce_code_for thy target some_width some_module_name args naming program (names, selects) =
-  string selects (mount_serializer thy target some_width some_module_name args naming program names);
+fun produce_code_for thy target some_width some_module_name args naming program names =
+  produce (mount_serializer thy target some_width some_module_name args naming program names);
+
+fun present_code_for thy target some_width some_module_name args naming program (names, selects) =
+  present selects (mount_serializer thy target some_width some_module_name args naming program names);
 
 fun check_code_for thy target strict args naming program names_cs =
   let
@@ -367,7 +376,7 @@
     fun ext_check env_param p =
       let 
         val destination = make_destination p;
-        val _ = file (SOME destination) (mount_serializer thy target (SOME 80)
+        val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
           (SOME module_name) args naming program names_cs);
         val cmd = make_command env_param module_name;
       in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
@@ -415,10 +424,15 @@
 fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
   ((map o apfst o apsnd) prep_destination seris);
 
-fun produce_code thy cs names_stmt target some_width some_module_name args =
+fun produce_code thy cs target some_width some_module_name args =
   let
     val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
-  in produce_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
+  in produce_code_for thy target some_width some_module_name args naming program names_cs end;
+
+fun present_code thy cs names_stmt target some_width some_module_name args =
+  let
+    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
+  in present_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
 
 fun check_code thy cs seris =
   let