turned show_hyps and show_tags into proper configuration option;
authorwenzelm
Mon Sep 06 22:58:06 2010 +0200 (2010-09-06)
changeset 3916619efc2af3e6c
parent 39165 e790a5560834
child 39167 803431dcc7fb
child 39197 35fcab3da1b7
child 39198 f967a16dfcdd
turned show_hyps and show_tags into proper configuration option;
src/Pure/Isar/attrib.ML
src/Pure/Isar/element.ML
src/Pure/display.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Sep 06 22:31:54 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Sep 06 22:58:06 2010 +0200
     1.3 @@ -402,6 +402,8 @@
     1.4    register_config Goal_Display.goals_limit_raw #>
     1.5    register_config Goal_Display.show_main_goal_raw #>
     1.6    register_config Goal_Display.show_consts_raw #>
     1.7 +  register_config Display.show_hyps_raw #>
     1.8 +  register_config Display.show_tags_raw #>
     1.9    register_config Unify.trace_bound_raw #>
    1.10    register_config Unify.search_bound_raw #>
    1.11    register_config Unify.trace_simp_raw #>
     2.1 --- a/src/Pure/Isar/element.ML	Mon Sep 06 22:31:54 2010 +0200
     2.2 +++ b/src/Pure/Isar/element.ML	Mon Sep 06 22:58:06 2010 +0200
     2.3 @@ -323,7 +323,7 @@
     2.4  fun pretty_witness ctxt witn =
     2.5    let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
     2.6      Pretty.block (prt_term (witness_prop witn) ::
     2.7 -      (if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
     2.8 +      (if Config.get ctxt show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
     2.9           (map prt_term (witness_hyps witn))] else []))
    2.10    end;
    2.11  
     3.1 --- a/src/Pure/display.ML	Mon Sep 06 22:31:54 2010 +0200
     3.2 +++ b/src/Pure/display.ML	Mon Sep 06 22:58:06 2010 +0200
     3.3 @@ -9,8 +9,10 @@
     3.4  sig
     3.5    val show_consts_default: bool Unsynchronized.ref
     3.6    val show_consts: bool Config.T
     3.7 -  val show_hyps: bool Unsynchronized.ref
     3.8 -  val show_tags: bool Unsynchronized.ref
     3.9 +  val show_hyps_raw: Config.raw
    3.10 +  val show_hyps: bool Config.T
    3.11 +  val show_tags_raw: Config.raw
    3.12 +  val show_tags: bool Config.T
    3.13  end;
    3.14  
    3.15  signature DISPLAY =
    3.16 @@ -39,8 +41,11 @@
    3.17  val show_consts_default = Goal_Display.show_consts_default;
    3.18  val show_consts = Goal_Display.show_consts;
    3.19  
    3.20 -val show_hyps = Unsynchronized.ref false;    (*false: print meta-hypotheses as dots*)
    3.21 -val show_tags = Unsynchronized.ref false;    (*false: suppress tags*)
    3.22 +val show_hyps_raw = Config.declare "show_hyps" (fn _ => Config.Bool false);
    3.23 +val show_hyps = Config.bool show_hyps_raw;
    3.24 +
    3.25 +val show_tags_raw = Config.declare "show_tags" (fn _ => Config.Bool false);
    3.26 +val show_tags = Config.bool show_tags_raw;
    3.27  
    3.28  
    3.29  
    3.30 @@ -49,11 +54,11 @@
    3.31  fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
    3.32  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    3.33  
    3.34 -fun display_status false _ = ""
    3.35 -  | display_status true th =
    3.36 +fun display_status _ false _ = ""
    3.37 +  | display_status show_hyps true th =
    3.38        let
    3.39          val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    3.40 -        val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
    3.41 +        val oracle = oracle0 andalso (not (! quick_and_dirty) orelse show_hyps);
    3.42        in
    3.43          if failed then "!!"
    3.44          else if oracle andalso unfinished then "!?"
    3.45 @@ -64,6 +69,9 @@
    3.46  
    3.47  fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th =
    3.48    let
    3.49 +    val show_tags = Config.get ctxt show_tags;
    3.50 +    val show_hyps = Config.get ctxt show_hyps;
    3.51 +
    3.52      val th = Thm.strip_shyps raw_th;
    3.53      val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    3.54      val xshyps = Thm.extra_shyps th;
    3.55 @@ -73,20 +81,20 @@
    3.56      val prt_term = q o Syntax.pretty_term ctxt;
    3.57  
    3.58      val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    3.59 -    val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    3.60 -    val status = display_status show_status th;
    3.61 +    val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps;
    3.62 +    val status = display_status show_hyps show_status th;
    3.63  
    3.64      val hlen = length xshyps + length hyps' + length tpairs;
    3.65      val hsymbs =
    3.66        if hlen = 0 andalso status = "" then []
    3.67 -      else if ! show_hyps orelse show_hyps' then
    3.68 +      else if show_hyps orelse show_hyps' then
    3.69          [Pretty.brk 2, Pretty.list "[" "]"
    3.70            (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    3.71             map (Syntax.pretty_sort ctxt) xshyps @
    3.72              (if status = "" then [] else [Pretty.str status]))]
    3.73        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    3.74      val tsymbs =
    3.75 -      if null tags orelse not (! show_tags) then []
    3.76 +      if null tags orelse not show_tags then []
    3.77        else [Pretty.brk 1, pretty_tags tags];
    3.78    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    3.79