equal
deleted
inserted
replaced
8 sig |
8 sig |
9 val is_visible: Proof.context -> bool |
9 val is_visible: Proof.context -> bool |
10 val set_visible: bool -> Proof.context -> Proof.context |
10 val set_visible: bool -> Proof.context -> Proof.context |
11 val restore_visible: Proof.context -> Proof.context -> Proof.context |
11 val restore_visible: Proof.context -> Proof.context -> Proof.context |
12 val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit |
12 val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit |
|
13 val is_visible_proof: Context.generic -> bool |
13 val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit |
14 val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit |
14 val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string |
15 val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string |
15 val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit |
16 val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit |
16 val report: Proof.context -> Position.T -> Markup.T -> unit |
17 val report: Proof.context -> Position.T -> Markup.T -> unit |
17 val reports: Proof.context -> Position.report list -> unit |
18 val reports: Proof.context -> Position.report list -> unit |
25 val set_visible = Config.put visible; |
26 val set_visible = Config.put visible; |
26 val restore_visible = set_visible o is_visible; |
27 val restore_visible = set_visible o is_visible; |
27 |
28 |
28 fun if_visible ctxt f x = if is_visible ctxt then f x else (); |
29 fun if_visible ctxt f x = if is_visible ctxt then f x else (); |
29 |
30 |
30 fun if_visible_proof (Context.Proof ctxt) f x = if_visible ctxt f x |
31 fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt |
31 | if_visible_proof _ _ _ = (); |
32 | is_visible_proof _ = false; |
|
33 |
|
34 fun if_visible_proof context f x = if is_visible_proof context then f x else (); |
32 |
35 |
33 fun reported_text ctxt pos markup txt = |
36 fun reported_text ctxt pos markup txt = |
34 if is_visible ctxt then Position.reported_text pos markup txt else ""; |
37 if is_visible ctxt then Position.reported_text pos markup txt else ""; |
35 |
38 |
36 fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt); |
39 fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt); |