equal
deleted
inserted
replaced
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 = "" |