equal
deleted
inserted
replaced
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 is_visible_proof: Context.generic -> bool |
14 val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit |
14 val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit |
|
15 val report_generic: Context.generic -> Position.T -> Markup.T -> unit |
15 val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string |
16 val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string |
16 val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit |
17 val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit |
17 val report: Proof.context -> Position.T -> Markup.T -> unit |
18 val report: Proof.context -> Position.T -> Markup.T -> unit |
18 val reports: Proof.context -> Position.report list -> unit |
19 val reports: Proof.context -> Position.report list -> unit |
19 end; |
20 end; |
31 fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt |
32 fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt |
32 | is_visible_proof _ = false; |
33 | is_visible_proof _ = false; |
33 |
34 |
34 fun if_visible_proof context f x = if is_visible_proof context then f x else (); |
35 fun if_visible_proof context f x = if is_visible_proof context then f x else (); |
35 |
36 |
|
37 fun report_generic context pos markup = |
|
38 if Config.get_generic context visible then |
|
39 Output.report (Position.reported_text pos markup "") |
|
40 else (); |
|
41 |
36 fun reported_text ctxt pos markup txt = |
42 fun reported_text ctxt pos markup txt = |
37 if is_visible ctxt then Position.reported_text pos markup txt else ""; |
43 if is_visible ctxt then Position.reported_text pos markup txt else ""; |
38 |
44 |
39 fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt); |
45 fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt); |
40 fun report ctxt pos markup = report_text ctxt pos markup ""; |
46 fun report ctxt pos markup = report_text ctxt pos markup ""; |