src/Tools/Code/code_target.ML
changeset 38863 9070a7c356c9
parent 38784 3b4d63ab03c4
child 38908 732149f6ebf9
equal deleted inserted replaced
38862:2795499a20bd 38863:9070a7c356c9
    11 
    11 
    12   type serializer
    12   type serializer
    13   type literals = Code_Printer.literals
    13   type literals = Code_Printer.literals
    14   val add_target: string * { serializer: serializer, literals: literals,
    14   val add_target: string * { serializer: serializer, literals: literals,
    15     check: { env_var: string, make_destination: Path.T -> Path.T,
    15     check: { env_var: string, make_destination: Path.T -> Path.T,
    16       make_command: string -> Path.T -> string -> string } } -> theory -> theory
    16       make_command: string -> string -> string } } -> theory -> theory
    17   val extend_target: string *
    17   val extend_target: string *
    18       (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    18       (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    19     -> theory -> theory
    19     -> theory -> theory
    20   val assert_target: theory -> string -> string
    20   val assert_target: theory -> string -> string
    21 
    21 
   114   -> (string list * string list)        (*selected statements*)
   114   -> (string list * string list)        (*selected statements*)
   115   -> serialization;
   115   -> serialization;
   116 
   116 
   117 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
   117 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
   118       check: { env_var: string, make_destination: Path.T -> Path.T,
   118       check: { env_var: string, make_destination: Path.T -> Path.T,
   119         make_command: string -> Path.T -> string -> string } }
   119         make_command: string -> string -> string } }
   120   | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
   120   | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
   121 
   121 
   122 datatype target = Target of {
   122 datatype target = Target of {
   123   serial: serial,
   123   serial: serial,
   124   description: description,
   124   description: description,
   334     fun ext_check env_param p =
   334     fun ext_check env_param p =
   335       let 
   335       let 
   336         val destination = make_destination p;
   336         val destination = make_destination p;
   337         val _ = file destination (serialize thy target (SOME 80)
   337         val _ = file destination (serialize thy target (SOME 80)
   338           (SOME module_name) args naming program names_cs);
   338           (SOME module_name) args naming program names_cs);
   339         val cmd = make_command env_param destination module_name;
   339         val cmd = make_command env_param module_name;
   340       in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
   340       in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
   341         then error ("Code check failed for " ^ target ^ ": " ^ cmd)
   341         then error ("Code check failed for " ^ target ^ ": " ^ cmd)
   342         else ()
   342         else ()
   343       end;
   343       end;
   344   in if env_param = ""
   344   in if env_param = ""