src/Pure/context.ML
changeset 18711 cf020c54e2f5
parent 18678 dd0c569fa43d
child 18731 3989c3c41983
     1.1 --- a/src/Pure/context.ML	Thu Jan 19 21:22:15 2006 +0100
     1.2 +++ b/src/Pure/context.ML	Thu Jan 19 21:22:16 2006 +0100
     1.3 @@ -62,8 +62,8 @@
     1.4    val use_mltext: string -> bool -> theory option -> unit
     1.5    val use_mltext_theory: string -> bool -> theory -> theory
     1.6    val use_let: string -> string -> string -> theory -> theory
     1.7 -  val add_setup: (theory -> theory) list -> unit
     1.8 -  val setup: unit -> (theory -> theory) list
     1.9 +  val add_setup: (theory -> theory) -> unit
    1.10 +  val setup: unit -> theory -> theory
    1.11    (*proof context*)
    1.12    type proof
    1.13    val theory_of_proof: proof -> theory
    1.14 @@ -476,7 +476,8 @@
    1.15  
    1.16  val ml_output = (writeln, Output.error_msg);
    1.17  
    1.18 -fun use_output verbose txt = use_text ml_output verbose (Symbol.escape txt);
    1.19 +fun use_output verbose txt =
    1.20 +  Output.ML_errors (use_text ml_output verbose) (Symbol.escape txt);
    1.21  
    1.22  fun use_mltext txt verbose opt_thy = setmp opt_thy (fn () => use_output verbose txt) ();
    1.23  fun use_mltext_theory txt verbose thy = #2 (pass_theory thy (use_output verbose) txt);
    1.24 @@ -490,10 +491,10 @@
    1.25  (* delayed theory setup *)
    1.26  
    1.27  local
    1.28 -  val setup_fns = ref ([]: (theory -> theory) list);
    1.29 +  val setup_fn = ref (I: theory -> theory);
    1.30  in
    1.31 -  fun add_setup fns = setup_fns := ! setup_fns @ fns;
    1.32 -  fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end;
    1.33 +  fun add_setup f = setup_fn := (! setup_fn #> f);
    1.34 +  fun setup () = let val f = ! setup_fn in setup_fn := I; f end;
    1.35  end;
    1.36  
    1.37