author  wenzelm 
Fri, 17 Sep 2010 20:18:27 +0200  
changeset 39507  839873937ddd 
parent 39440  4c2547af5909 
child 39508  dfacdb01e1ec 
permissions  rwrr 
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 
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset

13 
val reported_text: Proof.context > Position.T > Markup.T > string > string 
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset

14 
val report_text: Proof.context > Position.T > Markup.T > string > unit 
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset

15 
val report: Proof.context > Position.T > Markup.T > unit 
28405  16 
end; 
17 

33383  18 
structure Context_Position: CONTEXT_POSITION = 
28405  19 
struct 
20 

33519  21 
structure Data = Proof_Data 
28405  22 
( 
23 
type T = bool; 

24 
fun init _ = true; 

25 
); 

26 

27 
val is_visible = Data.get; 

28 
val set_visible = Data.put; 

29 
val restore_visible = set_visible o is_visible; 

30 

38831
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38481
diff
changeset

31 
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

32 

39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset

33 
fun reported_text ctxt pos markup txt = 
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset

34 
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

35 

39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset

36 
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

37 
fun report ctxt pos markup = report_text ctxt pos markup ""; 
28405  38 

39 
end; 