src/Pure/context_position.ML
changeset 39508 dfacdb01e1ec
parent 39507 839873937ddd
child 41470 890b25753bf7
equal deleted inserted replaced
39507:839873937ddd 39508:dfacdb01e1ec
    16 end;
    16 end;
    17 
    17 
    18 structure Context_Position: CONTEXT_POSITION =
    18 structure Context_Position: CONTEXT_POSITION =
    19 struct
    19 struct
    20 
    20 
    21 structure Data = Proof_Data
    21 val visible = Config.bool (Config.declare "Context_Position.visible" (K (Config.Bool true)));
    22 (
    22 fun is_visible ctxt = Config.get ctxt visible;
    23   type T = bool;
    23 val set_visible = Config.put visible;
    24   fun init _ = true;
       
    25 );
       
    26 
       
    27 val is_visible = Data.get;
       
    28 val set_visible = Data.put;
       
    29 val restore_visible = set_visible o is_visible;
    24 val restore_visible = set_visible o is_visible;
    30 
    25 
    31 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
    26 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
    32 
    27 
    33 fun reported_text ctxt pos markup txt =
    28 fun reported_text ctxt pos markup txt =