src/Pure/codegen.ML
changeset 24634 38db11874724
parent 24585 c359896d0f48
child 24655 24b630fd008f
     1.1 --- a/src/Pure/codegen.ML	Tue Sep 18 18:05:34 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Tue Sep 18 18:05:37 2007 +0200
     1.3 @@ -827,7 +827,7 @@
     1.4    end;
     1.5  
     1.6  fun gen_generate_code prep_term thy modules module =
     1.7 -  PrintMode.with_default (Pretty.setmp_margin (!margin) (fn xs =>
     1.8 +  PrintMode.setmp [] (Pretty.setmp_margin (!margin) (fn xs =>
     1.9    let
    1.10      val _ = (module <> "" orelse
    1.11          member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
    1.12 @@ -921,7 +921,7 @@
    1.13        map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
    1.14      val (code, gr) = setmp mode ["term_of", "test"]
    1.15        (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
    1.16 -    val s = PrintMode.with_default (fn () => "structure TestTerm =\nstruct\n\n" ^
    1.17 +    val s = PrintMode.setmp [] (fn () => "structure TestTerm =\nstruct\n\n" ^
    1.18        space_implode "\n" (map snd code) ^
    1.19        "\nopen Generated;\n\n" ^ Pretty.string_of
    1.20          (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
    1.21 @@ -1004,7 +1004,7 @@
    1.22  
    1.23  val eval_result = ref (Bound 0);
    1.24  
    1.25 -fun eval_term thy = PrintMode.with_default (fn t =>
    1.26 +fun eval_term thy = PrintMode.setmp [] (fn t =>
    1.27    let
    1.28      val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
    1.29        error "Term to be evaluated contains type variables";
    1.30 @@ -1051,7 +1051,7 @@
    1.31  
    1.32  (**** Interface ****)
    1.33  
    1.34 -val str = PrintMode.with_default Pretty.str;
    1.35 +val str = PrintMode.setmp [] Pretty.str;
    1.36  
    1.37  fun parse_mixfix rd s =
    1.38    (case Scan.finite Symbol.stopper (Scan.repeat