src/Pure/context_position.ML
author wenzelm
Mon Sep 29 21:26:26 2008 +0200 (2008-09-29)
changeset 28409 a1feb819b0a2
parent 28405 000dee6d5d80
child 29606 fedb8be05f24
permissions -rw-r--r--
renamed report to report_visible;
tuned comments;
     1 (*  Title:      Pure/context_position.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Context position visibility flag.
     6 *)
     7 
     8 signature CONTEXT_POSITION =
     9 sig
    10   val is_visible: Proof.context -> bool
    11   val set_visible: bool -> Proof.context -> Proof.context
    12   val restore_visible: Proof.context -> Proof.context -> Proof.context
    13   val report_visible: Proof.context -> Markup.T -> Position.T -> unit
    14 end;
    15 
    16 structure ContextPosition: CONTEXT_POSITION =
    17 struct
    18 
    19 structure Data = ProofDataFun
    20 (
    21   type T = bool;
    22   fun init _ = true;
    23 );
    24 
    25 val is_visible = Data.get;
    26 val set_visible = Data.put;
    27 val restore_visible = set_visible o is_visible;
    28 
    29 fun report_visible ctxt markup pos =
    30   if is_visible ctxt then Position.report markup pos else ();
    31 
    32 end;