# HG changeset patch
# User wenzelm
# Date 1222692083 -7200
# Node ID 000dee6d5d80af1c0cc35b8039396975b2a0e974
# Parent  b906dd1de8553af44904bb51db74931d73cf9b94
Context position visibility.

diff -r b906dd1de855 -r 000dee6d5d80 src/Pure/context_position.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/context_position.ML	Mon Sep 29 14:41:23 2008 +0200
@@ -0,0 +1,32 @@
+(*  Title:      Pure/context_position.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Context position visibility.
+*)
+
+signature CONTEXT_POSITION =
+sig
+  val is_visible: Proof.context -> bool
+  val set_visible: bool -> Proof.context -> Proof.context
+  val restore_visible: Proof.context -> Proof.context -> Proof.context
+  val report: Proof.context -> Markup.T -> Position.T -> unit
+end;
+
+structure ContextPosition: CONTEXT_POSITION =
+struct
+
+structure Data = ProofDataFun
+(
+  type T = bool;
+  fun init _ = true;
+);
+
+val is_visible = Data.get;
+val set_visible = Data.put;
+val restore_visible = set_visible o is_visible;
+
+fun report ctxt markup pos =
+  if is_visible ctxt then Position.report markup pos else ();
+
+end;