src/Pure/context_position.ML
changeset 39508 dfacdb01e1ec
parent 39507 839873937ddd
child 41470 890b25753bf7
--- a/src/Pure/context_position.ML	Fri Sep 17 20:18:27 2010 +0200
+++ b/src/Pure/context_position.ML	Fri Sep 17 20:42:26 2010 +0200
@@ -18,14 +18,9 @@
 structure Context_Position: CONTEXT_POSITION =
 struct
 
-structure Data = Proof_Data
-(
-  type T = bool;
-  fun init _ = true;
-);
-
-val is_visible = Data.get;
-val set_visible = Data.put;
+val visible = Config.bool (Config.declare "Context_Position.visible" (K (Config.Bool true)));
+fun is_visible ctxt = Config.get ctxt visible;
+val set_visible = Config.put visible;
 val restore_visible = set_visible o is_visible;
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();