help_antiquotations;
authorwenzelm
Fri Jun 30 21:21:11 2000 +0200 (2000-06-30)
changeset 92132651a4db8883
parent 9212 4afe62073b41
child 9214 9454f30eacc7
help_antiquotations;
src/Pure/Isar/isar_output.ML
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/isar_output.ML	Fri Jun 30 17:51:56 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_output.ML	Fri Jun 30 21:21:11 2000 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  sig
     1.5    val add_commands: (string * (Args.src -> Proof.context -> string)) list -> unit
     1.6    val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
     1.7 +  val help_antiquotations: unit -> Pretty.T list
     1.8    val boolean: string -> bool
     1.9    val integer: string -> int
    1.10    val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.11 @@ -68,6 +69,11 @@
    1.12  fun options [] f = f
    1.13    | options (opt :: opts) f = option opt (options opts f);
    1.14  
    1.15 +
    1.16 +fun help_antiquotations () =
    1.17 + [Pretty.strs ("antiquotation commands:" :: Symtab.keys (! global_commands)),
    1.18 +  Pretty.strs ("antiquotation options:" :: Symtab.keys (! global_options))];
    1.19 +
    1.20  end;
    1.21  
    1.22  
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Jun 30 17:51:56 2000 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Jun 30 21:21:11 2000 +0200
     2.3 @@ -222,6 +222,7 @@
     2.4    Toplevel.keep (fn state =>
     2.5      let val opt_thy = try Toplevel.theory_of state in
     2.6        help_outer_syntax () @
     2.7 +      IsarOutput.help_antiquotations () @
     2.8        Method.help_methods opt_thy @
     2.9        Attrib.help_attributes opt_thy
    2.10        |> Pretty.chunks |> Pretty.writeln