author | wenzelm |
Sun, 22 Jul 2012 12:26:41 +0200 | |
changeset 48423 | 0ccf143a2a69 |
parent 47813 | 18de60b8c906 |
child 48767 | 7f0c469cc796 |
permissions | -rw-r--r-- |
28405 | 1 |
(* Title: Pure/context_position.ML |
2 |
Author: Makarius |
|
3 |
||
28409 | 4 |
Context position visibility flag. |
28405 | 5 |
*) |
6 |
||
7 |
signature CONTEXT_POSITION = |
|
8 |
sig |
|
9 |
val is_visible: Proof.context -> bool |
|
10 |
val set_visible: bool -> Proof.context -> Proof.context |
|
11 |
val restore_visible: Proof.context -> Proof.context -> Proof.context |
|
38831
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38481
diff
changeset
|
12 |
val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit |
46874 | 13 |
val is_visible_proof: Context.generic -> bool |
41470
890b25753bf7
added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);
wenzelm
parents:
39508
diff
changeset
|
14 |
val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit |
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46874
diff
changeset
|
15 |
val report_generic: Context.generic -> Position.T -> Markup.T -> unit |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
16 |
val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
17 |
val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
18 |
val report: Proof.context -> Position.T -> Markup.T -> unit |
44736 | 19 |
val reports: Proof.context -> Position.report list -> unit |
28405 | 20 |
end; |
21 |
||
33383 | 22 |
structure Context_Position: CONTEXT_POSITION = |
28405 | 23 |
struct |
24 |
||
47813 | 25 |
structure Data = Generic_Data |
26 |
( |
|
27 |
type T = bool option; |
|
28 |
val empty: T = NONE; |
|
29 |
val extend = I; |
|
30 |
fun merge (x, y): T = if is_some x then x else y; |
|
31 |
); |
|
32 |
||
33 |
val is_visible_generic = the_default true o Data.get; |
|
34 |
val is_visible = is_visible_generic o Context.Proof; |
|
35 |
val set_visible = Context.proof_map o Data.put o SOME; |
|
28405 | 36 |
val restore_visible = set_visible o is_visible; |
37 |
||
38831
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38481
diff
changeset
|
38 |
fun if_visible ctxt f x = if is_visible ctxt then f x else (); |
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38481
diff
changeset
|
39 |
|
46874 | 40 |
fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt |
41 |
| is_visible_proof _ = false; |
|
42 |
||
43 |
fun if_visible_proof context f x = if is_visible_proof context then f x else (); |
|
41470
890b25753bf7
added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);
wenzelm
parents:
39508
diff
changeset
|
44 |
|
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46874
diff
changeset
|
45 |
fun report_generic context pos markup = |
47813 | 46 |
if is_visible_generic context then |
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46874
diff
changeset
|
47 |
Output.report (Position.reported_text pos markup "") |
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46874
diff
changeset
|
48 |
else (); |
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46874
diff
changeset
|
49 |
|
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
50 |
fun reported_text ctxt pos markup txt = |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
51 |
if is_visible ctxt then Position.reported_text pos markup txt else ""; |
38481
81ec258c4cd3
Output_Position.report_text -- markup with potential "arguments";
wenzelm
parents:
38237
diff
changeset
|
52 |
|
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
53 |
fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt); |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
54 |
fun report ctxt pos markup = report_text ctxt pos markup ""; |
28405 | 55 |
|
44736 | 56 |
fun reports ctxt reps = if is_visible ctxt then Position.reports reps else (); |
57 |
||
28405 | 58 |
end; |