made Context_Position independent from Config;
authorwenzelm
Fri Apr 27 21:44:44 2012 +0200 (2012-04-27)
changeset 4781318de60b8c906
parent 47809 4d8cbea248b0
child 47814 53668571d300
made Context_Position independent from Config;
src/Pure/ROOT.ML
src/Pure/context_position.ML
     1.1 --- a/src/Pure/ROOT.ML	Fri Apr 27 21:24:30 2012 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Apr 27 21:44:44 2012 +0200
     1.3 @@ -101,8 +101,8 @@
     1.4  use "name.ML";
     1.5  use "term.ML";
     1.6  use "context.ML";
     1.7 +use "context_position.ML";
     1.8  use "config.ML";
     1.9 -use "context_position.ML";
    1.10  
    1.11  
    1.12  (* inner syntax *)
     2.1 --- a/src/Pure/context_position.ML	Fri Apr 27 21:24:30 2012 +0200
     2.2 +++ b/src/Pure/context_position.ML	Fri Apr 27 21:44:44 2012 +0200
     2.3 @@ -22,9 +22,17 @@
     2.4  structure Context_Position: CONTEXT_POSITION =
     2.5  struct
     2.6  
     2.7 -val visible = Config.bool (Config.declare "Context_Position.visible" (K (Config.Bool true)));
     2.8 -fun is_visible ctxt = Config.get ctxt visible;
     2.9 -val set_visible = Config.put visible;
    2.10 +structure Data = Generic_Data
    2.11 +(
    2.12 +  type T = bool option;
    2.13 +  val empty: T = NONE;
    2.14 +  val extend = I;
    2.15 +  fun merge (x, y): T = if is_some x then x else y;
    2.16 +);
    2.17 +
    2.18 +val is_visible_generic = the_default true o Data.get;
    2.19 +val is_visible = is_visible_generic o Context.Proof;
    2.20 +val set_visible = Context.proof_map o Data.put o SOME;
    2.21  val restore_visible = set_visible o is_visible;
    2.22  
    2.23  fun if_visible ctxt f x = if is_visible ctxt then f x else ();
    2.24 @@ -35,7 +43,7 @@
    2.25  fun if_visible_proof context f x = if is_visible_proof context then f x else ();
    2.26  
    2.27  fun report_generic context pos markup =
    2.28 -  if Config.get_generic context visible then
    2.29 +  if is_visible_generic context then
    2.30      Output.report (Position.reported_text pos markup "")
    2.31    else ();
    2.32