--- 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