src/Tools/Code/code_target.ML

 
 (** theory data **)
 
 type language = {serializer: serializer, literals: literals,
   check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string},
-  evaluation_args: Token.T list}; 
+  evaluation_args: Token.T list};
 
 type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list;
 
 val merge_ancestry : ancestry * ancestry -> ancestry = AList.join (op =) (K snd);
 

     Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
       if #serial target1 = #serial target2 then
       ({serial = #serial target1, language = #language target1,
         ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
         Code_Printer.merge_data (data1, data2))
-      else error ("Incompatible targets: " ^ quote target_name) 
+      else error ("Incompatible targets: " ^ quote target_name)
     ) (targets1, targets2)
 );
 
 fun exists_target thy = Symtab.defined (Targets.get thy);
 fun lookup_target_data thy = Symtab.lookup (Targets.get thy);

 
 fun fold1 f xs = fold f (tl xs) (hd xs);
 
 fun join_ancestry thy target_name =
   let
-    val _ = assert_target thy target_name; 
+    val _ = assert_target thy target_name;
     val the_target_data = the o lookup_target_data thy;
     val (target, this_data) = the_target_data target_name;
     val ancestry = #ancestry target;
     val modifies = rev (map snd ancestry);
     val modify = fold (curry (op o)) modifies I;

     val _ = if exists_target thy target_name
       then error ("Attempt to overwrite existing target " ^ quote target_name)
       else ();
   in
     thy
-    |> (Targets.map o Symtab.update) (target_name, (target, Code_Printer.empty_data))  
+    |> (Targets.map o Symtab.update) (target_name, (target, Code_Printer.empty_data))
   end;
 
 fun add_language (target_name, language) =
   allocate_target target_name {serial = serial (), language = language,
     ancestry = []};

     val ancestries = map #ancestry targets @ [initial_ancestry];
     val ancestry = fold1 (fn ancestry' => fn ancestry =>
       merge_ancestry (ancestry, ancestry')) ancestries;
   in
     allocate_target target_name {serial = #serial supremum, language = #language supremum,
-      ancestry = ancestry} thy 
-  end;
-  
+      ancestry = ancestry} thy
+  end;
+
 fun map_data target_name f thy =
   let
     val _ = assert_target thy target_name;
   in
     thy
     |> (Targets.map o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
   end;
 
-fun map_reserved target_name =
-  map_data target_name o @{apply 3 (1)};
-fun map_identifiers target_name =
-  map_data target_name o @{apply 3 (2)};
-fun map_printings target_name =
-  map_data target_name o @{apply 3 (3)};
+fun map_reserved target_name = map_data target_name o @{apply 3(1)};
+fun map_identifiers target_name = map_data target_name o @{apply 3(2)};
+fun map_printings target_name = map_data target_name o @{apply 3(3)};
 
 
 (** serializer usage **)
 
 (* technical aside: pretty printing width *)

       (fn () => dynamic_compilation_text prepared_serializer width prepared_program syms) ctxt
   end;
 
 fun compilation_text ctxt target_name program syms =
   fst oo compilation_text' ctxt target_name NONE program syms
-  
+
 end; (* local *)
 
 
 (* code generation *)