author | Walther Neuper <walther.neuper@jku.at> |
Thu, 17 Dec 2020 09:10:30 +0100 | |
changeset 60134 | 85ce6e27e130 |
parent 60133 | 83003c700845 |
child 60139 | c3cb65678c47 |
permissions | -rw-r--r-- |
wenzelm@28405 | 1 |
(* Title: Pure/context_position.ML |
wenzelm@28405 | 2 |
Author: Makarius |
wenzelm@28405 | 3 |
|
wenzelm@28409 | 4 |
Context position visibility flag. |
wenzelm@28405 | 5 |
*) |
wenzelm@28405 | 6 |
|
wenzelm@28405 | 7 |
signature CONTEXT_POSITION = |
wenzelm@28405 | 8 |
sig |
wenzelm@57014 | 9 |
val is_visible_generic: Context.generic -> bool |
wenzelm@28405 | 10 |
val is_visible: Proof.context -> bool |
wenzelm@53837 | 11 |
val is_visible_global: theory -> bool |
wneuper@59324 | 12 |
val set_visible_generic: bool -> Context.generic -> Context.generic |
wenzelm@28405 | 13 |
val set_visible: bool -> Proof.context -> Proof.context |
wenzelm@53837 | 14 |
val set_visible_global: bool -> theory -> theory |
wenzelm@59074 | 15 |
val is_really_visible: Proof.context -> bool |
wenzelm@59074 | 16 |
val not_really: Proof.context -> Proof.context |
wneuper@59324 | 17 |
val restore_visible_generic: Context.generic -> Context.generic -> Context.generic |
wenzelm@28405 | 18 |
val restore_visible: Proof.context -> Proof.context -> Proof.context |
wenzelm@53837 | 19 |
val restore_visible_global: theory -> theory -> theory |
wenzelm@57265 | 20 |
val is_reported_generic: Context.generic -> Position.T -> bool |
wenzelm@57265 | 21 |
val is_reported: Proof.context -> Position.T -> bool |
wenzelm@47876 | 22 |
val report_generic: Context.generic -> Position.T -> Markup.T -> unit |
wenzelm@39776 | 23 |
val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string |
wenzelm@39776 | 24 |
val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit |
wenzelm@39776 | 25 |
val report: Proof.context -> Position.T -> Markup.T -> unit |
wenzelm@49782 | 26 |
val reports_text: Proof.context -> Position.report_text list -> unit |
wenzelm@45627 | 27 |
val reports: Proof.context -> Position.report list -> unit |
wenzelm@28405 | 28 |
end; |
wenzelm@28405 | 29 |
|
wenzelm@33383 | 30 |
structure Context_Position: CONTEXT_POSITION = |
wenzelm@28405 | 31 |
struct |
wenzelm@28405 | 32 |
|
wenzelm@48684 | 33 |
structure Data = Generic_Data |
wenzelm@48684 | 34 |
( |
wenzelm@59074 | 35 |
type T = bool option * bool option; (*really, visible*) |
wenzelm@59074 | 36 |
val empty: T = (NONE, NONE); |
wenzelm@48684 | 37 |
val extend = I; |
wenzelm@59074 | 38 |
fun merge ((a, b), (a', b')) : T = (merge_options (a, a'), merge_options (b, b')); |
wenzelm@48684 | 39 |
); |
wenzelm@48684 | 40 |
|
wenzelm@59074 | 41 |
val is_visible_generic = the_default true o snd o Data.get; |
wenzelm@48684 | 42 |
val is_visible = is_visible_generic o Context.Proof; |
wenzelm@53837 | 43 |
val is_visible_global = is_visible_generic o Context.Theory; |
wenzelm@28405 | 44 |
|
wneuper@59324 | 45 |
val set_visible_generic = Data.map o apsnd o K o SOME; |
wenzelm@59074 | 46 |
val set_visible = Context.proof_map o Data.map o apsnd o K o SOME; |
wenzelm@59074 | 47 |
val set_visible_global = Context.theory_map o Data.map o apsnd o K o SOME; |
wenzelm@53837 | 48 |
|
wenzelm@59074 | 49 |
val is_really = the_default true o fst o Data.get o Context.Proof; |
wenzelm@59074 | 50 |
fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt; |
wenzelm@59074 | 51 |
val not_really = Context.proof_map (Data.map (apfst (K (SOME false)))); |
wenzelm@59074 | 52 |
|
wneuper@59324 | 53 |
val restore_visible_generic = Data.put o Data.get; |
wenzelm@59074 | 54 |
val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof; |
wenzelm@59074 | 55 |
val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory; |
wenzelm@39077 | 56 |
|
wenzelm@57265 | 57 |
fun is_reported_generic context pos = is_visible_generic context andalso Position.is_reported pos; |
wenzelm@57265 | 58 |
fun is_reported ctxt pos = is_visible ctxt andalso Position.is_reported pos; |
wenzelm@57265 | 59 |
|
wenzelm@47876 | 60 |
fun report_generic context pos markup = |
wenzelm@57265 | 61 |
if is_reported_generic context pos then |
walther@60133 | 62 |
((** )@{print} {a = "### Context_Position.report_generic"};( *..NOT yet available*) |
walther@60134 | 63 |
(**) writeln "### Context_Position.report_generic";(**) |
walther@60133 | 64 |
Output.report [Position.reported_text pos markup ""]) |
wenzelm@47876 | 65 |
else (); |
wenzelm@47876 | 66 |
|
wenzelm@39776 | 67 |
fun reported_text ctxt pos markup txt = |
wenzelm@57265 | 68 |
if is_reported ctxt pos then Position.reported_text pos markup txt else ""; |
wenzelm@38799 | 69 |
|
wenzelm@57675 | 70 |
fun report_text ctxt pos markup txt = Output.report [reported_text ctxt pos markup txt]; |
wenzelm@39776 | 71 |
fun report ctxt pos markup = report_text ctxt pos markup ""; |
wenzelm@28405 | 72 |
|
wenzelm@49782 | 73 |
fun reports_text ctxt reps = if is_visible ctxt then Position.reports_text reps else (); |
wenzelm@45627 | 74 |
fun reports ctxt reps = if is_visible ctxt then Position.reports reps else (); |
wenzelm@45627 | 75 |
|
wenzelm@28405 | 76 |
end; |