src/Pure/context_position.ML
changeset 28409 a1feb819b0a2
parent 28405 000dee6d5d80
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/context_position.ML	Mon Sep 29 14:59:02 2008 +0200
     1.2 +++ b/src/Pure/context_position.ML	Mon Sep 29 21:26:26 2008 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Context position visibility.
     1.8 +Context position visibility flag.
     1.9  *)
    1.10  
    1.11  signature CONTEXT_POSITION =
    1.12 @@ -10,7 +10,7 @@
    1.13    val is_visible: Proof.context -> bool
    1.14    val set_visible: bool -> Proof.context -> Proof.context
    1.15    val restore_visible: Proof.context -> Proof.context -> Proof.context
    1.16 -  val report: Proof.context -> Markup.T -> Position.T -> unit
    1.17 +  val report_visible: Proof.context -> Markup.T -> Position.T -> unit
    1.18  end;
    1.19  
    1.20  structure ContextPosition: CONTEXT_POSITION =
    1.21 @@ -26,7 +26,7 @@
    1.22  val set_visible = Data.put;
    1.23  val restore_visible = set_visible o is_visible;
    1.24  
    1.25 -fun report ctxt markup pos =
    1.26 +fun report_visible ctxt markup pos =
    1.27    if is_visible ctxt then Position.report markup pos else ();
    1.28  
    1.29  end;