# HG changeset patch
# User haftmann
# Date 1283178107 -7200
# Node ID d1d4d808be26ebf41200e9c2a2fc212de1cf0cb5
# Parent  c79c1e4e11115cc311cfd036457fe1e3babe229f
tuned

diff -r c79c1e4e1111 -r d1d4d808be26 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Mon Aug 30 16:17:10 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Mon Aug 30 16:21:47 2010 +0200
@@ -316,7 +316,7 @@
 fun serialize_haskell module_prefix module_name string_classes labelled_name
     raw_reserved includes module_alias
     syntax_class syntax_tyco syntax_const program
-    (stmt_names, presentation_stmt_names) width =
+    (stmt_names, presentation_stmt_names) =
   let
     val reserved = fold (insert (op =) o fst) includes raw_reserved;
     val (deresolver, hs_program) = haskell_program_of_program labelled_name
@@ -396,7 +396,6 @@
       (fn width => (rpair [] o cat_lines o map (string_of_pretty width o snd)))
       (map (uncurry print_module) includes
         @ map serialize_module (Symtab.dest hs_program))
-      width
   end;
 
 val literals = let
diff -r c79c1e4e1111 -r d1d4d808be26 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Aug 30 16:17:10 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Mon Aug 30 16:21:47 2010 +0200
@@ -908,7 +908,7 @@
 
 fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
   reserved includes module_alias _ syntax_tyco syntax_const program
-  (stmt_names, presentation_stmt_names) width =
+  (stmt_names, presentation_stmt_names) =
   let
     val is_cons = Code_Thingol.is_cons program;
     val is_presentation = not (null presentation_stmt_names);
@@ -937,7 +937,7 @@
   in
     Code_Target.mk_serialization
       (fn width => (fn NONE => writeln_pretty width | SOME file => File.write file o string_of_pretty width))
-      (fn width => (rpair stmt_names' o string_of_pretty width)) p width 
+      (fn width => (rpair stmt_names' o string_of_pretty width)) p
   end;
 
 end; (*local*)
diff -r c79c1e4e1111 -r d1d4d808be26 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Mon Aug 30 16:17:10 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Mon Aug 30 16:21:47 2010 +0200
@@ -415,7 +415,7 @@
 
 fun serialize_scala labelled_name raw_reserved includes module_alias
     _ syntax_tyco syntax_const
-    program (stmt_names, presentation_stmt_names) width =
+    program (stmt_names, presentation_stmt_names) =
   let
 
     (* build program *)
@@ -483,7 +483,7 @@
   in
     Code_Target.mk_serialization
       (fn width => (fn NONE => writeln_pretty width | SOME file => File.write file o string_of_pretty width))
-      (rpair [] oo string_of_pretty) p width
+      (rpair [] oo string_of_pretty) p
   end;
 
 end; (*local*)
diff -r c79c1e4e1111 -r d1d4d808be26 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Aug 30 16:17:10 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Mon Aug 30 16:21:47 2010 +0200
@@ -22,7 +22,6 @@
   type destination
   type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
-  val stmt_names_of_destination: destination -> string list
   val mk_serialization: (int -> Path.T option -> 'a -> unit)
     -> (int -> 'a -> string * string option list)
     -> 'a -> int -> serialization
@@ -67,14 +66,14 @@
 type serialization = destination -> (string * string option list) option;
 
 fun export f = (f (File NONE); ());
-fun file p f = (f (File (SOME p)); ());
-fun string stmts f = fst (the (f (String stmts)));
+fun file path f = (f (File (SOME path)); ());
+fun string stmt_names f = fst (the (f (String stmt_names)));
 
-fun stmt_names_of_destination (String stmts) = stmts
+fun stmt_names_of_destination (String stmt_names) = stmt_names
   | stmt_names_of_destination _ = [];
 
-fun mk_serialization output _ code width (File p) = (output width p code; NONE)
-  | mk_serialization _ string code width (String _) = SOME (string width code);
+fun mk_serialization output _ pretty width (File path) = (output width path pretty; NONE)
+  | mk_serialization _ string pretty width (String _) = SOME (string width pretty);
 
 
 (** theory data **)