src/Tools/Code/code_target.ML

 
 signature CODE_TARGET =
 sig
   val cert_tyco: Proof.context -> string -> string
   val read_tyco: Proof.context -> string -> string
-
-  datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
-  val next_export: theory -> string * theory
 
   val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string
     -> int option -> Token.T list  -> Code_Thingol.program -> bool -> Code_Symbol.T list
     -> local_theory -> local_theory
   val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list

     -> (string list * Bytes.T) list * string
   val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
     -> ((string list * Bytes.T) list * string) * (Code_Symbol.T -> string option)
 
+  datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
   type serializer
-  type literals = Code_Printer.literals
   type language
   type ancestry
   val assert_target: theory -> string -> string
   val add_language: string * language -> theory -> theory
   val add_derived_target: string * ancestry -> theory -> theory
-  val the_literals: Proof.context -> string -> literals
+  val the_literals: Proof.context -> string -> Code_Printer.literals
+
   val parse_args: 'a parser -> Token.T list -> 'a
   val default_code_width: int Config.T
+  val next_export: theory -> string * theory
 
   type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
   val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
     -> theory -> theory
   val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, string * Code_Symbol.T list) symbol_attr_decl

 struct
 
 open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 
-type literals = Code_Printer.literals;
 type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl =
   (string * (string * 'a option) list, string * (string * 'b option) list,
     class * (string * 'c option) list, (class * class) * (string * 'd option) list,
     (class * string) * (string * 'e option) list,
     string * (string * 'f option) list) Code_Symbol.attr;

     module_name: string }
   -> Code_Thingol.program
   -> Code_Symbol.T list
   -> pretty_modules * (Code_Symbol.T -> string option);
 
-type language = {serializer: serializer, literals: literals,
+type language = {serializer: serializer, literals: Code_Printer.literals,
   check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string},
   evaluation_args: Token.T list};
 
 type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list;