equal
deleted
inserted
replaced
16 include BASIC_CONTEXT |
16 include BASIC_CONTEXT |
17 val get_context: unit -> theory option |
17 val get_context: unit -> theory option |
18 val set_context: theory option -> unit |
18 val set_context: theory option -> unit |
19 val reset_context: unit -> unit |
19 val reset_context: unit -> unit |
20 val setmp: theory option -> ('a -> 'b) -> 'a -> 'b |
20 val setmp: theory option -> ('a -> 'b) -> 'a -> 'b |
|
21 val fetch: theory option -> ('a -> 'b) -> 'a -> 'b * theory option |
|
22 val fetch_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory |
21 val save: ('a -> 'b) -> 'a -> 'b |
23 val save: ('a -> 'b) -> 'a -> 'b |
22 val >> : (theory -> theory) -> unit |
24 val >> : (theory -> theory) -> unit |
23 end; |
25 end; |
24 |
26 |
25 structure Context: CONTEXT = |
27 structure Context: CONTEXT = |
42 | _ => error "Unknown theory context"); |
44 | _ => error "Unknown theory context"); |
43 |
45 |
44 fun context thy = set_context (Some thy); |
46 fun context thy = set_context (Some thy); |
45 fun reset_context () = set_context None; |
47 fun reset_context () = set_context None; |
46 |
48 |
|
49 fun fetch opt_thy f x = |
|
50 setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x; |
|
51 |
|
52 fun fetch_theory thy f x = |
|
53 (case fetch (Some thy) f x of |
|
54 (y, Some thy') => (y, thy') |
|
55 | (_, None) => error "Missing ML theory context"); |
|
56 |
47 fun save f x = setmp (get_context ()) f x; |
57 fun save f x = setmp (get_context ()) f x; |
48 |
58 |
49 |
59 |
50 (* map context *) |
60 (* map context *) |
51 |
61 |