src/Pure/Isar/outer_syntax.ML
changeset 9223 eb752c2fac22
parent 9213 2651a4db8883
child 9552 e3981c1f769d
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Jul 01 19:45:23 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Jul 01 19:45:43 2000 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    val loop: unit -> unit
     1.5    val sync_main: unit -> unit
     1.6    val sync_loop: unit -> unit
     1.7 -  val help: unit -> unit
     1.8  end;
     1.9  
    1.10  signature OUTER_SYNTAX =
    1.11 @@ -53,7 +52,7 @@
    1.12    val dest_keywords: unit -> string list
    1.13    val dest_parsers: unit -> (string * string * string * bool) list
    1.14    val print_outer_syntax: unit -> unit
    1.15 -  val print_help: Toplevel.transition -> Toplevel.transition
    1.16 +  val print_commands: Toplevel.transition -> Toplevel.transition
    1.17    val add_keywords: string list -> unit
    1.18    val add_parsers: parser list -> unit
    1.19    val deps_thy: string -> bool -> Path.T -> string list * Path.T list
    1.20 @@ -205,7 +204,7 @@
    1.21    map (fn (name, (((cmt, kind), (int_only, _)), _)) => (name, cmt, kind, int_only))
    1.22      (Symtab.dest (get_parsers ()));
    1.23  
    1.24 -fun help_outer_syntax () =
    1.25 +fun print_outer_syntax () =
    1.26    let
    1.27      fun pretty_cmd (name, comment, _, _) =
    1.28        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.29 @@ -214,19 +213,10 @@
    1.30      [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
    1.31        Pretty.big_list "proper commands:" (map pretty_cmd cmds),
    1.32        Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)]
    1.33 +    |> Pretty.chunks |> Pretty.writeln
    1.34    end;
    1.35  
    1.36 -val print_outer_syntax = Pretty.writeln o Pretty.chunks o help_outer_syntax;
    1.37 -
    1.38 -val print_help =
    1.39 -  Toplevel.keep (fn state =>
    1.40 -    let val opt_thy = try Toplevel.theory_of state in
    1.41 -      help_outer_syntax () @
    1.42 -      IsarOutput.help_antiquotations () @
    1.43 -      Method.help_methods opt_thy @
    1.44 -      Attrib.help_attributes opt_thy
    1.45 -      |> Pretty.chunks |> Pretty.writeln
    1.46 -    end);
    1.47 +val print_commands = Toplevel.imperative print_outer_syntax;
    1.48  
    1.49  
    1.50  
    1.51 @@ -363,7 +353,7 @@
    1.52  
    1.53  fun help () =
    1.54    writeln ("This is Isabelle's underlying ML system (" ^ ml_system ^ ");\n\
    1.55 -    \invoke 'loop();' to enter the Isar loop.");
    1.56 +    \invoke 'Isar.loop();' to get back to the Isar read-eval-print loop.");
    1.57  
    1.58  
    1.59  (*final declarations of this structure!*)