more uniform "verbose" option to print name space;
authorwenzelm
Fri Apr 03 19:56:51 2015 +0200 (2015-04-03 ago)
changeset 599179830c944670f
parent 59916 f673ce6b1e2b
child 59918 d01e6d159c33
more uniform "verbose" option to print name space;
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Isar_Ref/Generic.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Isar_Ref/Misc.thy
src/Doc/Isar_Ref/Spec.thy
src/HOL/Tools/inductive.ML
src/Pure/General/name_space.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_context.ML
src/Pure/Thy/thy_output.ML
src/Pure/display.ML
src/Pure/simplifier.ML
src/Pure/thm.ML
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Apr 03 18:36:19 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Apr 03 19:56:51 2015 +0200
     1.3 @@ -85,6 +85,7 @@
     1.4  
     1.5  text \<open>
     1.6    \begin{matharray}{rcl}
     1.7 +    @{command_def "print_antiquotations"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
     1.8      @{antiquotation_def "theory"} & : & @{text antiquotation} \\
     1.9      @{antiquotation_def "thm"} & : & @{text antiquotation} \\
    1.10      @{antiquotation_def "lemma"} & : & @{text antiquotation} \\
    1.11 @@ -132,6 +133,10 @@
    1.12    antiquotations are checked within the current theory or proof
    1.13    context.
    1.14  
    1.15 +  @{rail \<open>
    1.16 +    @@{command print_antiquotations} ('!'?)
    1.17 +  \<close>}
    1.18 +
    1.19    %% FIXME less monolithic presentation, move to individual sections!?
    1.20    @{rail \<open>
    1.21      '@{' antiquotation '}'
    1.22 @@ -182,7 +187,11 @@
    1.23    text @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"}.
    1.24  
    1.25    \begin{description}
    1.26 -  
    1.27 +
    1.28 +  \item @{command "print_antiquotations"} prints all document antiquotations
    1.29 +  that are defined in the current context; the ``@{text "!"}'' option
    1.30 +  indicates extra verbosity.
    1.31 +
    1.32    \item @{text "@{theory A}"} prints the name @{text "A"}, which is
    1.33    guaranteed to refer to a valid ancestor theory in the current
    1.34    context.
     2.1 --- a/src/Doc/Isar_Ref/Generic.thy	Fri Apr 03 18:36:19 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Fri Apr 03 19:56:51 2015 +0200
     2.3 @@ -37,13 +37,16 @@
     2.4    \end{matharray}
     2.5  
     2.6    @{rail \<open>
     2.7 +    @@{command print_options} ('!'?)
     2.8 +    ;
     2.9      @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
    2.10    \<close>}
    2.11  
    2.12    \begin{description}
    2.13    
    2.14    \item @{command "print_options"} prints the available configuration
    2.15 -  options, with names, types, and current values.
    2.16 +  options, with names, types, and current values; the ``@{text "!"}'' option
    2.17 +  indicates extra verbosity.
    2.18    
    2.19    \item @{text "name = value"} as an attribute expression modifies the
    2.20    named option, with the syntax of the value depending on the option's
    2.21 @@ -611,6 +614,8 @@
    2.22    @{rail \<open>
    2.23      (@@{attribute simp} | @@{attribute split} | @@{attribute cong})
    2.24        (() | 'add' | 'del')
    2.25 +    ;
    2.26 +    @@{command print_simpset} ('!'?)
    2.27    \<close>}
    2.28  
    2.29    \begin{description}
    2.30 @@ -716,9 +721,9 @@
    2.31    This can make simplification much faster, but may require an extra
    2.32    case split over the condition @{text "?q"} to prove the goal.
    2.33  
    2.34 -  \item @{command "print_simpset"} prints the collection of rules
    2.35 -  declared to the Simplifier, which is also known as ``simpset''
    2.36 -  internally.
    2.37 +  \item @{command "print_simpset"} prints the collection of rules declared
    2.38 +  to the Simplifier, which is also known as ``simpset'' internally; the
    2.39 +  ``@{text "!"}'' option indicates extra verbosity.
    2.40  
    2.41    For historical reasons, simpsets may occur independently from the
    2.42    current context, but are conceptually dependent on it.  When the
     3.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Apr 03 18:36:19 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Apr 03 19:56:51 2015 +0200
     3.3 @@ -105,6 +105,8 @@
     3.4      ;
     3.5      clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
     3.6      ;
     3.7 +    @@{command print_inductives} ('!'?)
     3.8 +    ;
     3.9      @@{attribute (HOL) mono} (() | 'add' | 'del')
    3.10    \<close>}
    3.11  
    3.12 @@ -137,7 +139,7 @@
    3.13    where multiple arguments are simulated via tuples.
    3.14  
    3.15    \item @{command "print_inductives"} prints (co)inductive definitions and
    3.16 -  monotonicity rules.
    3.17 +  monotonicity rules; the ``@{text "!"}'' option indicates extra verbosity.
    3.18  
    3.19    \item @{attribute (HOL) mono} declares monotonicity rules in the
    3.20    context.  These rule are involved in the automated monotonicity
     4.1 --- a/src/Doc/Isar_Ref/Misc.thy	Fri Apr 03 18:36:19 2015 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Misc.thy	Fri Apr 03 19:56:51 2015 +0200
     4.3 @@ -21,9 +21,12 @@
     4.4    \end{matharray}
     4.5  
     4.6    @{rail \<open>
     4.7 -    (@@{command print_theory} | @@{command print_theorems} | @@{command print_facts}) ('!'?)
     4.8 +    (@@{command print_theory} |
     4.9 +      @@{command print_methods} |
    4.10 +      @@{command print_attributes} |
    4.11 +      @@{command print_theorems} |
    4.12 +      @@{command print_facts}) ('!'?)
    4.13      ;
    4.14 -
    4.15      @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * )
    4.16      ;
    4.17      thmcriterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
    4.18 @@ -45,23 +48,24 @@
    4.19  
    4.20    \begin{description}
    4.21    
    4.22 -  \item @{command "print_theory"} prints the main logical content of
    4.23 -  the background theory; the ``@{text "!"}'' option indicates extra
    4.24 +  \item @{command "print_theory"} prints the main logical content of the
    4.25 +  background theory; the ``@{text "!"}'' option indicates extra verbosity.
    4.26 +
    4.27 +  \item @{command "print_methods"} prints all proof methods available in the
    4.28 +  current theory context; the ``@{text "!"}'' option indicates extra
    4.29    verbosity.
    4.30 -
    4.31 -  \item @{command "print_methods"} prints all proof methods
    4.32 -  available in the current theory context.
    4.33    
    4.34 -  \item @{command "print_attributes"} prints all attributes
    4.35 -  available in the current theory context.
    4.36 +  \item @{command "print_attributes"} prints all attributes available in the
    4.37 +  current theory context; the ``@{text "!"}'' option indicates extra
    4.38 +  verbosity.
    4.39    
    4.40 -  \item @{command "print_theorems"} prints theorems of the background
    4.41 -  theory resulting from the last command; the ``@{text "!"}'' option
    4.42 -  indicates extra verbosity.
    4.43 +  \item @{command "print_theorems"} prints theorems of the background theory
    4.44 +  resulting from the last command; the ``@{text "!"}'' option indicates
    4.45 +  extra verbosity.
    4.46    
    4.47 -  \item @{command "print_facts"} prints all local facts of the
    4.48 -  current context, both named and unnamed ones; the ``@{text "!"}''
    4.49 -  option indicates extra verbosity.
    4.50 +  \item @{command "print_facts"} prints all local facts of the current
    4.51 +  context, both named and unnamed ones; the ``@{text "!"}'' option indicates
    4.52 +  extra verbosity.
    4.53    
    4.54    \item @{command "print_term_bindings"} prints all term bindings that
    4.55    are present in the context.
     5.1 --- a/src/Doc/Isar_Ref/Spec.thy	Fri Apr 03 18:36:19 2015 +0200
     5.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Fri Apr 03 19:56:51 2015 +0200
     5.3 @@ -223,6 +223,8 @@
     5.4    @{rail \<open>
     5.5      @@{command bundle} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes}
     5.6      ;
     5.7 +    @@{command print_bundles} ('!'?)
     5.8 +    ;
     5.9      (@@{command include} | @@{command including}) (@{syntax nameref}+)
    5.10      ;
    5.11      @{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
    5.12 @@ -237,8 +239,9 @@
    5.13    into different application contexts; this works analogously to any
    5.14    other local theory specification.
    5.15  
    5.16 -  \item @{command print_bundles} prints the named bundles that are
    5.17 -  available in the current context.
    5.18 +  \item @{command print_bundles} prints the named bundles that are available
    5.19 +  in the current context; the ``@{text "!"}'' option indicates extra
    5.20 +  verbosity.
    5.21  
    5.22    \item @{command include}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} includes the declarations
    5.23    from the given bundles into the current proof body context.  This is
    5.24 @@ -290,8 +293,9 @@
    5.25      @@{command abbreviation} @{syntax mode}? \<newline>
    5.26        (decl @'where')? @{syntax prop}
    5.27      ;
    5.28 -
    5.29      decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
    5.30 +    ;
    5.31 +    @@{command print_abbrevs} ('!'?)
    5.32    \<close>}
    5.33  
    5.34    \begin{description}
    5.35 @@ -330,8 +334,8 @@
    5.36    declared for abbreviations, cf.\ @{command "syntax"} in
    5.37    \secref{sec:syn-trans}.
    5.38    
    5.39 -  \item @{command "print_abbrevs"} prints all constant abbreviations
    5.40 -  of the current context.
    5.41 +  \item @{command "print_abbrevs"} prints all constant abbreviations of the
    5.42 +  current context; the ``@{text "!"}'' option indicates extra verbosity.
    5.43    
    5.44    \end{description}
    5.45  \<close>
    5.46 @@ -520,6 +524,8 @@
    5.47      ;
    5.48      @@{command print_locale} '!'? @{syntax nameref}
    5.49      ;
    5.50 +    @@{command print_locales} ('!'?)
    5.51 +    ;
    5.52      @{syntax_def locale}: @{syntax context_elem}+ |
    5.53        @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
    5.54      ;
    5.55 @@ -626,8 +632,8 @@
    5.56    elements by default.  Use @{command "print_locale"}@{text "!"} to
    5.57    have them included.
    5.58  
    5.59 -  \item @{command "print_locales"} prints the names of all locales
    5.60 -  of the current theory.
    5.61 +  \item @{command "print_locales"} prints the names of all locales of the
    5.62 +  current theory; the ``@{text "!"}'' option indicates extra verbosity.
    5.63  
    5.64    \item @{command "locale_deps"} visualizes all locales and their
    5.65    relations as a Hasse diagram. This includes locales defined as type
     6.1 --- a/src/HOL/Tools/inductive.ML	Fri Apr 03 18:36:19 2015 +0200
     6.2 +++ b/src/HOL/Tools/inductive.ML	Fri Apr 03 19:56:51 2015 +0200
     6.3 @@ -26,7 +26,7 @@
     6.4    val transform_result: morphism -> inductive_result -> inductive_result
     6.5    type inductive_info = {names: string list, coind: bool} * inductive_result
     6.6    val the_inductive: Proof.context -> string -> inductive_info
     6.7 -  val print_inductives: Proof.context -> unit
     6.8 +  val print_inductives: bool -> Proof.context -> unit
     6.9    val get_monos: Proof.context -> thm list
    6.10    val mono_add: attribute
    6.11    val mono_del: attribute
    6.12 @@ -227,7 +227,7 @@
    6.13  
    6.14  fun rep_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data rep => rep);
    6.15  
    6.16 -fun print_inductives ctxt =
    6.17 +fun print_inductives verbose ctxt =
    6.18    let
    6.19      val {infos, monos, ...} = rep_data ctxt;
    6.20      val space = Consts.space_of (Proof_Context.consts_of ctxt);
    6.21 @@ -235,7 +235,8 @@
    6.22      [Pretty.block
    6.23        (Pretty.breaks
    6.24          (Pretty.str "(co)inductives:" ::
    6.25 -          map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))),
    6.26 +          map (Pretty.mark_str o #1)
    6.27 +            (Name_Space.markup_entries verbose ctxt space (Symtab.dest infos)))),
    6.28       Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
    6.29    end |> Pretty.writeln_chunks;
    6.30  
    6.31 @@ -1190,7 +1191,7 @@
    6.32  val _ =
    6.33    Outer_Syntax.command @{command_spec "print_inductives"}
    6.34      "print (co)inductive definitions and monotonicity rules"
    6.35 -    (Scan.succeed (Toplevel.unknown_context o
    6.36 -      Toplevel.keep (print_inductives o Toplevel.context_of)));
    6.37 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
    6.38 +      Toplevel.keep (print_inductives b o Toplevel.context_of)));
    6.39  
    6.40  end;
     7.1 --- a/src/Pure/General/name_space.ML	Fri Apr 03 18:36:19 2015 +0200
     7.2 +++ b/src/Pure/General/name_space.ML	Fri Apr 03 19:56:51 2015 +0200
     7.3 @@ -79,10 +79,12 @@
     7.4    val merge_tables: 'a table * 'a table -> 'a table
     7.5    val join_tables: (string -> 'a * 'a -> 'a) (*exception Change_Table.SAME*) ->
     7.6      'a table * 'a table -> 'a table
     7.7 -  val extern_entries: Proof.context -> T -> (string * 'a) list -> ((string * xstring) * 'a) list
     7.8 -  val markup_entries: Proof.context -> T -> (string * 'a) list -> ((Markup.T * xstring) * 'a) list
     7.9 -  val extern_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
    7.10 -  val markup_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
    7.11 +  val extern_entries: bool -> Proof.context -> T -> (string * 'a) list ->
    7.12 +    ((string * xstring) * 'a) list
    7.13 +  val markup_entries: bool -> Proof.context -> T -> (string * 'a) list ->
    7.14 +    ((Markup.T * xstring) * 'a) list
    7.15 +  val extern_table: bool -> Proof.context -> 'a table -> ((string * xstring) * 'a) list
    7.16 +  val markup_table: bool -> Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
    7.17  end;
    7.18  
    7.19  structure Name_Space: NAME_SPACE =
    7.20 @@ -569,15 +571,20 @@
    7.21  
    7.22  (* present table content *)
    7.23  
    7.24 -fun extern_entries ctxt space entries =
    7.25 -  fold (fn (name, x) => cons ((name, extern ctxt space name), x)) entries []
    7.26 +fun extern_entries verbose ctxt space entries =
    7.27 +  fold (fn (name, x) =>
    7.28 +    (verbose orelse not (is_concealed space name)) ?
    7.29 +      cons ((name, extern ctxt space name), x)) entries []
    7.30    |> Library.sort_wrt (#2 o #1);
    7.31  
    7.32 -fun markup_entries ctxt space entries =
    7.33 -  extern_entries ctxt space entries
    7.34 +fun markup_entries verbose ctxt space entries =
    7.35 +  extern_entries verbose ctxt space entries
    7.36    |> map (fn ((name, xname), x) => ((markup space name, xname), x));
    7.37  
    7.38 -fun extern_table ctxt (Table (space, tab)) = extern_entries ctxt space (Change_Table.dest tab);
    7.39 -fun markup_table ctxt (Table (space, tab)) = markup_entries ctxt space (Change_Table.dest tab);
    7.40 +fun extern_table verbose ctxt (Table (space, tab)) =
    7.41 +  extern_entries verbose ctxt space (Change_Table.dest tab);
    7.42 +
    7.43 +fun markup_table verbose ctxt (Table (space, tab)) =
    7.44 +  markup_entries verbose ctxt space (Change_Table.dest tab);
    7.45  
    7.46  end;
     8.1 --- a/src/Pure/Isar/attrib.ML	Fri Apr 03 18:36:19 2015 +0200
     8.2 +++ b/src/Pure/Isar/attrib.ML	Fri Apr 03 19:56:51 2015 +0200
     8.3 @@ -9,7 +9,7 @@
     8.4    type binding = binding * Token.src list
     8.5    val empty_binding: binding
     8.6    val is_empty_binding: binding -> bool
     8.7 -  val print_attributes: Proof.context -> unit
     8.8 +  val print_attributes: bool -> Proof.context -> unit
     8.9    val define_global: Binding.binding -> (Token.src -> attribute) ->
    8.10      string -> theory -> string * theory
    8.11    val define: Binding.binding -> (Token.src -> attribute) ->
    8.12 @@ -56,7 +56,7 @@
    8.13    val partial_evaluation: Proof.context ->
    8.14      (binding * (thm list * Token.src list) list) list ->
    8.15      (binding * (thm list * Token.src list) list) list
    8.16 -  val print_options: Proof.context -> unit
    8.17 +  val print_options: bool -> Proof.context -> unit
    8.18    val config_bool: Binding.binding ->
    8.19      (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    8.20    val config_int: Binding.binding ->
    8.21 @@ -111,7 +111,7 @@
    8.22      val attribs' = Name_Space.merge_tables (attribs0, get_attributes ctxt);
    8.23    in Context.proof_map (Attributes.put attribs') ctxt end;
    8.24  
    8.25 -fun print_attributes ctxt =
    8.26 +fun print_attributes verbose ctxt =
    8.27    let
    8.28      val attribs = get_attributes ctxt;
    8.29      fun prt_attr (name, (_, "")) = Pretty.mark_str name
    8.30 @@ -119,7 +119,7 @@
    8.31            Pretty.block
    8.32              (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
    8.33    in
    8.34 -    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table ctxt attribs))]
    8.35 +    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table verbose ctxt attribs))]
    8.36      |> Pretty.writeln_chunks
    8.37    end;
    8.38  
    8.39 @@ -387,7 +387,7 @@
    8.40    fun merge data = Symtab.merge (K true) data;
    8.41  );
    8.42  
    8.43 -fun print_options ctxt =
    8.44 +fun print_options verbose ctxt =
    8.45    let
    8.46      fun prt (name, config) =
    8.47        let val value = Config.get ctxt config in
    8.48 @@ -396,7 +396,7 @@
    8.49        end;
    8.50      val space = attribute_space ctxt;
    8.51      val configs =
    8.52 -      Name_Space.markup_entries ctxt space
    8.53 +      Name_Space.markup_entries verbose ctxt space
    8.54          (Symtab.dest (Configs.get (Proof_Context.theory_of ctxt)));
    8.55    in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
    8.56  
     9.1 --- a/src/Pure/Isar/bundle.ML	Fri Apr 03 18:36:19 2015 +0200
     9.2 +++ b/src/Pure/Isar/bundle.ML	Fri Apr 03 19:56:51 2015 +0200
     9.3 @@ -24,7 +24,7 @@
     9.4      generic_theory -> Binding.scope * local_theory
     9.5    val context_cmd: (xstring * Position.T) list -> Element.context list ->
     9.6      generic_theory -> Binding.scope * local_theory
     9.7 -  val print_bundles: Proof.context -> unit
     9.8 +  val print_bundles: bool -> Proof.context -> unit
     9.9  end;
    9.10  
    9.11  structure Bundle: BUNDLE =
    9.12 @@ -122,7 +122,7 @@
    9.13  
    9.14  (* print_bundles *)
    9.15  
    9.16 -fun print_bundles ctxt =
    9.17 +fun print_bundles verbose ctxt =
    9.18    let
    9.19      val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    9.20  
    9.21 @@ -134,7 +134,7 @@
    9.22        Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name ::
    9.23          Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
    9.24    in
    9.25 -    map prt_bundle (Name_Space.markup_table ctxt (get_bundles ctxt))
    9.26 +    map prt_bundle (Name_Space.markup_table verbose ctxt (get_bundles ctxt))
    9.27    end |> Pretty.writeln_chunks;
    9.28  
    9.29  end;
    10.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Apr 03 18:36:19 2015 +0200
    10.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 03 19:56:51 2015 +0200
    10.3 @@ -257,7 +257,7 @@
    10.4  
    10.5  fun pretty_theorems verbose st =
    10.6    if Toplevel.is_proof st then
    10.7 -    Proof_Context.pretty_local_facts (Toplevel.context_of st) verbose
    10.8 +    Proof_Context.pretty_local_facts verbose (Toplevel.context_of st)
    10.9    else
   10.10      let
   10.11        val thy = Toplevel.theory_of st;
    11.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 03 18:36:19 2015 +0200
    11.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 03 19:56:51 2015 +0200
    11.3 @@ -350,8 +350,8 @@
    11.4  val _ =
    11.5    Outer_Syntax.command @{command_spec "print_bundles"}
    11.6      "print bundles of declarations"
    11.7 -    (Scan.succeed (Toplevel.unknown_context o
    11.8 -      Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
    11.9 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
   11.10 +      Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
   11.11  
   11.12  
   11.13  (* local theories *)
   11.14 @@ -681,8 +681,6 @@
   11.15  val opt_modes =
   11.16    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
   11.17  
   11.18 -val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
   11.19 -
   11.20  val _ =
   11.21    Outer_Syntax.command @{command_spec "help"}
   11.22      "retrieve outer syntax commands according to name patterns"
   11.23 @@ -695,8 +693,8 @@
   11.24  
   11.25  val _ =
   11.26    Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
   11.27 -    (Scan.succeed (Toplevel.unknown_context o
   11.28 -      Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
   11.29 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
   11.30 +      Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
   11.31  
   11.32  val _ =
   11.33    Outer_Syntax.command @{command_spec "print_context"}
   11.34 @@ -705,13 +703,13 @@
   11.35  
   11.36  val _ =
   11.37    Outer_Syntax.command @{command_spec "print_theory"}
   11.38 -    "print logical theory contents (verbose!)"
   11.39 -    (opt_bang >> (fn b => Toplevel.unknown_theory o
   11.40 +    "print logical theory contents"
   11.41 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
   11.42        Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
   11.43  
   11.44  val _ =
   11.45    Outer_Syntax.command @{command_spec "print_syntax"}
   11.46 -    "print inner syntax of context (verbose!)"
   11.47 +    "print inner syntax of context"
   11.48      (Scan.succeed (Toplevel.unknown_context o
   11.49        Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
   11.50  
   11.51 @@ -724,21 +722,21 @@
   11.52  val _ =
   11.53    Outer_Syntax.command @{command_spec "print_abbrevs"}
   11.54      "print constant abbreviations of context"
   11.55 -    (Scan.succeed (Toplevel.unknown_context o
   11.56 -      Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
   11.57 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
   11.58 +      Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
   11.59  
   11.60  val _ =
   11.61    Outer_Syntax.command @{command_spec "print_theorems"}
   11.62      "print theorems of local theory or proof context"
   11.63 -    (opt_bang >> (fn b =>
   11.64 +    (Parse.opt_bang >> (fn b =>
   11.65        Toplevel.unknown_context o
   11.66        Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
   11.67  
   11.68  val _ =
   11.69    Outer_Syntax.command @{command_spec "print_locales"}
   11.70      "print locales of this theory"
   11.71 -    (Scan.succeed (Toplevel.unknown_theory o
   11.72 -      Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
   11.73 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
   11.74 +      Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
   11.75  
   11.76  val _ =
   11.77    Outer_Syntax.command @{command_spec "print_classes"}
   11.78 @@ -749,7 +747,7 @@
   11.79  val _ =
   11.80    Outer_Syntax.command @{command_spec "print_locale"}
   11.81      "print locale of this theory"
   11.82 -    (opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
   11.83 +    (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
   11.84        Toplevel.unknown_theory o
   11.85        Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
   11.86  
   11.87 @@ -763,21 +761,21 @@
   11.88  val _ =
   11.89    Outer_Syntax.command @{command_spec "print_dependencies"}
   11.90      "print dependencies of locale expression"
   11.91 -    (opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
   11.92 +    (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
   11.93        Toplevel.unknown_context o
   11.94        Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
   11.95  
   11.96  val _ =
   11.97    Outer_Syntax.command @{command_spec "print_attributes"}
   11.98      "print attributes of this theory"
   11.99 -    (Scan.succeed (Toplevel.unknown_theory o
  11.100 -      Toplevel.keep (Attrib.print_attributes o Toplevel.context_of)));
  11.101 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  11.102 +      Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
  11.103  
  11.104  val _ =
  11.105    Outer_Syntax.command @{command_spec "print_simpset"}
  11.106      "print context of Simplifier"
  11.107 -    (Scan.succeed (Toplevel.unknown_context o
  11.108 -      Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset o Toplevel.context_of)));
  11.109 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  11.110 +      Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
  11.111  
  11.112  val _ =
  11.113    Outer_Syntax.command @{command_spec "print_rules"} "print intro/elim rules"
  11.114 @@ -786,20 +784,20 @@
  11.115  
  11.116  val _ =
  11.117    Outer_Syntax.command @{command_spec "print_methods"} "print methods of this theory"
  11.118 -    (Scan.succeed (Toplevel.unknown_theory o
  11.119 -      Toplevel.keep (Method.print_methods o Toplevel.context_of)));
  11.120 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
  11.121 +      Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
  11.122  
  11.123  val _ =
  11.124    Outer_Syntax.command @{command_spec "print_antiquotations"}
  11.125      "print document antiquotations"
  11.126 -    (Scan.succeed (Toplevel.unknown_context o
  11.127 -      Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
  11.128 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  11.129 +      Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
  11.130  
  11.131  val _ =
  11.132    Outer_Syntax.command @{command_spec "print_ML_antiquotations"}
  11.133      "print ML antiquotations"
  11.134 -    (Scan.succeed (Toplevel.unknown_context o
  11.135 -      Toplevel.keep (ML_Context.print_antiquotations o Toplevel.context_of)));
  11.136 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  11.137 +      Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
  11.138  
  11.139  val _ =
  11.140    Outer_Syntax.command @{command_spec "thy_deps"} "visualize theory dependencies"
  11.141 @@ -818,8 +816,8 @@
  11.142  
  11.143  val _ =
  11.144    Outer_Syntax.command @{command_spec "print_facts"} "print facts of proof context"
  11.145 -    (opt_bang >> (fn verbose => Toplevel.unknown_context o
  11.146 -      Toplevel.keep (fn st => Proof_Context.print_local_facts (Toplevel.context_of st) verbose)));
  11.147 +    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
  11.148 +      Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
  11.149  
  11.150  val _ =
  11.151    Outer_Syntax.command @{command_spec "print_cases"} "print cases of proof context"
    12.1 --- a/src/Pure/Isar/locale.ML	Fri Apr 03 18:36:19 2015 +0200
    12.2 +++ b/src/Pure/Isar/locale.ML	Fri Apr 03 19:56:51 2015 +0200
    12.3 @@ -84,7 +84,7 @@
    12.4  
    12.5    (* Diagnostic *)
    12.6    val hyp_spec_of: theory -> string -> Element.context_i list
    12.7 -  val print_locales: theory -> unit
    12.8 +  val print_locales: bool -> theory -> unit
    12.9    val print_locale: theory -> bool -> xstring * Position.T -> unit
   12.10    val print_registrations: Proof.context -> xstring * Position.T -> unit
   12.11    val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
   12.12 @@ -653,12 +653,12 @@
   12.13  
   12.14  fun hyp_spec_of thy = #hyp_spec o the_locale thy;
   12.15  
   12.16 -fun print_locales thy =
   12.17 +fun print_locales verbose thy =
   12.18    Pretty.block
   12.19      (Pretty.breaks
   12.20        (Pretty.str "locales:" ::
   12.21          map (Pretty.mark_str o #1)
   12.22 -          (Name_Space.markup_table (Proof_Context.init_global thy) (Locales.get thy))))
   12.23 +          (Name_Space.markup_table verbose (Proof_Context.init_global thy) (Locales.get thy))))
   12.24    |> Pretty.writeln;
   12.25  
   12.26  fun pretty_locale thy show_facts name =
    13.1 --- a/src/Pure/Isar/method.ML	Fri Apr 03 18:36:19 2015 +0200
    13.2 +++ b/src/Pure/Isar/method.ML	Fri Apr 03 19:56:51 2015 +0200
    13.3 @@ -54,7 +54,7 @@
    13.4    val done_text: text
    13.5    val sorry_text: bool -> text
    13.6    val finish_text: text option * bool -> text
    13.7 -  val print_methods: Proof.context -> unit
    13.8 +  val print_methods: bool -> Proof.context -> unit
    13.9    val check_name: Proof.context -> xstring * Position.T -> string
   13.10    val check_src: Proof.context -> Token.src -> Token.src
   13.11    val method_syntax: (Proof.context -> method) context_parser ->
   13.12 @@ -333,7 +333,7 @@
   13.13      val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt));
   13.14    in Context.proof_map (map_methods (K meths')) ctxt end;
   13.15  
   13.16 -fun print_methods ctxt =
   13.17 +fun print_methods verbose ctxt =
   13.18    let
   13.19      val meths = get_methods (Context.Proof ctxt);
   13.20      fun prt_meth (name, (_, "")) = Pretty.mark_str name
   13.21 @@ -341,7 +341,7 @@
   13.22            Pretty.block
   13.23              (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   13.24    in
   13.25 -    [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))]
   13.26 +    [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table verbose ctxt meths))]
   13.27      |> Pretty.writeln_chunks
   13.28    end;
   13.29  
    14.1 --- a/src/Pure/Isar/parse.ML	Fri Apr 03 18:36:19 2015 +0200
    14.2 +++ b/src/Pure/Isar/parse.ML	Fri Apr 03 19:56:51 2015 +0200
    14.3 @@ -46,6 +46,7 @@
    14.4    val tags: string list parser
    14.5    val opt_unit: unit parser
    14.6    val opt_keyword: string -> bool parser
    14.7 +  val opt_bang: bool parser
    14.8    val begin: string parser
    14.9    val opt_begin: bool parser
   14.10    val nat: int parser
   14.11 @@ -231,6 +232,7 @@
   14.12  
   14.13  val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
   14.14  fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
   14.15 +val opt_bang = Scan.optional ($$$ "!" >> K true) false;
   14.16  
   14.17  val begin = $$$ "begin";
   14.18  val opt_begin = Scan.optional (begin >> K true) false;
   14.19 @@ -460,4 +462,3 @@
   14.20  val xthms1 = Scan.repeat1 xthm;
   14.21  
   14.22  end;
   14.23 -
    15.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 03 18:36:19 2015 +0200
    15.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Apr 03 19:56:51 2015 +0200
    15.3 @@ -167,10 +167,10 @@
    15.4      (term * term) * Context.generic
    15.5    val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
    15.6    val print_syntax: Proof.context -> unit
    15.7 -  val print_abbrevs: Proof.context -> unit
    15.8 +  val print_abbrevs: bool -> Proof.context -> unit
    15.9    val pretty_term_bindings: Proof.context -> Pretty.T list
   15.10 -  val pretty_local_facts: Proof.context -> bool -> Pretty.T list
   15.11 -  val print_local_facts: Proof.context -> bool -> unit
   15.12 +  val pretty_local_facts: bool -> Proof.context -> Pretty.T list
   15.13 +  val print_local_facts: bool -> Proof.context -> unit
   15.14    val pretty_cases: Proof.context -> Pretty.T list
   15.15    val debug: bool Config.T
   15.16    val verbose: bool Config.T
   15.17 @@ -1276,7 +1276,7 @@
   15.18  
   15.19  (* abbreviations *)
   15.20  
   15.21 -fun pretty_abbrevs show_globals ctxt =
   15.22 +fun pretty_abbrevs verbose show_globals ctxt =
   15.23    let
   15.24      val space = const_space ctxt;
   15.25      val (constants, global_constants) =
   15.26 @@ -1286,13 +1286,13 @@
   15.27        | add_abbr (c, (T, SOME t)) =
   15.28            if not show_globals andalso Symtab.defined globals c then I
   15.29            else cons (c, Logic.mk_equals (Const (c, T), t));
   15.30 -    val abbrevs = Name_Space.markup_entries ctxt space (fold add_abbr constants []);
   15.31 +    val abbrevs = Name_Space.markup_entries verbose ctxt space (fold add_abbr constants []);
   15.32    in
   15.33      if null abbrevs then []
   15.34      else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
   15.35    end;
   15.36  
   15.37 -val print_abbrevs = Pretty.writeln_chunks o pretty_abbrevs true;
   15.38 +fun print_abbrevs verbose = Pretty.writeln_chunks o pretty_abbrevs verbose true;
   15.39  
   15.40  
   15.41  (* term bindings *)
   15.42 @@ -1309,7 +1309,7 @@
   15.43  
   15.44  (* local facts *)
   15.45  
   15.46 -fun pretty_local_facts ctxt verbose =
   15.47 +fun pretty_local_facts verbose ctxt =
   15.48    let
   15.49      val facts = facts_of ctxt;
   15.50      val props = Facts.props facts;
   15.51 @@ -1323,8 +1323,8 @@
   15.52          (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
   15.53    end;
   15.54  
   15.55 -fun print_local_facts ctxt verbose =
   15.56 -  Pretty.writeln_chunks (pretty_local_facts ctxt verbose);
   15.57 +fun print_local_facts verbose ctxt =
   15.58 +  Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
   15.59  
   15.60  
   15.61  (* local contexts *)
   15.62 @@ -1447,9 +1447,9 @@
   15.63    in
   15.64      verb single (K pretty_thy) @
   15.65      pretty_ctxt ctxt @
   15.66 -    verb (pretty_abbrevs false) (K ctxt) @
   15.67 +    verb (pretty_abbrevs true false) (K ctxt) @
   15.68      verb pretty_term_bindings (K ctxt) @
   15.69 -    verb (pretty_local_facts ctxt) (K true) @
   15.70 +    verb (pretty_local_facts true) (K ctxt) @
   15.71      verb pretty_cases (K ctxt) @
   15.72      verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
   15.73      verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
   15.74 @@ -1458,4 +1458,3 @@
   15.75  end;
   15.76  
   15.77  val show_abbrevs = Proof_Context.show_abbrevs;
   15.78 -
    16.1 --- a/src/Pure/ML/ml_context.ML	Fri Apr 03 18:36:19 2015 +0200
    16.2 +++ b/src/Pure/ML/ml_context.ML	Fri Apr 03 19:56:51 2015 +0200
    16.3 @@ -19,7 +19,7 @@
    16.4    val value_decl: string -> string -> Proof.context -> decl * Proof.context
    16.5    val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
    16.6      theory -> theory
    16.7 -  val print_antiquotations: Proof.context -> unit
    16.8 +  val print_antiquotations: bool -> Proof.context -> unit
    16.9    val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   16.10    val eval_file: ML_Compiler.flags -> Path.T -> unit
   16.11    val eval_source: ML_Compiler.flags -> Input.source -> unit
   16.12 @@ -102,9 +102,9 @@
   16.13  fun add_antiquotation name f thy = thy
   16.14    |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
   16.15  
   16.16 -fun print_antiquotations ctxt =
   16.17 +fun print_antiquotations verbose ctxt =
   16.18    Pretty.big_list "ML antiquotations:"
   16.19 -    (map (Pretty.mark_str o #1) (Name_Space.markup_table ctxt (get_antiquotations ctxt)))
   16.20 +    (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt)))
   16.21    |> Pretty.writeln;
   16.22  
   16.23  fun apply_antiquotation src ctxt =
    17.1 --- a/src/Pure/Thy/thy_output.ML	Fri Apr 03 18:36:19 2015 +0200
    17.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Apr 03 19:56:51 2015 +0200
    17.3 @@ -17,7 +17,7 @@
    17.4    val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
    17.5    val check_command: Proof.context -> xstring * Position.T -> string
    17.6    val check_option: Proof.context -> xstring * Position.T -> string
    17.7 -  val print_antiquotations: Proof.context -> unit
    17.8 +  val print_antiquotations: bool -> Proof.context -> unit
    17.9    val antiquotation: binding -> 'a context_parser ->
   17.10      ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
   17.11        theory -> theory
   17.12 @@ -104,11 +104,11 @@
   17.13        Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
   17.14    in opt s ctxt end;
   17.15  
   17.16 -fun print_antiquotations ctxt =
   17.17 +fun print_antiquotations verbose ctxt =
   17.18    let
   17.19      val (commands, options) = get_antiquotations ctxt;
   17.20 -    val command_names = map #1 (Name_Space.markup_table ctxt commands);
   17.21 -    val option_names = map #1 (Name_Space.markup_table ctxt options);
   17.22 +    val command_names = map #1 (Name_Space.markup_table verbose ctxt commands);
   17.23 +    val option_names = map #1 (Name_Space.markup_table verbose ctxt options);
   17.24    in
   17.25      [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
   17.26       Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
    18.1 --- a/src/Pure/display.ML	Fri Apr 03 18:36:19 2015 +0200
    18.2 +++ b/src/Pure/display.ML	Fri Apr 03 19:56:51 2015 +0200
    18.3 @@ -157,25 +157,22 @@
    18.4      val arities = Sorts.arities_of class_algebra;
    18.5  
    18.6      val clsses =
    18.7 -      Name_Space.extern_entries ctxt class_space
    18.8 +      Name_Space.extern_entries verbose ctxt class_space
    18.9          (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
   18.10        |> map (apfst #1);
   18.11 -    val tdecls = Name_Space.extern_table ctxt types |> map (apfst #1);
   18.12 +    val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1);
   18.13      val arties =
   18.14 -      Name_Space.extern_entries ctxt (Type.type_space tsig) (Symtab.dest arities)
   18.15 +      Name_Space.extern_entries verbose ctxt (Type.type_space tsig) (Symtab.dest arities)
   18.16        |> map (apfst #1);
   18.17  
   18.18 +    val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
   18.19 +    val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   18.20 +    val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   18.21 +    val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
   18.22 +
   18.23 +    val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
   18.24 +
   18.25      fun prune_const c = not verbose andalso Consts.is_concealed consts c;
   18.26 -    val cnsts =
   18.27 -      Name_Space.markup_entries ctxt const_space
   18.28 -        (filter_out (prune_const o fst) constants);
   18.29 -
   18.30 -    val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   18.31 -    val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   18.32 -    val cnstrs = Name_Space.markup_entries ctxt const_space constraints;
   18.33 -
   18.34 -    val axms = Name_Space.markup_table ctxt (Theory.axiom_table thy);
   18.35 -
   18.36      val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
   18.37        |> map (fn (lhs, rhs) =>
   18.38          (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
   18.39 @@ -195,7 +192,8 @@
   18.40        Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
   18.41        Pretty.big_list "axioms:" (map pretty_axm axms),
   18.42        Pretty.block
   18.43 -        (Pretty.breaks (Pretty.str "oracles:" :: map Pretty.mark_str (Thm.extern_oracles ctxt))),
   18.44 +        (Pretty.breaks (Pretty.str "oracles:" ::
   18.45 +          map Pretty.mark_str (Thm.extern_oracles verbose ctxt))),
   18.46        Pretty.big_list "definitions:"
   18.47          [pretty_finals reds0,
   18.48           Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
    19.1 --- a/src/Pure/simplifier.ML	Fri Apr 03 18:36:19 2015 +0200
    19.2 +++ b/src/Pure/simplifier.ML	Fri Apr 03 19:56:51 2015 +0200
    19.3 @@ -42,7 +42,7 @@
    19.4    val def_simproc_cmd: {name: binding, lhss: string list,
    19.5      proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
    19.6      local_theory -> local_theory
    19.7 -  val pretty_simpset: Proof.context -> Pretty.T
    19.8 +  val pretty_simpset: bool -> Proof.context -> Pretty.T
    19.9    val default_mk_sym: Proof.context -> thm -> thm option
   19.10    val prems_of: Proof.context -> thm list
   19.11    val add_simp: thm -> Proof.context -> Proof.context
   19.12 @@ -158,7 +158,7 @@
   19.13  
   19.14  (** pretty_simpset **)
   19.15  
   19.16 -fun pretty_simpset ctxt =
   19.17 +fun pretty_simpset verbose ctxt =
   19.18    let
   19.19      val pretty_term = Syntax.pretty_term ctxt;
   19.20      val pretty_thm = Display.pretty_thm ctxt;
   19.21 @@ -177,7 +177,7 @@
   19.22      val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
   19.23        dest_ss (simpset_of ctxt);
   19.24      val simprocs =
   19.25 -      Name_Space.markup_entries ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
   19.26 +      Name_Space.markup_entries verbose ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
   19.27    in
   19.28      [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
   19.29        Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
    20.1 --- a/src/Pure/thm.ML	Fri Apr 03 18:36:19 2015 +0200
    20.2 +++ b/src/Pure/thm.ML	Fri Apr 03 19:56:51 2015 +0200
    20.3 @@ -137,7 +137,7 @@
    20.4      bool * thm * int -> int -> thm -> thm Seq.seq
    20.5    val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
    20.6    (*oracles*)
    20.7 -  val extern_oracles: Proof.context -> (Markup.T * xstring) list
    20.8 +  val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list
    20.9    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   20.10  end;
   20.11  
   20.12 @@ -1750,8 +1750,8 @@
   20.13    fun merge data : T = Name_Space.merge_tables data;
   20.14  );
   20.15  
   20.16 -fun extern_oracles ctxt =
   20.17 -  map #1 (Name_Space.markup_table ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
   20.18 +fun extern_oracles verbose ctxt =
   20.19 +  map #1 (Name_Space.markup_table verbose ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
   20.20  
   20.21  fun add_oracle (b, oracle) thy =
   20.22    let
    21.1 --- a/src/Tools/Code/code_preproc.ML	Fri Apr 03 18:36:19 2015 +0200
    21.2 +++ b/src/Tools/Code/code_preproc.ML	Fri Apr 03 19:56:51 2015 +0200
    21.3 @@ -227,12 +227,12 @@
    21.4        Pretty.block [
    21.5          Pretty.str "preprocessing simpset:",
    21.6          Pretty.fbrk,
    21.7 -        Simplifier.pretty_simpset (put_simpset pre ctxt)
    21.8 +        Simplifier.pretty_simpset true (put_simpset pre ctxt)
    21.9        ],
   21.10        Pretty.block [
   21.11          Pretty.str "postprocessing simpset:",
   21.12          Pretty.fbrk,
   21.13 -        Simplifier.pretty_simpset (put_simpset post ctxt)
   21.14 +        Simplifier.pretty_simpset true (put_simpset post ctxt)
   21.15        ],
   21.16        Pretty.block (
   21.17          Pretty.str "function transformers:"