--- a/src/Tools/Code/code_haskell.ML Mon Aug 30 16:31:38 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon Aug 30 16:33:06 2010 +0200
@@ -390,7 +390,7 @@
end
| write_module width NONE (_, content) = writeln_pretty width content;
in
- Code_Target.mk_serialization
+ Code_Target.serialization
(fn width => fn destination => K () o map (write_module width destination))
(fn width => rpair [] o cat_lines o map (string_of_pretty width o snd))
(map (uncurry print_module) includes
--- a/src/Tools/Code/code_ml.ML Mon Aug 30 16:31:38 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Mon Aug 30 16:33:06 2010 +0200
@@ -937,7 +937,7 @@
fun write width NONE = writeln_pretty width
| write width (SOME p) = File.write p o string_of_pretty width;
in
- Code_Target.mk_serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
+ Code_Target.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
end;
end; (*local*)
--- a/src/Tools/Code/code_scala.ML Mon Aug 30 16:31:38 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Mon Aug 30 16:33:06 2010 +0200
@@ -483,7 +483,7 @@
fun write width NONE = writeln_pretty width
| write width (SOME p) = File.write p o string_of_pretty width;
in
- Code_Target.mk_serialization write (rpair [] oo string_of_pretty) p
+ Code_Target.serialization write (rpair [] oo string_of_pretty) p
end;
end; (*local*)
--- a/src/Tools/Code/code_target.ML Mon Aug 30 16:31:38 2010 +0200
+++ b/src/Tools/Code/code_target.ML Mon Aug 30 16:33:06 2010 +0200
@@ -22,7 +22,7 @@
type destination
type serialization
val parse_args: 'a parser -> Token.T list -> 'a
- val mk_serialization: (int -> Path.T option -> 'a -> unit)
+ val serialization: (int -> Path.T option -> 'a -> unit)
-> (int -> 'a -> string * string option list)
-> 'a -> int -> serialization
val serialize: theory -> string -> int option -> string option -> Token.T list
@@ -70,8 +70,8 @@
fun stmt_names_of_destination (String stmt_names) = stmt_names
| stmt_names_of_destination _ = [];
-fun mk_serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
- | mk_serialization _ string pretty width (String _) = SOME (string width pretty);
+fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
+ | serialization _ string pretty width (String _) = SOME (string width pretty);
(** theory data **)