# HG changeset patch # User haftmann # Date 1283178786 -7200 # Node ID c0b857a0475856f3b7a0ba5ff1a1067fcecf6957 # Parent 026526cba0e668ef7b5f4aa0ab1641badc655af7 tuned diff -r 026526cba0e6 -r c0b857a04758 src/Tools/Code/code_haskell.ML --- 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 diff -r 026526cba0e6 -r c0b857a04758 src/Tools/Code/code_ml.ML --- 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*) diff -r 026526cba0e6 -r c0b857a04758 src/Tools/Code/code_scala.ML --- 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*) diff -r 026526cba0e6 -r c0b857a04758 src/Tools/Code/code_target.ML --- 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 **)