diff -r e98c900540f9 -r 7d4ec8992b23 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Nov 24 11:59:50 1998 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Nov 24 12:00:05 1998 +0100
@@ -21,6 +21,7 @@
   val parser: bool -> string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val print_outer_syntax: unit -> unit
+  val commands: unit -> string list
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
   val get_header: Position.T -> (string, 'a) Source.source -> (bstring * bstring list) option
@@ -71,6 +72,8 @@
 val global_lexicon = ref Scan.empty_lexicon;
 val global_parsers = ref (Symtab.empty: (string * (bool * parser_fn)) Symtab.table);
 
+fun commands () = Symtab.keys (! global_parsers);
+
 
 (* print syntax *)
 
@@ -195,6 +198,5 @@
 
 end;
 
-
 structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
 open BasicOuterSyntax;