# HG changeset patch
# User haftmann
# Date 1283179374 -7200
# Node ID c7da3cc8813502eb30d897309a34549d887c2f46
# Parent  c0b857a0475856f3b7a0ba5ff1a1067fcecf6957
tuned

diff -r c0b857a04758 -r c7da3cc88135 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Mon Aug 30 16:33:06 2010 +0200
+++ b/doc-src/more_antiquote.ML	Mon Aug 30 16:42:54 2010 +0200
@@ -130,6 +130,7 @@
       Code_Target.code_of thy
         target NONE "Example" (mk_cs thy)
         (fn naming => maps (fn f => f thy naming) mk_stmtss)
+      |> fst
       |> typewriter
     end);
 
diff -r c0b857a04758 -r c7da3cc88135 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Aug 30 16:33:06 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Mon Aug 30 16:42:54 2010 +0200
@@ -25,18 +25,18 @@
   val serialization: (int -> Path.T option -> 'a -> unit)
     -> (int -> 'a -> string * string option list)
     -> 'a -> int -> serialization
+
   val serialize: theory -> string -> int option -> string option -> Token.T list
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
   val serialize_custom: theory -> string * serializer -> string option
-    -> Code_Thingol.naming -> Code_Thingol.program -> string list
-    -> string * string option list
-  val the_literals: theory -> string -> literals
-  val file: Path.T option -> serialization -> unit
-  val string: string list -> serialization -> string
+    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
+  val check: theory -> string list
+    -> Code_Thingol.naming -> Code_Thingol.program -> string -> bool -> Token.T list -> unit
   val code_of: theory -> string -> int option -> string
-    -> string list -> (Code_Thingol.naming -> string list) -> string
+    -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
   val set_default_code_width: int -> theory -> theory
   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
+  val the_literals: theory -> string -> literals
 
   val allow_abort: string -> theory -> theory
   type tyco_syntax = Code_Printer.tyco_syntax
@@ -64,15 +64,15 @@
 datatype destination = File of Path.T option | String of string list;
 type serialization = destination -> (string * string option list) option;
 
-fun file some_path f = (f (File some_path); ());
-fun string stmt_names f = fst (the (f (String stmt_names)));
-
 fun stmt_names_of_destination (String stmt_names) = stmt_names
   | stmt_names_of_destination _ = [];
 
 fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
   | serialization _ string pretty width (String _) = SOME (string width pretty);
 
+fun file some_path f = f (File some_path);
+fun string stmt_names f = the (f (String stmt_names));
+
 
 (** theory data **)