# HG changeset patch
# User wenzelm
# Date 1428083811 -7200
# Node ID 9830c944670f70861957608fcc4f800c34942a9b
# Parent  f673ce6b1e2b71cce98b155620c650d48b74bfd1
more uniform "verbose" option to print name space;

diff -r f673ce6b1e2b -r 9830c944670f src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Apr 03 19:56:51 2015 +0200
@@ -85,6 +85,7 @@
 
 text \<open>
   \begin{matharray}{rcl}
+    @{command_def "print_antiquotations"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
     @{antiquotation_def "theory"} & : & @{text antiquotation} \\
     @{antiquotation_def "thm"} & : & @{text antiquotation} \\
     @{antiquotation_def "lemma"} & : & @{text antiquotation} \\
@@ -132,6 +133,10 @@
   antiquotations are checked within the current theory or proof
   context.
 
+  @{rail \<open>
+    @@{command print_antiquotations} ('!'?)
+  \<close>}
+
   %% FIXME less monolithic presentation, move to individual sections!?
   @{rail \<open>
     '@{' antiquotation '}'
@@ -182,7 +187,11 @@
   text @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"}.
 
   \begin{description}
-  
+
+  \item @{command "print_antiquotations"} prints all document antiquotations
+  that are defined in the current context; the ``@{text "!"}'' option
+  indicates extra verbosity.
+
   \item @{text "@{theory A}"} prints the name @{text "A"}, which is
   guaranteed to refer to a valid ancestor theory in the current
   context.
diff -r f673ce6b1e2b -r 9830c944670f src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Fri Apr 03 19:56:51 2015 +0200
@@ -37,13 +37,16 @@
   \end{matharray}
 
   @{rail \<open>
+    @@{command print_options} ('!'?)
+    ;
     @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
   \<close>}
 
   \begin{description}
   
   \item @{command "print_options"} prints the available configuration
-  options, with names, types, and current values.
+  options, with names, types, and current values; the ``@{text "!"}'' option
+  indicates extra verbosity.
   
   \item @{text "name = value"} as an attribute expression modifies the
   named option, with the syntax of the value depending on the option's
@@ -611,6 +614,8 @@
   @{rail \<open>
     (@@{attribute simp} | @@{attribute split} | @@{attribute cong})
       (() | 'add' | 'del')
+    ;
+    @@{command print_simpset} ('!'?)
   \<close>}
 
   \begin{description}
@@ -716,9 +721,9 @@
   This can make simplification much faster, but may require an extra
   case split over the condition @{text "?q"} to prove the goal.
 
-  \item @{command "print_simpset"} prints the collection of rules
-  declared to the Simplifier, which is also known as ``simpset''
-  internally.
+  \item @{command "print_simpset"} prints the collection of rules declared
+  to the Simplifier, which is also known as ``simpset'' internally; the
+  ``@{text "!"}'' option indicates extra verbosity.
 
   For historical reasons, simpsets may occur independently from the
   current context, but are conceptually dependent on it.  When the
diff -r f673ce6b1e2b -r 9830c944670f src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Apr 03 19:56:51 2015 +0200
@@ -105,6 +105,8 @@
     ;
     clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
     ;
+    @@{command print_inductives} ('!'?)
+    ;
     @@{attribute (HOL) mono} (() | 'add' | 'del')
   \<close>}
 
@@ -137,7 +139,7 @@
   where multiple arguments are simulated via tuples.
 
   \item @{command "print_inductives"} prints (co)inductive definitions and
-  monotonicity rules.
+  monotonicity rules; the ``@{text "!"}'' option indicates extra verbosity.
 
   \item @{attribute (HOL) mono} declares monotonicity rules in the
   context.  These rule are involved in the automated monotonicity
diff -r f673ce6b1e2b -r 9830c944670f src/Doc/Isar_Ref/Misc.thy
--- a/src/Doc/Isar_Ref/Misc.thy	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Doc/Isar_Ref/Misc.thy	Fri Apr 03 19:56:51 2015 +0200
@@ -21,9 +21,12 @@
   \end{matharray}
 
   @{rail \<open>
-    (@@{command print_theory} | @@{command print_theorems} | @@{command print_facts}) ('!'?)
+    (@@{command print_theory} |
+      @@{command print_methods} |
+      @@{command print_attributes} |
+      @@{command print_theorems} |
+      @@{command print_facts}) ('!'?)
     ;
-
     @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * )
     ;
     thmcriterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
@@ -45,23 +48,24 @@
 
   \begin{description}
   
-  \item @{command "print_theory"} prints the main logical content of
-  the background theory; the ``@{text "!"}'' option indicates extra
+  \item @{command "print_theory"} prints the main logical content of the
+  background theory; the ``@{text "!"}'' option indicates extra verbosity.
+
+  \item @{command "print_methods"} prints all proof methods available in the
+  current theory context; the ``@{text "!"}'' option indicates extra
   verbosity.
-
-  \item @{command "print_methods"} prints all proof methods
-  available in the current theory context.
   
-  \item @{command "print_attributes"} prints all attributes
-  available in the current theory context.
+  \item @{command "print_attributes"} prints all attributes available in the
+  current theory context; the ``@{text "!"}'' option indicates extra
+  verbosity.
   
-  \item @{command "print_theorems"} prints theorems of the background
-  theory resulting from the last command; the ``@{text "!"}'' option
-  indicates extra verbosity.
+  \item @{command "print_theorems"} prints theorems of the background 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_facts"} prints all local facts of the current
+  context, both named and unnamed ones; the ``@{text "!"}'' option indicates
+  extra verbosity.
   
   \item @{command "print_term_bindings"} prints all term bindings that
   are present in the context.
diff -r f673ce6b1e2b -r 9830c944670f src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri Apr 03 19:56:51 2015 +0200
@@ -223,6 +223,8 @@
   @{rail \<open>
     @@{command bundle} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes}
     ;
+    @@{command print_bundles} ('!'?)
+    ;
     (@@{command include} | @@{command including}) (@{syntax nameref}+)
     ;
     @{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
@@ -237,8 +239,9 @@
   into different application contexts; this works analogously to any
   other local theory specification.
 
-  \item @{command print_bundles} prints the named bundles that are
-  available in the current context.
+  \item @{command print_bundles} prints the named bundles that are available
+  in the current context; the ``@{text "!"}'' option indicates extra
+  verbosity.
 
   \item @{command include}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} includes the declarations
   from the given bundles into the current proof body context.  This is
@@ -290,8 +293,9 @@
     @@{command abbreviation} @{syntax mode}? \<newline>
       (decl @'where')? @{syntax prop}
     ;
-
     decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
+    ;
+    @@{command print_abbrevs} ('!'?)
   \<close>}
 
   \begin{description}
