1(* Title: Pure/context_position.ML 2 Author: Makarius 3 4Context position visibility flag. 5*) 6 7signature CONTEXT_POSITION = 8sig 9 val is_visible_generic: Context.generic -> bool 10 val is_visible: Proof.context -> bool 11 val is_visible_global: theory -> bool 12 val set_visible_generic: bool -> Context.generic -> Context.generic 13 val set_visible: bool -> Proof.context -> Proof.context 14 val set_visible_global: bool -> theory -> theory 15 val is_really_visible: Proof.context -> bool 16 val not_really: Proof.context -> Proof.context 17 val restore_visible_generic: Context.generic -> Context.generic -> Context.generic 18 val restore_visible: Proof.context -> Proof.context -> Proof.context 19 val restore_visible_global: theory -> theory -> theory 20 val is_reported_generic: Context.generic -> Position.T -> bool 21 val is_reported: Proof.context -> Position.T -> bool 22 val report_generic: Context.generic -> Position.T -> Markup.T -> unit 23 val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string 24 val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit 25 val report: Proof.context -> Position.T -> Markup.T -> unit 26 val reports_text: Proof.context -> Position.report_text list -> unit 27 val reports: Proof.context -> Position.report list -> unit 28end; 29 30structure Context_Position: CONTEXT_POSITION = 31struct 32 33structure Data = Generic_Data 34( 35 type T = bool option * bool option; (*really, visible*) 36 val empty: T = (NONE, NONE); 37 val extend = I; 38 fun merge ((a, b), (a', b')) : T = (merge_options (a, a'), merge_options (b, b')); 39); 40 41val is_visible_generic = the_default true o snd o Data.get; 42val is_visible = is_visible_generic o Context.Proof; 43val is_visible_global = is_visible_generic o Context.Theory; 44 45val set_visible_generic = Data.map o apsnd o K o SOME; 46val set_visible = Context.proof_map o Data.map o apsnd o K o SOME; 47val set_visible_global = Context.theory_map o Data.map o apsnd o K o SOME; 48 49val is_really = the_default true o fst o Data.get o Context.Proof; 50fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt; 51val not_really = Context.proof_map (Data.map (apfst (K (SOME false)))); 52 53val restore_visible_generic = Data.put o Data.get; 54val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof; 55val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory; 56 57fun is_reported_generic context pos = is_visible_generic context andalso Position.is_reported pos; 58fun is_reported ctxt pos = is_visible ctxt andalso Position.is_reported pos; 59 60fun report_generic context pos markup = 61 if is_reported_generic context pos then 62 Output.report [Position.reported_text pos markup ""] 63 else (); 64 65fun reported_text ctxt pos markup txt = 66 if is_reported ctxt pos then Position.reported_text pos markup txt else ""; 67 68fun report_text ctxt pos markup txt = Output.report [reported_text ctxt pos markup txt]; 69fun report ctxt pos markup = report_text ctxt pos markup ""; 70 71fun reports_text ctxt reps = if is_visible ctxt then Position.reports_text reps else (); 72fun reports ctxt reps = if is_visible ctxt then Position.reports reps else (); 73 74end; 75