src/Tools/Code/code_target.ML

   val cert_tyco: theory -> string -> string
   val read_tyco: theory -> string -> string
 
   type serializer
   type literals = Code_Printer.literals
-  val add_target: string * { serializer: serializer, literals: literals, check: unit }
-    -> theory -> theory
+  val add_target: string * { serializer: serializer, literals: literals,
+    check: { env_var: string, make_destination: Path.T -> Path.T,
+      make_command: string -> Path.T -> string -> string } } -> theory -> theory
   val extend_target: string *
       (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
     -> theory -> theory
   val assert_target: theory -> string -> string
 

   val export: serialization -> unit
   val file: Path.T -> serialization -> unit
   val string: string list -> serialization -> string
   val code_of: theory -> string -> int option -> string
     -> string list -> (Code_Thingol.naming -> string list) -> string
-  val external_check: theory -> string -> string
-    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> unit
+  val check: theory -> string -> unit
   val set_default_code_width: int -> theory -> theory
   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
 
   val allow_abort: string -> theory -> theory
   type tyco_syntax = Code_Printer.tyco_syntax

   -> ((Pretty.T -> string) * (Pretty.T -> unit))
   -> Code_Thingol.program
   -> string list                        (*selected statements*)
   -> serialization;
 
-datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, check: unit }
+datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
+      check: { env_var: string, make_destination: Path.T -> Path.T,
+        make_command: string -> Path.T -> string -> string } }
   | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
 
 datatype target = Target of {
   serial: serial,
   description: description,

 
 (** serializer usage **)
 
 (* montage *)
 
-fun the_literals thy =
+fun the_fundamental thy =
   let
     val ((targets, _), _) = Targets.get thy;
-    fun literals target = case Symtab.lookup targets target
+    fun fundamental target = case Symtab.lookup targets target
      of SOME data => (case the_description data
-         of Fundamental { literals, ... } => literals
-          | Extension (super, _) => literals super)
+         of Fundamental data => data
+          | Extension (super, _) => fundamental super)
       | NONE => error ("Unknown code target language: " ^ quote target);
-  in literals end;
+  in fundamental end;
+
+fun the_literals thy = #literals o the_fundamental thy;
 
 local
 
 fun activate_syntax lookup_name src_tab = Symtab.empty
   |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier

     val names3 = transitivly_non_empty_funs thy naming program;
     val cs3 = map_filter (fn (c, name) =>
       if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
   in union (op =) cs3 cs1 end;
 
-fun external_check thy target env_var make_destination make_command =
-  let
+fun check thy target =
+  let
+    val { env_var, make_destination, make_command } =
+      (#check o the_fundamental thy) target;
     val env_param = getenv env_var;
     fun ext_check env_param p =
       let 
         val module_name = "Code_Test";
         val (cs, (naming, program)) =

   in if env_param = ""
     then warning (env_var ^ " not set; skipped code check for " ^ target)
     else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
   end;
 
+
 fun export_code thy cs seris =
   let
     val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
     fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
       else file (Path.explode dest);