# HG changeset patch # User wenzelm # Date 1185201899 -7200 # Node ID 4d82207fb25146e8de7b22b1ab609f4fc1f38754 # Parent 6d81e2ef69f772676bedfbb1ec6cba397904718b PrintMode.with_default; diff -r 6d81e2ef69f7 -r 4d82207fb251 src/Pure/Tools/codegen_serializer.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 ";"]; diff -r 6d81e2ef69f7 -r 4d82207fb251 src/Pure/codegen.ML --- 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