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;