@@ -330,8 +334,8 @@
   declared for abbreviations, cf.\ @{command "syntax"} in
   \secref{sec:syn-trans}.
   
-  \item @{command "print_abbrevs"} prints all constant abbreviations
-  of the current context.
+  \item @{command "print_abbrevs"} prints all constant abbreviations of the
+  current context; the ``@{text "!"}'' option indicates extra verbosity.
   
   \end{description}
 \<close>
@@ -520,6 +524,8 @@
     ;
     @@{command print_locale} '!'? @{syntax nameref}
     ;
+    @@{command print_locales} ('!'?)
+    ;
     @{syntax_def locale}: @{syntax context_elem}+ |
       @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
     ;
@@ -626,8 +632,8 @@
   elements by default.  Use @{command "print_locale"}@{text "!"} to
   have them included.
 
-  \item @{command "print_locales"} prints the names of all locales
-  of the current theory.
+  \item @{command "print_locales"} prints the names of all locales of the
+  current theory; the ``@{text "!"}'' option indicates extra verbosity.
 
   \item @{command "locale_deps"} visualizes all locales and their
   relations as a Hasse diagram. This includes locales defined as type
diff -r f673ce6b1e2b -r 9830c944670f src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -26,7 +26,7 @@
   val transform_result: morphism -> inductive_result -> inductive_result
   type inductive_info = {names: string list, coind: bool} * inductive_result
   val the_inductive: Proof.context -> string -> inductive_info
