more explicit treatment of verbose mode, which includes concealed entries;
authorwenzelm
Sat Mar 15 11:22:25 2014 +0100 (2014-03-15 ago)
changeset 56158c2c6d560e7b2
parent 56157 7cfe7b6d501a
child 56159 39f7b7690de6
more explicit treatment of verbose mode, which includes concealed entries;
src/Doc/IsarRef/Misc.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/proof_general.ML
src/Pure/facts.ML
     1.1 --- a/src/Doc/IsarRef/Misc.thy	Sat Mar 15 10:29:42 2014 +0100
     1.2 +++ b/src/Doc/IsarRef/Misc.thy	Sat Mar 15 11:22:25 2014 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail \<open>
     1.7 -    (@@{command print_theory} | @@{command print_theorems}) ('!'?)
     1.8 +    (@@{command print_theory} | @@{command print_theorems} | @@{command print_facts}) ('!'?)
     1.9      ;
    1.10  
    1.11      @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * )
    1.12 @@ -59,6 +59,13 @@
    1.13    theory resulting from the last command; the ``@{text "!"}'' option
    1.14    indicates extra verbosity.
    1.15    
    1.16 +  \item @{command "print_facts"} prints all local facts of the
    1.17 +  current context, both named and unnamed ones; the ``@{text "!"}''
    1.18 +  option indicates extra verbosity.
    1.19 +  
    1.20 +  \item @{command "print_binds"} prints all term abbreviations
    1.21 +  present in the context.
    1.22 +
    1.23    \item @{command "find_theorems"}~@{text criteria} retrieves facts
    1.24    from the theory or proof context matching all of given search
    1.25    criteria.  The criterion @{text "name: p"} selects all theorems
    1.26 @@ -102,12 +109,6 @@
    1.27    defaults to the current theory. If no range is specified,
    1.28    only the unused theorems in the current theory are displayed.
    1.29    
    1.30 -  \item @{command "print_facts"} prints all local facts of the
    1.31 -  current context, both named and unnamed ones.
    1.32 -  
    1.33 -  \item @{command "print_binds"} prints all term abbreviations
    1.34 -  present in the context.
    1.35 -
    1.36    \end{description}
    1.37  *}
    1.38  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Mar 15 10:29:42 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Mar 15 11:22:25 2014 +0100
     2.3 @@ -459,7 +459,7 @@
     2.4        else
     2.5          is_too_complex
     2.6      val local_facts = Proof_Context.facts_of ctxt
     2.7 -    val named_locals = local_facts |> Facts.dest_static [global_facts]
     2.8 +    val named_locals = local_facts |> Facts.dest_static true [global_facts]
     2.9      val assms = Assumption.all_assms_of ctxt
    2.10      fun is_good_unnamed_local th =
    2.11        not (Thm.has_name_hint th) andalso
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 10:29:42 2014 +0100
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 11:22:25 2014 +0100
     3.3 @@ -255,8 +255,9 @@
     3.4  
     3.5  (* print theorems *)
     3.6  
     3.7 -val print_theorems_proof =
     3.8 -  Toplevel.keep (Proof_Context.print_local_facts o Proof.context_of o Toplevel.proof_of);
     3.9 +fun print_theorems_proof verbose =
    3.10 +  Toplevel.keep (fn st =>
    3.11 +    Proof_Context.print_local_facts (Proof.context_of (Toplevel.proof_of st)) verbose);
    3.12  
    3.13  fun print_theorems_theory verbose = Toplevel.keep (fn state =>
    3.14    Toplevel.theory_of state |>
    3.15 @@ -265,7 +266,7 @@
    3.16    | NONE => Proof_Display.print_theorems verbose));
    3.17  
    3.18  fun print_theorems verbose =
    3.19 -  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof;
    3.20 +  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof verbose;
    3.21  
    3.22  
    3.23  (* display dependencies *)
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Mar 15 10:29:42 2014 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 15 11:22:25 2014 +0100
     4.3 @@ -876,8 +876,8 @@
     4.4  
     4.5  val _ =
     4.6    Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
     4.7 -    (Scan.succeed (Toplevel.unknown_context o
     4.8 -      Toplevel.keep (Proof_Context.print_local_facts o Toplevel.context_of)));
     4.9 +    (opt_bang >> (fn verbose => Toplevel.unknown_context o
    4.10 +      Toplevel.keep (fn st => Proof_Context.print_local_facts (Toplevel.context_of st) verbose)));
    4.11  
    4.12  val _ =
    4.13    Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
     5.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 15 10:29:42 2014 +0100
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 15 11:22:25 2014 +0100
     5.3 @@ -162,7 +162,7 @@
     5.4    val print_syntax: Proof.context -> unit
     5.5    val print_abbrevs: Proof.context -> unit
     5.6    val print_binds: Proof.context -> unit
     5.7 -  val print_local_facts: Proof.context -> unit
     5.8 +  val print_local_facts: Proof.context -> bool -> unit
     5.9    val print_cases: Proof.context -> unit
    5.10    val debug: bool Config.T
    5.11    val verbose: bool Config.T
    5.12 @@ -1268,13 +1268,13 @@
    5.13  
    5.14  (* local facts *)
    5.15  
    5.16 -fun pretty_local_facts ctxt =
    5.17 +fun pretty_local_facts ctxt verbose =
    5.18    let
    5.19      val facts = facts_of ctxt;
    5.20      val props = Facts.props facts;
    5.21      val local_facts =
    5.22        (if null props then [] else [("<unnamed>", props)]) @
    5.23 -      Facts.dest_static [Global_Theory.facts_of (theory_of ctxt)] facts;
    5.24 +      Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts;
    5.25    in
    5.26      if null local_facts then []
    5.27      else
    5.28 @@ -1282,7 +1282,8 @@
    5.29          (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
    5.30    end;
    5.31  
    5.32 -val print_local_facts = Pretty.writeln o Pretty.chunks o pretty_local_facts;
    5.33 +fun print_local_facts ctxt verbose =
    5.34 +  Pretty.writeln (Pretty.chunks (pretty_local_facts ctxt verbose));
    5.35  
    5.36  
    5.37  (* local contexts *)
    5.38 @@ -1406,7 +1407,7 @@
    5.39      pretty_ctxt ctxt @
    5.40      verb (pretty_abbrevs false) (K ctxt) @
    5.41      verb pretty_binds (K ctxt) @
    5.42 -    verb pretty_local_facts (K ctxt) @
    5.43 +    verb (pretty_local_facts ctxt) (K true) @
    5.44      verb pretty_cases (K ctxt) @
    5.45      verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
    5.46      verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
     6.1 --- a/src/Pure/Isar/proof_display.ML	Sat Mar 15 10:29:42 2014 +0100
     6.2 +++ b/src/Pure/Isar/proof_display.ML	Sat Mar 15 11:22:25 2014 +0100
     6.3 @@ -63,9 +63,7 @@
     6.4    let
     6.5      val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
     6.6      val facts = Global_Theory.facts_of thy;
     6.7 -    val thmss =
     6.8 -      Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
     6.9 -      |> not verbose ? filter_out (Facts.is_concealed facts o #1);
    6.10 +    val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
    6.11    in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    6.12  
    6.13  fun print_theorems_diff verbose prev_thy thy =
     7.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Mar 15 10:29:42 2014 +0100
     7.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Mar 15 11:22:25 2014 +0100
     7.3 @@ -382,13 +382,12 @@
     7.4  
     7.5  fun all_facts_of ctxt =
     7.6    let
     7.7 -    fun visible_facts facts =
     7.8 -      Facts.dest_static [] facts
     7.9 -      |> filter_out (Facts.is_concealed facts o #1);
    7.10 +    val local_facts = Proof_Context.facts_of ctxt;
    7.11 +    val global_facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
    7.12    in
    7.13      maps Facts.selections
    7.14 -     (visible_facts (Proof_Context.facts_of ctxt) @
    7.15 -      visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)))
    7.16 +     (Facts.dest_static false [] local_facts @  (* FIXME exclude global_facts *)
    7.17 +      Facts.dest_static false [] global_facts)
    7.18    end;
    7.19  
    7.20  fun filter_theorems ctxt theorems query =
     8.1 --- a/src/Pure/Tools/proof_general.ML	Sat Mar 15 10:29:42 2014 +0100
     8.2 +++ b/src/Pure/Tools/proof_general.ML	Sat Mar 15 11:22:25 2014 +0100
     8.3 @@ -391,7 +391,7 @@
     8.4      let
     8.5        val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state);
     8.6        val facts = Global_Theory.facts_of (Toplevel.theory_of state');
     8.7 -      val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static [prev_facts] facts));
     8.8 +      val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static true [prev_facts] facts));
     8.9      in
    8.10        if null names orelse null deps then ()
    8.11        else thm_deps_message (spaces_quote names, spaces_quote deps)
     9.1 --- a/src/Pure/facts.ML	Sat Mar 15 10:29:42 2014 +0100
     9.2 +++ b/src/Pure/facts.ML	Sat Mar 15 11:22:25 2014 +0100
     9.3 @@ -31,8 +31,7 @@
     9.4    val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
     9.5    val defined: T -> string -> bool
     9.6    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
     9.7 -  val dest_static: T list -> T -> (string * thm list) list
     9.8 -  val extern_static: Proof.context -> T list -> T -> (xstring * thm list) list
     9.9 +  val dest_static: bool -> T list -> T -> (string * thm list) list
    9.10    val props: T -> thm list
    9.11    val could_unify: T -> term -> thm list
    9.12    val merge: T * T -> T
    9.13 @@ -159,6 +158,9 @@
    9.14  fun extern ctxt = Name_Space.extern ctxt o space_of;
    9.15  fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of
    9.16  
    9.17 +
    9.18 +(* retrieve *)
    9.19 +
    9.20  val defined = is_some oo (Name_Space.lookup_key o facts_of);
    9.21  
    9.22  fun lookup context facts name =
    9.23 @@ -179,22 +181,18 @@
    9.24        | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
    9.25    in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
    9.26  
    9.27 +
    9.28 +(* static content *)
    9.29 +
    9.30  fun fold_static f =
    9.31    Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
    9.32  
    9.33 -
    9.34 -(* content difference *)
    9.35 -
    9.36 -fun diff_table prev_facts facts =
    9.37 +fun dest_static verbose prev_facts facts =
    9.38    fold_static (fn (name, ths) =>
    9.39 -    if exists (fn prev => defined prev name) prev_facts then I
    9.40 -    else cons (name, ths)) facts [];
    9.41 -
    9.42 -fun dest_static prev_facts facts =
    9.43 -  sort_wrt #1 (diff_table prev_facts facts);
    9.44 -
    9.45 -fun extern_static ctxt prev_facts facts =
    9.46 -  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern ctxt facts)));
    9.47 +    if exists (fn prev => defined prev name) prev_facts orelse
    9.48 +      not verbose andalso is_concealed facts name then I
    9.49 +    else cons (name, ths)) facts []
    9.50 +  |> sort_wrt #1;
    9.51  
    9.52  
    9.53  (* indexed props *)