# HG changeset patch
# User wenzelm
# Date 1394878945 -3600
# Node ID c2c6d560e7b219a3ae5801a68fd4b4e50b19f7cd
# Parent  7cfe7b6d501a0f3e88a8d32fe1bb72f27a14db2c
more explicit treatment of verbose mode, which includes concealed entries;

diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/Doc/IsarRef/Misc.thy
--- a/src/Doc/IsarRef/Misc.thy	Sat Mar 15 10:29:42 2014 +0100
+++ b/src/Doc/IsarRef/Misc.thy	Sat Mar 15 11:22:25 2014 +0100
@@ -21,7 +21,7 @@
   \end{matharray}
 
   @{rail \<open>
-    (@@{command print_theory} | @@{command print_theorems}) ('!'?)
+    (@@{command print_theory} | @@{command print_theorems} | @@{command print_facts}) ('!'?)
     ;
 
     @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * )
@@ -59,6 +59,13 @@
   theory resulting from the last command; the ``@{text "!"}'' option
   indicates extra verbosity.
   
+  \item @{command "print_facts"} prints all local facts of the
+  current context, both named and unnamed ones; the ``@{text "!"}''
+  option indicates extra verbosity.
+  
+  \item @{command "print_binds"} prints all term abbreviations
+  present in the context.
+
   \item @{command "find_theorems"}~@{text criteria} retrieves facts
   from the theory or proof context matching all of given search
   criteria.  The criterion @{text "name: p"} selects all theorems
@@ -102,12 +109,6 @@
   defaults to the current theory. If no range is specified,
   only the unused theorems in the current theory are displayed.
   
-  \item @{command "print_facts"} prints all local facts of the
-  current context, both named and unnamed ones.
-  
-  \item @{command "print_binds"} prints all term abbreviations
-  present in the context.
-
   \end{description}
 *}
 
diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Mar 15 10:29:42 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Mar 15 11:22:25 2014 +0100
@@ -459,7 +459,7 @@
       else
         is_too_complex
     val local_facts = Proof_Context.facts_of ctxt
-    val named_locals = local_facts |> Facts.dest_static [global_facts]
+    val named_locals = local_facts |> Facts.dest_static true [global_facts]
     val assms = Assumption.all_assms_of ctxt
     fun is_good_unnamed_local th =
       not (Thm.has_name_hint th) andalso
diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 10:29:42 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 11:22:25 2014 +0100
@@ -255,8 +255,9 @@
 
 (* print theorems *)
 
-val print_theorems_proof =
-  Toplevel.keep (Proof_Context.print_local_facts o Proof.context_of o Toplevel.proof_of);
+fun print_theorems_proof verbose =
+  Toplevel.keep (fn st =>
+    Proof_Context.print_local_facts (Proof.context_of (Toplevel.proof_of st)) verbose);
 
 fun print_theorems_theory verbose = Toplevel.keep (fn state =>
   Toplevel.theory_of state |>
@@ -265,7 +266,7 @@
   | NONE => Proof_Display.print_theorems verbose));
 
 fun print_theorems verbose =
-  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof;
+  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof verbose;
 
 
 (* display dependencies *)
diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Mar 15 10:29:42 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 15 11:22:25 2014 +0100
@@ -876,8 +876,8 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Proof_Context.print_local_facts o Toplevel.context_of)));
+    (opt_bang >> (fn verbose => Toplevel.unknown_context o
+      Toplevel.keep (fn st => Proof_Context.print_local_facts (Toplevel.context_of st) verbose)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 15 10:29:42 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 15 11:22:25 2014 +0100
@@ -162,7 +162,7 @@
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
   val print_binds: Proof.context -> unit
-  val print_local_facts: Proof.context -> unit
+  val print_local_facts: Proof.context -> bool -> unit
   val print_cases: Proof.context -> unit
   val debug: bool Config.T
   val verbose: bool Config.T
@@ -1268,13 +1268,13 @@
 
 (* local facts *)
 
-fun pretty_local_facts ctxt =
+fun pretty_local_facts ctxt verbose =
   let
     val facts = facts_of ctxt;
     val props = Facts.props facts;
     val local_facts =
       (if null props then [] else [("<unnamed>", props)]) @
-      Facts.dest_static [Global_Theory.facts_of (theory_of ctxt)] facts;
+      Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts;
   in
     if null local_facts then []
     else
@@ -1282,7 +1282,8 @@
         (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
   end;
 
-val print_local_facts = Pretty.writeln o Pretty.chunks o pretty_local_facts;
+fun print_local_facts ctxt verbose =
+  Pretty.writeln (Pretty.chunks (pretty_local_facts ctxt verbose));
 
 
 (* local contexts *)
@@ -1406,7 +1407,7 @@
     pretty_ctxt ctxt @
     verb (pretty_abbrevs false) (K ctxt) @
     verb pretty_binds (K ctxt) @
-    verb pretty_local_facts (K ctxt) @
+    verb (pretty_local_facts ctxt) (K true) @
     verb pretty_cases (K ctxt) @
     verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
     verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sat Mar 15 10:29:42 2014 +0100
+++ b/src/Pure/Isar/proof_display.ML	Sat Mar 15 11:22:25 2014 +0100
@@ -63,9 +63,7 @@
   let
     val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
     val facts = Global_Theory.facts_of thy;
-    val thmss =
-      Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
-      |> not verbose ? filter_out (Facts.is_concealed facts o #1);
+    val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
   in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
 
 fun print_theorems_diff verbose prev_thy thy =
diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Mar 15 10:29:42 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sat Mar 15 11:22:25 2014 +0100
@@ -382,13 +382,12 @@
 
 fun all_facts_of ctxt =
   let
-    fun visible_facts facts =
-      Facts.dest_static [] facts
-      |> filter_out (Facts.is_concealed facts o #1);
+    val local_facts = Proof_Context.facts_of ctxt;
+    val global_facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
   in
     maps Facts.selections
-     (visible_facts (Proof_Context.facts_of ctxt) @
-      visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)))
+     (Facts.dest_static false [] local_facts @  (* FIXME exclude global_facts *)
+      Facts.dest_static false [] global_facts)
   end;
 
 fun filter_theorems ctxt theorems query =
diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Sat Mar 15 10:29:42 2014 +0100
+++ b/src/Pure/Tools/proof_general.ML	Sat Mar 15 11:22:25 2014 +0100
@@ -391,7 +391,7 @@
     let
       val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state);
       val facts = Global_Theory.facts_of (Toplevel.theory_of state');
-      val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static [prev_facts] facts));
+      val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static true [prev_facts] facts));
     in
       if null names orelse null deps then ()
       else thm_deps_message (spaces_quote names, spaces_quote deps)
diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sat Mar 15 10:29:42 2014 +0100
+++ b/src/Pure/facts.ML	Sat Mar 15 11:22:25 2014 +0100
@@ -31,8 +31,7 @@
   val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
   val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
-  val dest_static: T list -> T -> (string * thm list) list
-  val extern_static: Proof.context -> T list -> T -> (xstring * thm list) list
+  val dest_static: bool -> T list -> T -> (string * thm list) list
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
@@ -159,6 +158,9 @@
 fun extern ctxt = Name_Space.extern ctxt o space_of;
 fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of
 
+
+(* retrieve *)
+
 val defined = is_some oo (Name_Space.lookup_key o facts_of);
 
 fun lookup context facts name =
@@ -179,22 +181,18 @@
       | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
   in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
 
+
+(* static content *)
+
 fun fold_static f =
   Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
 
-
-(* content difference *)
-
-fun diff_table prev_facts facts =
+fun dest_static verbose prev_facts facts =
   fold_static (fn (name, ths) =>
-    if exists (fn prev => defined prev name) prev_facts then I
-    else cons (name, ths)) facts [];
-
-fun dest_static prev_facts facts =
-  sort_wrt #1 (diff_table prev_facts facts);
-
-fun extern_static ctxt prev_facts facts =
-  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern ctxt facts)));
+    if exists (fn prev => defined prev name) prev_facts orelse
+      not verbose andalso is_concealed facts name then I
+    else cons (name, ths)) facts []
+  |> sort_wrt #1;
 
 
 (* indexed props *)