author | wenzelm |
Sun, 22 Aug 2010 19:33:01 +0200 | |
changeset 38578 | 1ebc6b76e5ff |
parent 38481 | 81ec258c4cd3 |
child 38831 | 4933a3dfd745 |
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 |
|
38481
81ec258c4cd3
Output_Position.report_text -- markup with potential "arguments";
wenzelm
parents:
38237
diff
changeset
|
12 |
val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit |
38237
8b0383334031
prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
wenzelm
parents:
33519
diff
changeset
|
13 |
val report: Proof.context -> Markup.T -> Position.T -> unit |
28405 | 14 |
end; |
15 |
||
33383 | 16 |
structure Context_Position: CONTEXT_POSITION = |
28405 | 17 |
struct |
18 |
||
33519 | 19 |
structure Data = Proof_Data |
28405 | 20 |
( |
21 |
type T = bool; |
|
22 |
fun init _ = true; |
|
23 |
); |
|
24 |
||
25 |
val is_visible = Data.get; |
|
26 |
val set_visible = Data.put; |
|
27 |
val restore_visible = set_visible o is_visible; |
|
28 |
||
38481
81ec258c4cd3
Output_Position.report_text -- markup with potential "arguments";
wenzelm
parents:
38237
diff
changeset
|
29 |
fun report_text ctxt markup pos txt = |
81ec258c4cd3
Output_Position.report_text -- markup with potential "arguments";
wenzelm
parents:
38237
diff
changeset
|
30 |
if is_visible ctxt then Position.report_text markup pos txt else (); |
81ec258c4cd3
Output_Position.report_text -- markup with potential "arguments";
wenzelm
parents:
38237
diff
changeset
|
31 |
|
81ec258c4cd3
Output_Position.report_text -- markup with potential "arguments";
wenzelm
parents:
38237
diff
changeset
|
32 |
fun report ctxt markup pos = report_text ctxt markup pos ""; |
28405 | 33 |
|
34 |
end; |