--- 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;