PrintMode.with_default;
authorwenzelm
Mon, 23 Jul 2007 16:44:59 +0200
changeset 23931 4d82207fb251
parent 23930 6d81e2ef69f7
child 23932 7afee4bf89e8
PrintMode.with_default;
src/Pure/Tools/codegen_serializer.ML
src/Pure/codegen.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Mon Jul 23 15:16:35 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Jul 23 16:44:59 2007 +0200
@@ -53,7 +53,7 @@
 infixr 5 @|;
 fun x @@ y = [x, y];
 fun xs @| y = xs @ [y];
-val str = setmp print_mode [] Pretty.str;
+val str = PrintMode.with_default Pretty.str;
 val concat = Pretty.block o Pretty.breaks;
 val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
 fun semicolon ps = Pretty.block [concat ps, str ";"];
--- a/src/Pure/codegen.ML	Mon Jul 23 15:16:35 2007 +0200
+++ b/src/Pure/codegen.ML	Mon Jul 23 16:44:59 2007 +0200
@@ -879,7 +879,7 @@
   end;
 
 fun gen_generate_code prep_term thy modules module =
-  setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
+  PrintMode.with_default (Pretty.setmp_margin (!margin) (fn xs =>
   let
     val _ = (module <> "" orelse
         member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
@@ -973,7 +973,7 @@
       map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
     val (code, gr) = setmp mode ["term_of", "test"]
       (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
-    val s = setmp print_mode [] (fn () => "structure TestTerm =\nstruct\n\n" ^
+    val s = PrintMode.with_default (fn () => "structure TestTerm =\nstruct\n\n" ^
       space_implode "\n" (map snd code) ^
       "\nopen Generated;\n\n" ^ Pretty.string_of
         (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
@@ -1032,7 +1032,7 @@
 
 val eval_result = ref (Bound 0);
 
-fun eval_term thy = setmp print_mode [] (fn t =>
+fun eval_term thy = PrintMode.with_default (fn t =>
   let
     val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
       error "Term to be evaluated contains type variables";
@@ -1078,7 +1078,7 @@
 
 (**** Interface ****)
 
-val str = setmp print_mode [] Pretty.str;
+val str = PrintMode.with_default Pretty.str;
 
 fun parse_mixfix rd s =
   (case Scan.finite Symbol.stopper (Scan.repeat