help_antiquotations;

--- a/src/Pure/Isar/isar_output.ML	Fri Jun 30 17:51:56 2000 +0200
+++ b/src/Pure/Isar/isar_output.ML	Fri Jun 30 21:21:11 2000 +0200
@@ -10,6 +10,7 @@
 sig
   val add_commands: (string * (Args.src -> Proof.context -> string)) list -> unit
   val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
+  val help_antiquotations: unit -> Pretty.T list
   val boolean: string -> bool
   val integer: string -> int
   val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
@@ -68,6 +69,11 @@
 fun options [] f = f
   | options (opt :: opts) f = option opt (options opts f);
 
+
+fun help_antiquotations () =
+ [Pretty.strs ("antiquotation commands:" :: Symtab.keys (! global_commands)),
+  Pretty.strs ("antiquotation options:" :: Symtab.keys (! global_options))];
+
 end;
 
 

--- a/src/Pure/Isar/outer_syntax.ML	Fri Jun 30 17:51:56 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jun 30 21:21:11 2000 +0200
@@ -222,6 +222,7 @@
   Toplevel.keep (fn state =>
     let val opt_thy = try Toplevel.theory_of state in
       help_outer_syntax () @
+      IsarOutput.help_antiquotations () @
       Method.help_methods opt_thy @
       Attrib.help_attributes opt_thy
       |> Pretty.chunks |> Pretty.writeln