# HG changeset patch # User haftmann # Date 1283173292 -7200 # Node ID 919c924067f3c504ecc844270c7ac23c5f6ad11d # Parent 732149f6ebf9bf03399c804d0299eb83ebd31ea4 whitespace tuning diff -r 732149f6ebf9 -r 919c924067f3 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Aug 30 14:48:25 2010 +0200 +++ b/src/Tools/Code/code_target.ML Mon Aug 30 15:01:32 2010 +0200 @@ -1,7 +1,8 @@ (* Title: Tools/Code/code_target.ML Author: Florian Haftmann, TU Muenchen -Generic infrastructure for serializers from intermediate language ("Thin-gol") to target languages. +Generic infrastructure for serializers from intermediate language ("Thin-gol" +to target languages. *) signature CODE_TARGET = @@ -29,7 +30,8 @@ val serialize: theory -> string -> int option -> string option -> Token.T list -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization val serialize_custom: theory -> string * serializer -> string option - -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list + -> Code_Thingol.naming -> Code_Thingol.program -> string list + -> string * string option list val the_literals: theory -> string -> literals val export: serialization -> unit val file: Path.T -> serialization -> unit @@ -90,7 +92,8 @@ NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const }; fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) = mk_name_syntax_table (f ((class, instance), (tyco, const))); -fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 }, +fun merge_name_syntax_table + (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 }, NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) = mk_name_syntax_table ( (Symtab.join (K snd) (class1, class2), @@ -114,10 +117,12 @@ -> (string list * string list) (*selected statements*) -> serialization; -datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, +datatype description = Fundamental of { serializer: serializer, + literals: Code_Printer.literals, check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string -> string } } - | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program); + | Extension of string * + (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program); datatype target = Target of { serial: serial, @@ -190,8 +195,8 @@ thy |> (Targets.map o apfst o apfst o Symtab.update) (target, make_target ((serial (), seri), (([], Symtab.empty), - (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)), - Symtab.empty)))) + (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), + (Symtab.empty, Symtab.empty)), Symtab.empty)))) end; fun add_target (target, seri) = put_target (target, Fundamental seri);