# HG changeset patch
# User haftmann
# Date 1283176841 -7200
# Node ID 6af1d8673cbfb46d47f335bf1d2d2624e56c7736
# Parent  919c924067f3c504ecc844270c7ac23c5f6ad11d
width is a formal parameter of serialization

diff -r 919c924067f3 -r 6af1d8673cbf src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Mon Aug 30 15:01:32 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Mon Aug 30 16:00:41 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 (code_of_pretty, code_writeln) program
-    (stmt_names, presentation_stmt_names) destination =
+    (stmt_names, presentation_stmt_names) width =
   let
     val reserved = fold (insert (op =) o fst) includes raw_reserved;
     val (deresolver, hs_program) = haskell_program_of_program labelled_name
@@ -390,13 +390,13 @@
           ^ code_of_pretty content)
       end
   in
-    Code_Target.mk_serialization target
-      (fn NONE => K () o map (code_writeln o (fn p => Pretty.block [p, Pretty.fbrk]) o snd)
-        | SOME file => K () o map (write_module (check_destination file)))
-      (rpair [] o cat_lines o map (code_of_pretty o snd))
+    Code_Target.mk_serialization
+      (fn width => (fn NONE => K () o map (code_writeln o (fn p => Pretty.block [p, Pretty.fbrk]) o snd)
+        | SOME file => K () o map (write_module (check_destination file))))
+      (fn width => (rpair [] o cat_lines o map (code_of_pretty o snd)))
       (map (uncurry print_module) includes
         @ map serialize_module (Symtab.dest hs_program))
-      destination
+      width
   end;
 
 val literals = let
diff -r 919c924067f3 -r 6af1d8673cbf src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Aug 30 15:01:32 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Mon Aug 30 16:00:41 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 (code_of_pretty, code_writeln) program
-  (stmt_names, presentation_stmt_names) =
+  (stmt_names, presentation_stmt_names) width =
   let
     val is_cons = Code_Thingol.is_cons program;
     val is_presentation = not (null presentation_stmt_names);
@@ -935,9 +935,9 @@
       (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
   in
-    Code_Target.mk_serialization target
-      (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
-      (rpair stmt_names' o code_of_pretty) p
+    Code_Target.mk_serialization
+      (fn width => (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty))
+      (fn width => (rpair stmt_names' o code_of_pretty)) p width 
   end;
 
 end; (*local*)
diff -r 919c924067f3 -r 6af1d8673cbf src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Mon Aug 30 15:01:32 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Mon Aug 30 16:00:41 2010 +0200
@@ -415,7 +415,7 @@
 
 fun serialize_scala labelled_name raw_reserved includes module_alias
     _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
-    program (stmt_names, presentation_stmt_names) destination =
+    program (stmt_names, presentation_stmt_names) width =
   let
 
     (* build program *)
@@ -481,9 +481,9 @@
       then map (fn (base, p) => print_module base [] p) includes else [];
     val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
   in
-    Code_Target.mk_serialization target
-      (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
-      (rpair [] o code_of_pretty) p destination
+    Code_Target.mk_serialization
+      (fn width => (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty))
+      (fn width => (rpair [] o code_of_pretty)) p width
   end;
 
 end; (*local*)
diff -r 919c924067f3 -r 6af1d8673cbf src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Aug 30 15:01:32 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Mon Aug 30 16:00:41 2010 +0200
@@ -1,8 +1,7 @@
 (*  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 target language data.
 *)
 
 signature CODE_TARGET =
@@ -24,9 +23,9 @@
   type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
   val stmt_names_of_destination: destination -> string list
-  val mk_serialization: string -> (Path.T option -> 'a -> unit)
-    -> ('a -> string * string option list)
-    -> 'a -> serialization
+  val mk_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
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
   val serialize_custom: theory -> string * serializer -> string option
@@ -64,19 +63,18 @@
 
 (** basics **)
 
-datatype destination = Export | File of Path.T | String of string list;
+datatype destination = File of Path.T option | String of string list;
 type serialization = destination -> (string * string option list) option;
 
-fun export f = (f Export; ());
-fun file p f = (f (File p); ());
+fun export f = (f (File NONE); ());
+fun file p f = (f (File (SOME p)); ());
 fun string stmts f = fst (the (f (String stmts)));
 
 fun stmt_names_of_destination (String stmts) = stmts
   | stmt_names_of_destination _ = [];
 
-fun mk_serialization target output _ code Export = (output NONE code ; NONE)
-  | mk_serialization target output _ code (File file) = (output (SOME file) code; NONE)
-  | mk_serialization target _ string code (String _) = SOME (string code);
+fun mk_serialization output _ code width (File p) = (output width p code; NONE)
+  | mk_serialization _ string code width (String _) = SOME (string width code);
 
 
 (** theory data **)
@@ -115,10 +113,11 @@
   -> ((Pretty.T -> string) * (Pretty.T -> unit))
   -> Code_Thingol.program
   -> (string list * string list)        (*selected statements*)
+  -> int
   -> serialization;
 
 datatype description = Fundamental of { serializer: serializer,
-      literals: Code_Printer.literals,
+      literals: literals,
       check: { env_var: string, make_destination: Path.T -> Path.T,
         make_command: string -> string -> string } }
   | Extension of string *
@@ -259,7 +258,7 @@
   |>> map_filter I;
 
 fun invoke_serializer thy abortable serializer literals reserved abs_includes 
-    module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
+    module_alias class instance tyco const module_name args naming program2 (names1, presentation_names) width =
   let
     val (names_class, class') =
       activate_syntax (Code_Thingol.lookup_class naming) class;
@@ -284,7 +283,7 @@
       (if is_some module_name then K module_name else Symtab.lookup module_alias)
       (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
       (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
-      program4 (names1, presentation_names)
+      program4 (names1, presentation_names) width
   end;
 
 fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
@@ -322,8 +321,8 @@
     val width = the_default default_width some_width;
   in
     invoke_serializer thy abortable serializer literals reserved
-      includes module_alias class instance tyco const module_name width args
-        naming (modify program) (names, presentation_names) destination
+      includes module_alias class instance tyco const module_name args
+        naming (modify program) (names, presentation_names) width destination
   end;
 
 in