4338
|
1 |
(* Title: Pure/Thy/context.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
|
5 |
Global contexts: session and theory.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature CONTEXT =
|
|
9 |
sig
|
|
10 |
val get_session: unit -> string list
|
|
11 |
val add_session: string -> unit
|
|
12 |
val reset_session: unit -> unit
|
|
13 |
val get_context: unit -> theory
|
|
14 |
val context: theory -> unit
|
|
15 |
end;
|
|
16 |
|
|
17 |
structure Context: CONTEXT =
|
|
18 |
struct
|
|
19 |
|
|
20 |
|
|
21 |
(* session *)
|
|
22 |
|
|
23 |
val current_session = ref ([]: string list);
|
|
24 |
|
|
25 |
fun get_session () = ! current_session;
|
|
26 |
fun add_session s = current_session := ! current_session @ [s];
|
|
27 |
fun reset_session () = current_session := [];
|
|
28 |
|
|
29 |
|
|
30 |
(* theory context *)
|
|
31 |
|
|
32 |
val current_theory = ref ProtoPure.thy;
|
|
33 |
|
|
34 |
fun context thy = current_theory := thy;
|
|
35 |
fun get_context () = ! current_theory;
|
|
36 |
|
|
37 |
|
|
38 |
end;
|
|
39 |
|
|
40 |
open Context;
|