# HG changeset patch
# User haftmann
# Date 1285234162 -7200
# Node ID 07549694e2f1267b00fb7b43f681bd4a1b4b2629
# Parent  7bf0c7f0f24c5be6dab77a68eb7e82a6c7603c55
shifted abstraction over imperative print mode

diff -r 7bf0c7f0f24c -r 07549694e2f1 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Sep 23 10:39:25 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Sep 23 11:29:22 2010 +0200
@@ -115,19 +115,19 @@
 infixr 5 @|;
 fun x @@ y = [x, y];
 fun xs @| y = xs @ [y];
-val str = Print_Mode.setmp [] Pretty.str;
+val str = Print_Mode.with_modes [] Pretty.str;
 val concat = Pretty.block o Pretty.breaks;
-val commas = Print_Mode.setmp [] Pretty.commas;
-fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
+val commas = Print_Mode.with_modes [] Pretty.commas;
+fun enclose l r = Print_Mode.with_modes [] (Pretty.enclose l r);
 val brackets = enclose "(" ")" o Pretty.breaks;
-fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
+fun enum sep l r = Print_Mode.with_modes [] (Pretty.enum sep l r);
 fun enum_default default sep l r [] = str default
   | enum_default default sep l r xs = enum sep l r xs;
 fun semicolon ps = Pretty.block [concat ps, str ";"];
 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
-fun indent i = Print_Mode.setmp [] (Pretty.indent i);
+fun indent i = Print_Mode.with_modes [] (Pretty.indent i);
 
-fun markup_stmt name = Print_Mode.setmp [code_presentationN]
+fun markup_stmt name = Print_Mode.with_modes [code_presentationN]
   (Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
 
 fun filter_presentation [] tree =
@@ -150,7 +150,7 @@
       in snd (fold filter tree (true, Buffer.empty)) end;
 
 fun format presentation_names width =
-  Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
+  Print_Mode.with_modes [code_presentationN] (Pretty.string_of_margin width)
   #> YXML.parse_body
   #> filter_presentation presentation_names
   #> Buffer.content;
diff -r 7bf0c7f0f24c -r 07549694e2f1 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Sep 23 10:39:25 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Sep 23 11:29:22 2010 +0200
@@ -73,13 +73,21 @@
 datatype destination = Export of Path.T option | Produce | Present of string list;
 type serialization = int -> destination -> (string * (string -> string option)) option;
 
-fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
-  | serialization _ string content width Produce = SOME (string [] width content)
-  | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content);
+fun using_plain_output f x = Print_Mode.setmp [] f x;
 
-fun export some_path f = (f (Export some_path); ());
-fun produce f = the (f Produce);
-fun present stmt_names f = fst (the (f (Present stmt_names)));
+fun serialization output _ content width (Export some_path) =
+      (using_plain_output (output width some_path) content; NONE)
+  | serialization _ string content width Produce = 
+      SOME (using_plain_output (string [] width) content)
+  | serialization _ string content width (Present stmt_names) =
+      SOME (using_plain_output (string stmt_names width) content);
+
+fun export some_path serializer naming program names =
+  (using_plain_output (serializer naming program) names (Export some_path); ());
+fun produce serializer naming program names =
+  the (using_plain_output (serializer naming program) names Produce);
+fun present stmt_names serializer naming program names =
+  fst (the (using_plain_output (serializer naming program) names (Present stmt_names)));
 
 
 (** theory data **)
@@ -351,20 +359,20 @@
 in
 
 fun export_code_for thy some_path target some_width module_name args =
-  export some_path ooo mount_serializer thy target some_width module_name args;
+  export some_path (mount_serializer thy target some_width module_name args);
 
 fun produce_code_for thy target some_width module_name args =
   let
     val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
   in fn naming => fn program => fn names =>
-    produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
+    produce serializer naming program names |> apsnd (fn deresolve => map deresolve names)
   end;
 
 fun present_code_for thy target some_width module_name args =
   let
     val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
   in fn naming => fn program => fn (names, selects) =>
-    present selects (serializer naming program names)
+    present selects serializer naming program names
   end;
 
 fun check_code_for thy target strict args naming program names_cs =
@@ -377,7 +385,7 @@
       let 
         val destination = make_destination p;
         val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
-          module_name args naming program names_cs);
+          module_name args) naming program names_cs;
         val cmd = make_command env_param module_name;
       in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
         then error ("Code check failed for " ^ target ^ ": " ^ cmd)