ML context: full generic context, tuned signature;
authorwenzelm
Fri Jan 19 13:09:32 2007 +0100 (2007-01-19)
changeset 22085c138cfd500f7
parent 22084 2fef69700f50
child 22086 cf6019fece63
ML context: full generic context, tuned signature;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Fri Jan 19 13:09:31 2007 +0100
     1.2 +++ b/src/Pure/context.ML	Fri Jan 19 13:09:32 2007 +0100
     1.3 @@ -12,7 +12,6 @@
     1.4    type theory
     1.5    type theory_ref
     1.6    exception THEORY of string * theory list
     1.7 -  val context: theory -> unit
     1.8    val the_context: unit -> theory
     1.9  end;
    1.10  
    1.11 @@ -49,20 +48,6 @@
    1.12    val theory_data_of: theory -> string list
    1.13    val pre_pure_thy: theory
    1.14    val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
    1.15 -  (*ML theory context*)
    1.16 -  val get_context: unit -> theory option
    1.17 -  val set_context: theory option -> unit
    1.18 -  val reset_context: unit -> unit
    1.19 -  val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
    1.20 -  val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
    1.21 -  val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
    1.22 -  val save: ('a -> 'b) -> 'a -> 'b
    1.23 -  val >> : (theory -> theory) -> unit
    1.24 -  val use_mltext: string -> bool -> theory option -> unit
    1.25 -  val use_mltext_theory: string -> bool -> theory -> theory
    1.26 -  val use_let: string -> string -> string -> theory -> theory
    1.27 -  val add_setup: (theory -> theory) -> unit
    1.28 -  val setup: unit -> theory -> theory
    1.29    (*proof context*)
    1.30    type proof
    1.31    val theory_of_proof: proof -> theory
    1.32 @@ -82,6 +67,21 @@
    1.33    val proof_map: (generic -> generic) -> proof -> proof
    1.34    val theory_of: generic -> theory   (*total*)
    1.35    val proof_of: generic -> proof     (*total*)
    1.36 +  (*ML context*)
    1.37 +  val get_context: unit -> generic option
    1.38 +  val set_context: generic option -> unit
    1.39 +  val setmp: generic option -> ('a -> 'b) -> 'a -> 'b
    1.40 +  val the_generic_context: unit -> generic
    1.41 +  val the_local_context: unit -> proof
    1.42 +  val pass: generic option -> ('a -> 'b) -> 'a -> 'b * generic option
    1.43 +  val pass_context: generic -> ('a -> 'b) -> 'a -> 'b * generic
    1.44 +  val save: ('a -> 'b) -> 'a -> 'b
    1.45 +  val >> : (theory -> theory) -> unit
    1.46 +  val use_mltext: string -> bool -> generic option -> unit
    1.47 +  val use_mltext_update: string -> bool -> generic -> generic
    1.48 +  val use_let: string -> string -> string -> generic -> generic
    1.49 +  val add_setup: (theory -> theory) -> unit
    1.50 +  val setup: unit -> theory -> theory
    1.51  end;
    1.52  
    1.53  signature PRIVATE_CONTEXT =
    1.54 @@ -447,66 +447,6 @@
    1.55  
    1.56  
    1.57  
    1.58 -(*** ML theory context ***)
    1.59 -
    1.60 -local
    1.61 -  val current_theory = ref (NONE: theory option);
    1.62 -in
    1.63 -  fun get_context () = ! current_theory;
    1.64 -  fun set_context opt_thy = current_theory := opt_thy;
    1.65 -  fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
    1.66 -end;
    1.67 -
    1.68 -fun the_context () =
    1.69 -  (case get_context () of
    1.70 -    SOME thy => thy
    1.71 -  | _ => error "Unknown theory context");
    1.72 -
    1.73 -fun context thy = set_context (SOME thy);
    1.74 -fun reset_context () = set_context NONE;
    1.75 -
    1.76 -fun pass opt_thy f x =
    1.77 -  setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
    1.78 -
    1.79 -fun pass_theory thy f x =
    1.80 -  (case pass (SOME thy) f x of
    1.81 -    (y, SOME thy') => (y, thy')
    1.82 -  | (_, NONE) => error "Lost theory context in ML");
    1.83 -
    1.84 -fun save f x = setmp (get_context ()) f x;
    1.85 -
    1.86 -
    1.87 -(* map context *)
    1.88 -
    1.89 -nonfix >>;
    1.90 -fun >> f = set_context (SOME (f (the_context ())));
    1.91 -
    1.92 -
    1.93 -(* use ML text *)
    1.94 -
    1.95 -fun use_output verbose txt =
    1.96 -  Output.ML_errors (use_text Output.ml_output verbose) (Symbol.escape txt);
    1.97 -
    1.98 -fun use_mltext txt verbose opt_thy = setmp opt_thy (fn () => use_output verbose txt) ();
    1.99 -fun use_mltext_theory txt verbose thy = #2 (pass_theory thy (use_output verbose) txt);
   1.100 -
   1.101 -fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
   1.102 -
   1.103 -fun use_let bind body txt =
   1.104 -  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   1.105 -
   1.106 -
   1.107 -(* delayed theory setup *)
   1.108 -
   1.109 -local
   1.110 -  val setup_fn = ref (I: theory -> theory);
   1.111 -in
   1.112 -  fun add_setup f = setup_fn := (! setup_fn #> f);
   1.113 -  fun setup () = let val f = ! setup_fn in setup_fn := I; f end;
   1.114 -end;
   1.115 -
   1.116 -
   1.117 -
   1.118  (*** proof context ***)
   1.119  
   1.120  (* datatype proof *)
   1.121 @@ -601,6 +541,67 @@
   1.122  val theory_of = cases I theory_of_proof;
   1.123  val proof_of = cases init_proof I;
   1.124  
   1.125 +
   1.126 +
   1.127 +(*** ML context ***)
   1.128 +
   1.129 +local
   1.130 +  val current_context = ref (NONE: generic option);
   1.131 +in
   1.132 +  fun get_context () = ! current_context;
   1.133 +  fun set_context opt_context = current_context := opt_context;
   1.134 +  fun setmp opt_context f x = Library.setmp current_context opt_context f x;
   1.135 +end;
   1.136 +
   1.137 +fun the_generic_context () =
   1.138 +  (case get_context () of
   1.139 +    SOME context => context
   1.140 +  | _ => error "Unknown context");
   1.141 +
   1.142 +val the_context = theory_of o the_generic_context;
   1.143 +val the_local_context = the_proof o the_generic_context;
   1.144 +
   1.145 +fun pass opt_context f x =
   1.146 +  setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x;
   1.147 +
   1.148 +fun pass_context context f x =
   1.149 +  (case pass (SOME context) f x of
   1.150 +    (y, SOME context') => (y, context')
   1.151 +  | (_, NONE) => error "Lost context in ML");
   1.152 +
   1.153 +fun save f x = setmp (get_context ()) f x;
   1.154 +
   1.155 +
   1.156 +(* map context *)
   1.157 +
   1.158 +nonfix >>;
   1.159 +fun >> f = set_context (SOME (map_theory f (the_generic_context ())));
   1.160 +
   1.161 +
   1.162 +(* use ML text *)
   1.163 +
   1.164 +fun use_output verbose txt =
   1.165 +  Output.ML_errors (use_text Output.ml_output verbose) (Symbol.escape txt);
   1.166 +
   1.167 +fun use_mltext txt verbose opt_context = setmp opt_context (fn () => use_output verbose txt) ();
   1.168 +fun use_mltext_update txt verbose context = #2 (pass_context context (use_output verbose) txt);
   1.169 +
   1.170 +fun use_context txt = use_mltext_update
   1.171 +    ("Context.set_context (SOME ((" ^ txt ^ ") (Context.the_generic_context ())));") false;
   1.172 +
   1.173 +fun use_let bind body txt =
   1.174 +  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   1.175 +
   1.176 +
   1.177 +(* delayed theory setup *)
   1.178 +
   1.179 +local
   1.180 +  val setup_fn = ref (I: theory -> theory);
   1.181 +in
   1.182 +  fun add_setup f = setup_fn := (! setup_fn #> f);
   1.183 +  fun setup () = let val f = ! setup_fn in setup_fn := I; f end;
   1.184 +end;
   1.185 +
   1.186  end;
   1.187  
   1.188  structure BasicContext: BASIC_CONTEXT = Context;