PrintMode.with_default;
authorwenzelm
Mon Jul 23 16:44:59 2007 +0200 (2007-07-23)
changeset 239314d82207fb251
parent 23930 6d81e2ef69f7
child 23932 7afee4bf89e8
PrintMode.with_default;
src/Pure/Tools/codegen_serializer.ML
src/Pure/codegen.ML
     1.1 --- a/src/Pure/Tools/codegen_serializer.ML	Mon Jul 23 15:16:35 2007 +0200
     1.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Mon Jul 23 16:44:59 2007 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  infixr 5 @|;
     1.5  fun x @@ y = [x, y];
     1.6  fun xs @| y = xs @ [y];
     1.7 -val str = setmp print_mode [] Pretty.str;
     1.8 +val str = PrintMode.with_default Pretty.str;
     1.9  val concat = Pretty.block o Pretty.breaks;
    1.10  val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
    1.11  fun semicolon ps = Pretty.block [concat ps, str ";"];
     2.1 --- a/src/Pure/codegen.ML	Mon Jul 23 15:16:35 2007 +0200
     2.2 +++ b/src/Pure/codegen.ML	Mon Jul 23 16:44:59 2007 +0200
     2.3 @@ -879,7 +879,7 @@
     2.4    end;
     2.5  
     2.6  fun gen_generate_code prep_term thy modules module =
     2.7 -  setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
     2.8 +  PrintMode.with_default (Pretty.setmp_margin (!margin) (fn xs =>
     2.9    let
    2.10      val _ = (module <> "" orelse
    2.11          member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
    2.12 @@ -973,7 +973,7 @@
    2.13        map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
    2.14      val (code, gr) = setmp mode ["term_of", "test"]
    2.15        (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
    2.16 -    val s = setmp print_mode [] (fn () => "structure TestTerm =\nstruct\n\n" ^
    2.17 +    val s = PrintMode.with_default (fn () => "structure TestTerm =\nstruct\n\n" ^
    2.18        space_implode "\n" (map snd code) ^
    2.19        "\nopen Generated;\n\n" ^ Pretty.string_of
    2.20          (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
    2.21 @@ -1032,7 +1032,7 @@
    2.22  
    2.23  val eval_result = ref (Bound 0);
    2.24  
    2.25 -fun eval_term thy = setmp print_mode [] (fn t =>
    2.26 +fun eval_term thy = PrintMode.with_default (fn t =>
    2.27    let
    2.28      val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
    2.29        error "Term to be evaluated contains type variables";
    2.30 @@ -1078,7 +1078,7 @@
    2.31  
    2.32  (**** Interface ****)
    2.33  
    2.34 -val str = setmp print_mode [] Pretty.str;
    2.35 +val str = PrintMode.with_default Pretty.str;
    2.36  
    2.37  fun parse_mixfix rd s =
    2.38    (case Scan.finite Symbol.stopper (Scan.repeat