print_help;

--- a/src/Pure/Isar/attrib.ML	Thu Aug 26 19:01:22 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 26 19:01:58 1999 +0200
@@ -15,6 +15,7 @@
 signature ATTRIB =
 sig
   include BASIC_ATTRIB
+  val help_attributes: theory -> unit
   exception ATTRIB_FAIL of (string * Position.T) * exn
   val global_attribute: theory -> Args.src -> theory attribute
   val local_attribute: theory -> Args.src -> Proof.context attribute
@@ -58,19 +59,23 @@
       attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups =>
         error ("Attempt to merge different versions of attributes " ^ commas_quote dups)};
 
-  fun print _ ({space, attrs}) =
+  fun print_atts verbose ({space, attrs}) =
     let
       fun prt_attr (name, ((_, comment), _)) = Pretty.block
         [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     in
-      Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
+      if not verbose then ()
+      else Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
       Pretty.writeln (Pretty.big_list "attributes:"
         (map prt_attr (NameSpace.cond_extern_table space attrs)))
     end;
+
+   fun print _ = print_atts true;
 end;
 
 structure AttributesData = TheoryDataFun(AttributesDataArgs);
 val print_attributes = AttributesData.print;
+val help_attributes = AttributesDataArgs.print_atts false o AttributesData.get;
 
 
 (* get global / local attributes *)

--- a/src/Pure/Isar/method.ML	Thu Aug 26 19:01:22 1999 +0200
+++ b/src/Pure/Isar/method.ML	Thu Aug 26 19:01:58 1999 +0200
@@ -14,6 +14,7 @@
 signature METHOD =
 sig
   include BASIC_METHOD
+  val help_methods: theory -> unit
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val FINISHED: tactic -> tactic
   val METHOD: (thm list -> tactic) -> Proof.method
@@ -174,19 +175,23 @@
       meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups =>
         error ("Attempt to merge different versions of methods " ^ commas_quote dups)};
 
-  fun print _ {space, meths} =
+  fun print_meths verbose {space, meths} =
     let
       fun prt_meth (name, ((_, comment), _)) = Pretty.block
         [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     in
-      Pretty.writeln (Display.pretty_name_space ("method name space", space));
+      if not verbose then ()
+      else Pretty.writeln (Display.pretty_name_space ("method name space", space));
       Pretty.writeln (Pretty.big_list "methods:"
         (map prt_meth (NameSpace.cond_extern_table space meths)))
     end;
+
+  fun print _ = print_meths true;
 end;
 
 structure MethodsData = TheoryDataFun(MethodsDataArgs);
 val print_methods = MethodsData.print;
+val help_methods = MethodsDataArgs.print_meths false o MethodsData.get;
 
 
 (* get methods *)

--- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 26 19:01:22 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 26 19:01:58 1999 +0200
@@ -46,6 +46,7 @@
   val dest_keywords: unit -> string list
   val dest_parsers: unit -> (string * string * string * bool) list
   val print_outer_syntax: unit -> unit
+  val print_help: Toplevel.transition -> Toplevel.transition
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
   val theory_header: token list -> (string * string list * (string * bool) list) * token list
@@ -191,6 +192,13 @@
       (map pretty_cmd int_cmds))
   end;
 
+val print_help =
+  Toplevel.imperative print_outer_syntax o
+  Toplevel.keep (fn state =>
+    (print_outer_syntax ();
+      Method.help_methods (Toplevel.theory_of state);
+      Attrib.help_attributes (Toplevel.theory_of state)));
+
 
 
 (** read theory **)