diff -r e26aac53723d -r a1feb819b0a2 src/Pure/context_position.ML --- a/src/Pure/context_position.ML Mon Sep 29 14:59:02 2008 +0200 +++ b/src/Pure/context_position.ML Mon Sep 29 21:26:26 2008 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Author: Makarius -Context position visibility. +Context position visibility flag. *) signature CONTEXT_POSITION = @@ -10,7 +10,7 @@ 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 + val report_visible: Proof.context -> Markup.T -> Position.T -> unit end; structure ContextPosition: CONTEXT_POSITION = @@ -26,7 +26,7 @@ val set_visible = Data.put; val restore_visible = set_visible o is_visible; -fun report ctxt markup pos = +fun report_visible ctxt markup pos = if is_visible ctxt then Position.report markup pos else (); end;