1.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 16:33:06 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Aug 30 16:42:54 2010 +0200
     1.3 @@ -25,18 +25,18 @@
     1.4    val serialization: (int -> Path.T option -> 'a -> unit)
     1.5      -> (int -> 'a -> string * string option list)
     1.6      -> 'a -> int -> serialization
     1.7 +
     1.8    val serialize: theory -> string -> int option -> string option -> Token.T list
     1.9      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    1.10    val serialize_custom: theory -> string * serializer -> string option
    1.11 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list
    1.12 -    -> string * string option list
    1.13 -  val the_literals: theory -> string -> literals
    1.14 -  val file: Path.T option -> serialization -> unit
    1.15 -  val string: string list -> serialization -> string
    1.16 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    1.17 +  val check: theory -> string list
    1.18 +    -> Code_Thingol.naming -> Code_Thingol.program -> string -> bool -> Token.T list -> unit
    1.19    val code_of: theory -> string -> int option -> string
    1.20 -    -> string list -> (Code_Thingol.naming -> string list) -> string
    1.21 +    -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
    1.22    val set_default_code_width: int -> theory -> theory
    1.23    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    1.24 +  val the_literals: theory -> string -> literals
    1.25  
    1.26    val allow_abort: string -> theory -> theory
    1.27    type tyco_syntax = Code_Printer.tyco_syntax
    1.28 @@ -64,15 +64,15 @@
    1.29  datatype destination = File of Path.T option | String of string list;
    1.30  type serialization = destination -> (string * string option list) option;
    1.31  
    1.32 -fun file some_path f = (f (File some_path); ());
    1.33 -fun string stmt_names f = fst (the (f (String stmt_names)));
    1.34 -
    1.35  fun stmt_names_of_destination (String stmt_names) = stmt_names
    1.36    | stmt_names_of_destination _ = [];
    1.37  
    1.38  fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
    1.39    | serialization _ string pretty width (String _) = SOME (string width pretty);
    1.40  
    1.41 +fun file some_path f = f (File some_path);
    1.42 +fun string stmt_names f = the (f (String stmt_names));
    1.43 +
    1.44  
    1.45  (** theory data **)
    1.46