-  val print_inductives: Proof.context -> unit
+  val print_inductives: bool -> Proof.context -> unit
   val get_monos: Proof.context -> thm list
   val mono_add: attribute
   val mono_del: attribute
@@ -227,7 +227,7 @@
 
 fun rep_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data rep => rep);
 
-fun print_inductives ctxt =
+fun print_inductives verbose ctxt =
   let
     val {infos, monos, ...} = rep_data ctxt;
     val space = Consts.space_of (Proof_Context.consts_of ctxt);
@@ -235,7 +235,8 @@
     [Pretty.block
       (Pretty.breaks
         (Pretty.str "(co)inductives:" ::
-          map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))),
+          map (Pretty.mark_str o #1)
+            (Name_Space.markup_entries verbose ctxt space (Symtab.dest infos)))),
      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
   end |> Pretty.writeln_chunks;
 
@@ -1190,7 +1191,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "print_inductives"}
     "print (co)inductive definitions and monotonicity rules"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_inductives o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+      Toplevel.keep (print_inductives b o Toplevel.context_of)));
 
 end;
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/General/name_space.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -79,10 +79,12 @@
   val merge_tables: 'a table * 'a table -> 'a table
   val join_tables: (string -> 'a * 'a -> 'a) (*exception Change_Table.SAME*) ->
     'a table * 'a table -> 'a table
-  val extern_entries: Proof.context -> T -> (string * 'a) list -> ((string * xstring) * 'a) list
-  val markup_entries: Proof.context -> T -> (string * 'a) list -> ((Markup.T * xstring) * 'a) list
-  val extern_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
-  val markup_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
+  val extern_entries: bool -> Proof.context -> T -> (string * 'a) list ->
+    ((string * xstring) * 'a) list
+  val markup_entries: bool -> Proof.context -> T -> (string * 'a) list ->
+    ((Markup.T * xstring) * 'a) list
+  val extern_table: bool -> Proof.context -> 'a table -> ((string * xstring) * 'a) list
+  val markup_table: bool -> Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
 end;
 
 structure Name_Space: NAME_SPACE =
@@ -569,15 +571,20 @@
 
 (* present table content *)
 
-fun extern_entries ctxt space entries =
-  fold (fn (name, x) => cons ((name, extern ctxt space name), x)) entries []
+fun extern_entries verbose ctxt space entries =
+  fold (fn (name, x) =>
+    (verbose orelse not (is_concealed space name)) ?
+      cons ((name, extern ctxt space name), x)) entries []
   |> Library.sort_wrt (#2 o #1);
 
-fun markup_entries ctxt space entries =
-  extern_entries ctxt space entries
+fun markup_entries verbose ctxt space entries =
+  extern_entries verbose ctxt space entries
   |> map (fn ((name, xname), x) => ((markup space name, xname), x));
 
-fun extern_table ctxt (Table (space, tab)) = extern_entries ctxt space (Change_Table.dest tab);
-fun markup_table ctxt (Table (space, tab)) = markup_entries ctxt space (Change_Table.dest tab);
+fun extern_table verbose ctxt (Table (space, tab)) =
+  extern_entries verbose ctxt space (Change_Table.dest tab);
+
+fun markup_table verbose ctxt (Table (space, tab)) =
+  markup_entries verbose ctxt space (Change_Table.dest tab);
 
 end;
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -9,7 +9,7 @@
   type binding = binding * Token.src list
   val empty_binding: binding
   val is_empty_binding: binding -> bool
-  val print_attributes: Proof.context -> unit
+  val print_attributes: bool -> Proof.context -> unit
   val define_global: Binding.binding -> (Token.src -> attribute) ->
     string -> theory -> string * theory
   val define: Binding.binding -> (Token.src -> attribute) ->
@@ -56,7 +56,7 @@
   val partial_evaluation: Proof.context ->
     (binding * (thm list * Token.src list) list) list ->
     (binding * (thm list * Token.src list) list) list
-  val print_options: Proof.context -> unit
+  val print_options: bool -> Proof.context -> unit
   val config_bool: Binding.binding ->
     (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   val config_int: Binding.binding ->
@@ -111,7 +111,7 @@
     val attribs' = Name_Space.merge_tables (attribs0, get_attributes ctxt);
   in Context.proof_map (Attributes.put attribs') ctxt end;
 
-fun print_attributes ctxt =
+fun print_attributes verbose ctxt =
   let
     val attribs = get_attributes ctxt;
     fun prt_attr (name, (_, "")) = Pretty.mark_str name
@@ -119,7 +119,7 @@
           Pretty.block
             (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   in
-    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table ctxt attribs))]
+    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table verbose ctxt attribs))]
     |> Pretty.writeln_chunks
   end;
 
@@ -387,7 +387,7 @@
   fun merge data = Symtab.merge (K true) data;
 );
 
-fun print_options ctxt =
+fun print_options verbose ctxt =
   let
     fun prt (name, config) =
       let val value = Config.get ctxt config in
@@ -396,7 +396,7 @@
       end;
     val space = attribute_space ctxt;
     val configs =
-      Name_Space.markup_entries ctxt space
+      Name_Space.markup_entries verbose ctxt space
         (Symtab.dest (Configs.get (Proof_Context.theory_of ctxt)));
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
 
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Isar/bundle.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -24,7 +24,7 @@
     generic_theory -> Binding.scope * local_theory
   val context_cmd: (xstring * Position.T) list -> Element.context list ->
     generic_theory -> Binding.scope * local_theory
-  val print_bundles: Proof.context -> unit
+  val print_bundles: bool -> Proof.context -> unit
 end;
 
 structure Bundle: BUNDLE =
@@ -122,7 +122,7 @@
 
 (* print_bundles *)
 
-fun print_bundles ctxt =
+fun print_bundles verbose ctxt =
   let
     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
 
@@ -134,7 +134,7 @@
       Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name ::
         Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
   in
-    map prt_bundle (Name_Space.markup_table ctxt (get_bundles ctxt))
+    map prt_bundle (Name_Space.markup_table verbose ctxt (get_bundles ctxt))
   end |> Pretty.writeln_chunks;
 
 end;
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -257,7 +257,7 @@
 
 fun pretty_theorems verbose st =
   if Toplevel.is_proof st then
-    Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose
+    Proof_Context.pretty_local_facts verbose (Toplevel.context_of st)
   else
     let
       val thy = Toplevel.theory_of st;
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -350,8 +350,8 @@
 val _ =
   Outer_Syntax.command @{command_spec "print_bundles"}
     "print bundles of declarations"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+      Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
 
 
 (* local theories *)
@@ -681,8 +681,6 @@
 val opt_modes =
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
 
-val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
-
 val _ =
   Outer_Syntax.command @{command_spec "help"}
     "retrieve outer syntax commands according to name patterns"
@@ -695,8 +693,8 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+      Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_context"}
@@ -705,13 +703,13 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "print_theory"}
-    "print logical theory contents (verbose!)"
-    (opt_bang >> (fn b => Toplevel.unknown_theory o
+    "print logical theory contents"
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_syntax"}
-    "print inner syntax of context (verbose!)"
+    "print inner syntax of context"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
 
@@ -724,21 +722,21 @@
 val _ =
   Outer_Syntax.command @{command_spec "print_abbrevs"}
     "print constant abbreviations of context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+      Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_theorems"}
     "print theorems of local theory or proof context"
-    (opt_bang >> (fn b =>
+    (Parse.opt_bang >> (fn b =>
       Toplevel.unknown_context o
       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_locales"}
     "print locales of this theory"
-    (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
+      Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_classes"}
@@ -749,7 +747,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "print_locale"}
     "print locale of this theory"
-    (opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
+    (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
       Toplevel.unknown_theory o
       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
 
@@ -763,21 +761,21 @@
 val _ =
   Outer_Syntax.command @{command_spec "print_dependencies"}
     "print dependencies of locale expression"
-    (opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
+    (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
       Toplevel.unknown_context o
       Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_attributes"}
     "print attributes of this theory"
-    (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (Attrib.print_attributes o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
+      Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_simpset"}
     "print context of Simplifier"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+      Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_rules"} "print intro/elim rules"
@@ -786,20 +784,20 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "print_methods"} "print methods of this theory"
-    (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (Method.print_methods o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
+      Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_antiquotations"}
     "print document antiquotations"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+      Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_ML_antiquotations"}
     "print ML antiquotations"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (ML_Context.print_antiquotations o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+      Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "thy_deps"} "visualize theory dependencies"
@@ -818,8 +816,8 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "print_facts"} "print facts of proof context"
-    (opt_bang >> (fn verbose => Toplevel.unknown_context o
-      Toplevel.keep (fn st => Proof_Context.print_local_facts (Toplevel.context_of st) verbose)));
+    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+      Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_cases"} "print cases of proof context"
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -84,7 +84,7 @@
 
   (* Diagnostic *)
   val hyp_spec_of: theory -> string -> Element.context_i list
-  val print_locales: theory -> unit
+  val print_locales: bool -> theory -> unit
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
@@ -653,12 +653,12 @@
 
 fun hyp_spec_of thy = #hyp_spec o the_locale thy;
 
-fun print_locales thy =
+fun print_locales verbose thy =
   Pretty.block
     (Pretty.breaks
       (Pretty.str "locales:" ::
         map (Pretty.mark_str o #1)
-          (Name_Space.markup_table (Proof_Context.init_global thy) (Locales.get thy))))
+          (Name_Space.markup_table verbose (Proof_Context.init_global thy) (Locales.get thy))))
   |> Pretty.writeln;
 
 fun pretty_locale thy show_facts name =
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Isar/method.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -54,7 +54,7 @@
   val done_text: text
   val sorry_text: bool -> text
   val finish_text: text option * bool -> text
-  val print_methods: Proof.context -> unit
+  val print_methods: bool -> Proof.context -> unit
   val check_name: Proof.context -> xstring * Position.T -> string
   val check_src: Proof.context -> Token.src -> Token.src
   val method_syntax: (Proof.context -> method) context_parser ->
@@ -333,7 +333,7 @@
     val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt));
   in Context.proof_map (map_methods (K meths')) ctxt end;
 
-fun print_methods ctxt =
+fun print_methods verbose ctxt =
   let
     val meths = get_methods (Context.Proof ctxt);
     fun prt_meth (name, (_, "")) = Pretty.mark_str name
@@ -341,7 +341,7 @@
           Pretty.block
             (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   in
-    [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))]
+    [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table verbose ctxt meths))]
     |> Pretty.writeln_chunks
   end;
 
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -46,6 +46,7 @@
   val tags: string list parser
   val opt_unit: unit parser
   val opt_keyword: string -> bool parser
+  val opt_bang: bool parser
   val begin: string parser
   val opt_begin: bool parser
   val nat: int parser
@@ -231,6 +232,7 @@
 
 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
 fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
+val opt_bang = Scan.optional ($$$ "!" >> K true) false;
 
 val begin = $$$ "begin";
 val opt_begin = Scan.optional (begin >> K true) false;
@@ -460,4 +462,3 @@
 val xthms1 = Scan.repeat1 xthm;
 
 end;
-
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -167,10 +167,10 @@
     (term * term) * Context.generic
   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
   val print_syntax: Proof.context -> unit
-  val print_abbrevs: Proof.context -> unit
+  val print_abbrevs: bool -> Proof.context -> unit
   val pretty_term_bindings: Proof.context -> Pretty.T list
-  val pretty_local_facts: Proof.context -> bool -> Pretty.T list
-  val print_local_facts: Proof.context -> bool -> unit
+  val pretty_local_facts: bool -> Proof.context -> Pretty.T list
+  val print_local_facts: bool -> Proof.context -> unit
   val pretty_cases: Proof.context -> Pretty.T list
   val debug: bool Config.T
   val verbose: bool Config.T
@@ -1276,7 +1276,7 @@
 
 (* abbreviations *)
 
-fun pretty_abbrevs show_globals ctxt =
+fun pretty_abbrevs verbose show_globals ctxt =
   let
     val space = const_space ctxt;
     val (constants, global_constants) =
@@ -1286,13 +1286,13 @@
       | add_abbr (c, (T, SOME t)) =
           if not show_globals andalso Symtab.defined globals c then I
           else cons (c, Logic.mk_equals (Const (c, T), t));
-    val abbrevs = Name_Space.markup_entries ctxt space (fold add_abbr constants []);
+    val abbrevs = Name_Space.markup_entries verbose ctxt space (fold add_abbr constants []);
   in
     if null abbrevs then []
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
   end;
 
-val print_abbrevs = Pretty.writeln_chunks o pretty_abbrevs true;
+fun print_abbrevs verbose = Pretty.writeln_chunks o pretty_abbrevs verbose true;
 
 
 (* term bindings *)
@@ -1309,7 +1309,7 @@
 
 (* local facts *)
 
-fun pretty_local_facts ctxt verbose =
+fun pretty_local_facts verbose ctxt =
   let
     val facts = facts_of ctxt;
     val props = Facts.props facts;
@@ -1323,8 +1323,8 @@
         (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
   end;
 
-fun print_local_facts ctxt verbose =
-  Pretty.writeln_chunks (pretty_local_facts ctxt verbose);
+fun print_local_facts verbose ctxt =
+  Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
 
 
 (* local contexts *)
@@ -1447,9 +1447,9 @@
   in
     verb single (K pretty_thy) @
     pretty_ctxt ctxt @
-    verb (pretty_abbrevs false) (K ctxt) @
+    verb (pretty_abbrevs true false) (K ctxt) @
     verb pretty_term_bindings (K ctxt) @
-    verb (pretty_local_facts ctxt) (K true) @
+    verb (pretty_local_facts true) (K ctxt) @
     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)))
@@ -1458,4 +1458,3 @@
 end;
 
 val show_abbrevs = Proof_Context.show_abbrevs;
-
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -19,7 +19,7 @@
   val value_decl: string -> string -> Proof.context -> decl * Proof.context
   val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
     theory -> theory
-  val print_antiquotations: Proof.context -> unit
+  val print_antiquotations: bool -> Proof.context -> unit
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   val eval_file: ML_Compiler.flags -> Path.T -> unit
   val eval_source: ML_Compiler.flags -> Input.source -> unit
@@ -102,9 +102,9 @@
 fun add_antiquotation name f thy = thy
   |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
 
-fun print_antiquotations ctxt =
+fun print_antiquotations verbose ctxt =
   Pretty.big_list "ML antiquotations:"
-    (map (Pretty.mark_str o #1) (Name_Space.markup_table ctxt (get_antiquotations ctxt)))
+    (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt)))
   |> Pretty.writeln;
 
 fun apply_antiquotation src ctxt =
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -17,7 +17,7 @@
   val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   val check_command: Proof.context -> xstring * Position.T -> string
   val check_option: Proof.context -> xstring * Position.T -> string
-  val print_antiquotations: Proof.context -> unit
+  val print_antiquotations: bool -> Proof.context -> unit
   val antiquotation: binding -> 'a context_parser ->
     ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
       theory -> theory
@@ -104,11 +104,11 @@
       Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
   in opt s ctxt end;
 
-fun print_antiquotations ctxt =
+fun print_antiquotations verbose ctxt =
   let
     val (commands, options) = get_antiquotations ctxt;
-    val command_names = map #1 (Name_Space.markup_table ctxt commands);
-    val option_names = map #1 (Name_Space.markup_table ctxt options);
+    val command_names = map #1 (Name_Space.markup_table verbose ctxt commands);
+    val option_names = map #1 (Name_Space.markup_table verbose ctxt options);
   in
     [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
      Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/display.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -157,25 +157,22 @@
     val arities = Sorts.arities_of class_algebra;
 
     val clsses =
-      Name_Space.extern_entries ctxt class_space
+      Name_Space.extern_entries verbose ctxt class_space
         (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
       |> map (apfst #1);
-    val tdecls = Name_Space.extern_table ctxt types |> map (apfst #1);
+    val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1);
     val arties =
-      Name_Space.extern_entries ctxt (Type.type_space tsig) (Symtab.dest arities)
+      Name_Space.extern_entries verbose ctxt (Type.type_space tsig) (Symtab.dest arities)
       |> map (apfst #1);
 
+    val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
+    val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
+    val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
+    val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
+
+    val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
+
     fun prune_const c = not verbose andalso Consts.is_concealed consts c;
-    val cnsts =
-      Name_Space.markup_entries ctxt const_space
-        (filter_out (prune_const o fst) constants);
-
-    val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
-    val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
-    val cnstrs = Name_Space.markup_entries ctxt const_space constraints;
-
-    val axms = Name_Space.markup_table ctxt (Theory.axiom_table thy);
-
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
         (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
@@ -195,7 +192,8 @@
       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
       Pretty.big_list "axioms:" (map pretty_axm axms),
       Pretty.block
-        (Pretty.breaks (Pretty.str "oracles:" :: map Pretty.mark_str (Thm.extern_oracles ctxt))),
+        (Pretty.breaks (Pretty.str "oracles:" ::
+          map Pretty.mark_str (Thm.extern_oracles verbose ctxt))),
       Pretty.big_list "definitions:"
         [pretty_finals reds0,
          Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/simplifier.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -42,7 +42,7 @@
   val def_simproc_cmd: {name: binding, lhss: string list,
     proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
     local_theory -> local_theory
-  val pretty_simpset: Proof.context -> Pretty.T
+  val pretty_simpset: bool -> Proof.context -> Pretty.T
   val default_mk_sym: Proof.context -> thm -> thm option
   val prems_of: Proof.context -> thm list
   val add_simp: thm -> Proof.context -> Proof.context
@@ -158,7 +158,7 @@
 
 (** pretty_simpset **)
 
-fun pretty_simpset ctxt =
+fun pretty_simpset verbose ctxt =
   let
     val pretty_term = Syntax.pretty_term ctxt;
     val pretty_thm = Display.pretty_thm ctxt;
@@ -177,7 +177,7 @@
     val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
       dest_ss (simpset_of ctxt);
     val simprocs =
-      Name_Space.markup_entries ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
+      Name_Space.markup_entries verbose ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
   in
     [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
       Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
diff -r f673ce6b1e2b -r 9830c944670f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/thm.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -137,7 +137,7 @@
     bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   (*oracles*)
-  val extern_oracles: Proof.context -> (Markup.T * xstring) list
+  val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
 
@@ -1750,8 +1750,8 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
-fun extern_oracles ctxt =
-  map #1 (Name_Space.markup_table ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
+fun extern_oracles verbose ctxt =
+  map #1 (Name_Space.markup_table verbose ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
 
 fun add_oracle (b, oracle) thy =
   let
diff -r f673ce6b1e2b -r 9830c944670f src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -227,12 +227,12 @@
       Pretty.block [
         Pretty.str "preprocessing simpset:",
         Pretty.fbrk,
-        Simplifier.pretty_simpset (put_simpset pre ctxt)
+        Simplifier.pretty_simpset true (put_simpset pre ctxt)
       ],
       Pretty.block [
         Pretty.str "postprocessing simpset:",
         Pretty.fbrk,
-        Simplifier.pretty_simpset (put_simpset post ctxt)
+        Simplifier.pretty_simpset true (put_simpset post ctxt)
       ],
       Pretty.block (
         Pretty.str "function transformers:"