whitespace tuning
authorhaftmann
Mon Aug 30 15:01:32 2010 +0200 (2010-08-30)
changeset 38909919c924067f3
parent 38908 732149f6ebf9
child 38910 6af1d8673cbf
whitespace tuning
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 14:48:25 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Aug 30 15:01:32 2010 +0200
     1.3 @@ -1,7 +1,8 @@
     1.4  (*  Title:      Tools/Code/code_target.ML
     1.5      Author:     Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Generic infrastructure for serializers from intermediate language ("Thin-gol") to target languages.
     1.8 +Generic infrastructure for serializers from intermediate language ("Thin-gol"
     1.9 +to target languages.
    1.10  *)
    1.11  
    1.12  signature CODE_TARGET =
    1.13 @@ -29,7 +30,8 @@
    1.14    val serialize: theory -> string -> int option -> string option -> Token.T list
    1.15      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    1.16    val serialize_custom: theory -> string * serializer -> string option
    1.17 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    1.18 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list
    1.19 +    -> string * string option list
    1.20    val the_literals: theory -> string -> literals
    1.21    val export: serialization -> unit
    1.22    val file: Path.T -> serialization -> unit
    1.23 @@ -90,7 +92,8 @@
    1.24    NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
    1.25  fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
    1.26    mk_name_syntax_table (f ((class, instance), (tyco, const)));
    1.27 -fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
    1.28 +fun merge_name_syntax_table
    1.29 +  (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
    1.30      NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
    1.31    mk_name_syntax_table (
    1.32      (Symtab.join (K snd) (class1, class2),
    1.33 @@ -114,10 +117,12 @@
    1.34    -> (string list * string list)        (*selected statements*)
    1.35    -> serialization;
    1.36  
    1.37 -datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
    1.38 +datatype description = Fundamental of { serializer: serializer,
    1.39 +      literals: Code_Printer.literals,
    1.40        check: { env_var: string, make_destination: Path.T -> Path.T,
    1.41          make_command: string -> string -> string } }
    1.42 -  | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    1.43 +  | Extension of string *
    1.44 +      (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    1.45  
    1.46  datatype target = Target of {
    1.47    serial: serial,
    1.48 @@ -190,8 +195,8 @@
    1.49      thy
    1.50      |> (Targets.map o apfst o apfst o Symtab.update)
    1.51            (target, make_target ((serial (), seri), (([], Symtab.empty),
    1.52 -            (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
    1.53 -              Symtab.empty))))
    1.54 +            (mk_name_syntax_table ((Symtab.empty, Symreltab.empty),
    1.55 +              (Symtab.empty, Symtab.empty)), Symtab.empty))))
    1.56    end;
    1.57  
    1.58  fun add_target (target, seri) = put_target (target, Fundamental seri);