# 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);