src/Pure/context.ML
changeset 22095 07875394618e
parent 22085 c138cfd500f7
child 22131 fa8960e165a6
     1.1 --- a/src/Pure/context.ML	Fri Jan 19 22:08:01 2007 +0100
     1.2 +++ b/src/Pure/context.ML	Fri Jan 19 22:08:02 2007 +0100
     1.3 @@ -3,8 +3,8 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Generic theory contexts with unique identity, arbitrarily typed data,
     1.7 -development graph and history support.  Implicit theory contexts in ML.
     1.8 -Generic proof contexts with arbitrarily typed data.
     1.9 +development graph and history support. Generic proof contexts with
    1.10 +arbitrarily typed data.
    1.11  *)
    1.12  
    1.13  signature BASIC_CONTEXT =
    1.14 @@ -12,7 +12,6 @@
    1.15    type theory
    1.16    type theory_ref
    1.17    exception THEORY of string * theory list
    1.18 -  val the_context: unit -> theory
    1.19  end;
    1.20  
    1.21  signature CONTEXT =
    1.22 @@ -67,19 +66,7 @@
    1.23    val proof_map: (generic -> generic) -> proof -> proof
    1.24    val theory_of: generic -> theory   (*total*)
    1.25    val proof_of: generic -> proof     (*total*)
    1.26 -  (*ML context*)
    1.27 -  val get_context: unit -> generic option
    1.28 -  val set_context: generic option -> unit
    1.29 -  val setmp: generic option -> ('a -> 'b) -> 'a -> 'b
    1.30 -  val the_generic_context: unit -> generic
    1.31 -  val the_local_context: unit -> proof
    1.32 -  val pass: generic option -> ('a -> 'b) -> 'a -> 'b * generic option
    1.33 -  val pass_context: generic -> ('a -> 'b) -> 'a -> 'b * generic
    1.34 -  val save: ('a -> 'b) -> 'a -> 'b
    1.35 -  val >> : (theory -> theory) -> unit
    1.36 -  val use_mltext: string -> bool -> generic option -> unit
    1.37 -  val use_mltext_update: string -> bool -> generic -> generic
    1.38 -  val use_let: string -> string -> string -> generic -> generic
    1.39 +  (*delayed setup*)
    1.40    val add_setup: (theory -> theory) -> unit
    1.41    val setup: unit -> theory -> theory
    1.42  end;
    1.43 @@ -543,57 +530,7 @@
    1.44  
    1.45  
    1.46  
    1.47 -(*** ML context ***)
    1.48 -
    1.49 -local
    1.50 -  val current_context = ref (NONE: generic option);
    1.51 -in
    1.52 -  fun get_context () = ! current_context;
    1.53 -  fun set_context opt_context = current_context := opt_context;
    1.54 -  fun setmp opt_context f x = Library.setmp current_context opt_context f x;
    1.55 -end;
    1.56 -
    1.57 -fun the_generic_context () =
    1.58 -  (case get_context () of
    1.59 -    SOME context => context
    1.60 -  | _ => error "Unknown context");
    1.61 -
    1.62 -val the_context = theory_of o the_generic_context;
    1.63 -val the_local_context = the_proof o the_generic_context;
    1.64 -
    1.65 -fun pass opt_context f x =
    1.66 -  setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x;
    1.67 -
    1.68 -fun pass_context context f x =
    1.69 -  (case pass (SOME context) f x of
    1.70 -    (y, SOME context') => (y, context')
    1.71 -  | (_, NONE) => error "Lost context in ML");
    1.72 -
    1.73 -fun save f x = setmp (get_context ()) f x;
    1.74 -
    1.75 -
    1.76 -(* map context *)
    1.77 -
    1.78 -nonfix >>;
    1.79 -fun >> f = set_context (SOME (map_theory f (the_generic_context ())));
    1.80 -
    1.81 -
    1.82 -(* use ML text *)
    1.83 -
    1.84 -fun use_output verbose txt =
    1.85 -  Output.ML_errors (use_text Output.ml_output verbose) (Symbol.escape txt);
    1.86 -
    1.87 -fun use_mltext txt verbose opt_context = setmp opt_context (fn () => use_output verbose txt) ();
    1.88 -fun use_mltext_update txt verbose context = #2 (pass_context context (use_output verbose) txt);
    1.89 -
    1.90 -fun use_context txt = use_mltext_update
    1.91 -    ("Context.set_context (SOME ((" ^ txt ^ ") (Context.the_generic_context ())));") false;
    1.92 -
    1.93 -fun use_let bind body txt =
    1.94 -  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
    1.95 -
    1.96 -
    1.97 -(* delayed theory setup *)
    1.98 +(** delayed theory setup **)
    1.99  
   1.100  local
   1.101    val setup_fn = ref (I: theory -> theory);