# HG changeset patch
# User wenzelm
# Date 1335555884 -7200
# Node ID 18de60b8c9069285f279c51ebfda23fffd0468cb
# Parent  4d8cbea248b025a449f6346e1965fa23ac2374c4
made Context_Position independent from Config;

diff -r 4d8cbea248b0 -r 18de60b8c906 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Apr 27 21:24:30 2012 +0200
+++ b/src/Pure/ROOT.ML	Fri Apr 27 21:44:44 2012 +0200
@@ -101,8 +101,8 @@
 use "name.ML";
 use "term.ML";
 use "context.ML";
+use "context_position.ML";
 use "config.ML";
-use "context_position.ML";
 
 
 (* inner syntax *)
diff -r 4d8cbea248b0 -r 18de60b8c906 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Fri Apr 27 21:24:30 2012 +0200
+++ b/src/Pure/context_position.ML	Fri Apr 27 21:44:44 2012 +0200
@@ -22,9 +22,17 @@
 structure Context_Position: CONTEXT_POSITION =
 struct
 
-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;
+structure Data = Generic_Data
+(
+  type T = bool option;
+  val empty: T = NONE;
+  val extend = I;
+  fun merge (x, y): T = if is_some x then x else y;
+);
+
+val is_visible_generic = the_default true o Data.get;
+val is_visible = is_visible_generic o Context.Proof;
+val set_visible = Context.proof_map o Data.put o SOME;
 val restore_visible = set_visible o is_visible;
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
@@ -35,7 +43,7 @@
 fun if_visible_proof context f x = if is_visible_proof context then f x else ();
 
 fun report_generic context pos markup =
-  if Config.get_generic context visible then
+  if is_visible_generic context then
     Output.report (Position.reported_text pos markup "")
   else ();