diff -r 3cbb22cec751 -r cf3588177676 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Wed Jul 14 14:53:44 2010 +0200 +++ b/src/Tools/Code/code_target.ML Wed Jul 14 15:08:02 2010 +0200 @@ -11,8 +11,9 @@ 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 @@ -35,8 +36,7 @@ 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 @@ -115,7 +115,9 @@ -> 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 { @@ -221,15 +223,17 @@ (* 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 @@ -353,8 +357,10 @@ 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 = +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 @@ -374,6 +380,7 @@ 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;