src/Tools/Code/code_target.ML
changeset 38784 3b4d63ab03c4
parent 38779 89f654951200
child 38863 9070a7c356c9
equal deleted inserted replaced
38782:3865cbe5d2be 38784:3b4d63ab03c4
    26   val mk_serialization: string -> (Path.T option -> 'a -> unit)
    26   val mk_serialization: string -> (Path.T option -> 'a -> unit)
    27     -> ('a -> string * string option list)
    27     -> ('a -> string * string option list)
    28     -> 'a -> serialization
    28     -> 'a -> serialization
    29   val serialize: theory -> string -> int option -> string option -> Token.T list
    29   val serialize: theory -> string -> int option -> string option -> Token.T list
    30     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    30     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    31   val serialize_custom: theory -> string * serializer
    31   val serialize_custom: theory -> string * serializer -> string option
    32     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    32     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    33   val the_literals: theory -> string -> literals
    33   val the_literals: theory -> string -> literals
    34   val export: serialization -> unit
    34   val export: serialization -> unit
    35   val file: Path.T -> serialization -> unit
    35   val file: Path.T -> serialization -> unit
    36   val string: string list -> serialization -> string
    36   val string: string list -> serialization -> string
   346       then error (env_var ^ " not set; cannot check code for " ^ target)
   346       then error (env_var ^ " not set; cannot check code for " ^ target)
   347       else warning (env_var ^ " not set; skipped checking code for " ^ target)
   347       else warning (env_var ^ " not set; skipped checking code for " ^ target)
   348     else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
   348     else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
   349   end;
   349   end;
   350 
   350 
   351 fun serialize_custom thy (target_name, seri) naming program names =
   351 fun serialize_custom thy (target_name, seri) module_name naming program names =
   352   mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
   352   mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
   353   |> the;
   353   |> the;
   354 
   354 
   355 end; (* local *)
   355 end; (* local *)
   356 
   356 
   357 
   357