37 structure Context_Position: CONTEXT_POSITION = |
37 structure Context_Position: CONTEXT_POSITION = |
38 struct |
38 struct |
39 |
39 |
40 (* visible context *) |
40 (* visible context *) |
41 |
41 |
42 structure Data = Generic_Data |
42 val really = Config.declare_bool ("really", Position.none) (K true); |
43 ( |
43 val visible = Config.declare_bool ("visible", Position.none) (K true); |
44 type T = bool option * bool option; (*really, visible*) |
|
45 val empty: T = (NONE, NONE); |
|
46 val extend = I; |
|
47 fun merge ((a, b), (a', b')) : T = (merge_options (a, a'), merge_options (b, b')); |
|
48 ); |
|
49 |
44 |
50 val is_visible_generic = the_default true o snd o Data.get; |
45 val is_visible_generic = Config.apply_generic visible; |
51 val is_visible = is_visible_generic o Context.Proof; |
46 val is_visible = Config.apply visible; |
52 val is_visible_global = is_visible_generic o Context.Theory; |
47 val is_visible_global = Config.apply_global visible; |
53 |
48 |
54 val set_visible_generic = Data.map o apsnd o K o SOME; |
49 val set_visible_generic = Config.put_generic visible; |
55 val set_visible = Context.proof_map o Data.map o apsnd o K o SOME; |
50 val set_visible = Config.put visible; |
56 val set_visible_global = Context.theory_map o Data.map o apsnd o K o SOME; |
51 val set_visible_global = Config.put_global visible; |
57 |
52 |
58 val is_really = the_default true o fst o Data.get o Context.Proof; |
53 val is_really = Config.apply really; |
59 fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt; |
54 fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt; |
60 val not_really = Context.proof_map (Data.map (apfst (K (SOME false)))); |
55 val not_really = Config.put really false; |
61 |
56 |
62 val restore_visible_generic = Data.put o Data.get; |
57 fun restore_visible_generic context = |
63 val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof; |
58 Config.restore_generic really context #> |
64 val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory; |
59 Config.restore_generic visible context; |
|
60 |
|
61 val restore_visible = Context.proof_map o restore_visible_generic o Context.Proof; |
|
62 val restore_visible_global = Context.theory_map o restore_visible_generic o Context.Theory; |
65 |
63 |
66 |
64 |
67 (* PIDE reports *) |
65 (* PIDE reports *) |
68 |
66 |
69 fun pide_reports () = Options.default_bool "pide_reports"; |
67 fun pide_reports () = Options.default_bool "pide_reports"; |