1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 15 17:41:20 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 17 13:57:55 2000 +0200
     1.3 @@ -205,24 +205,26 @@
     1.4    map (fn (name, (((cmt, kind), (int_only, _)), _)) => (name, cmt, kind, int_only))
     1.5      (Symtab.dest (get_parsers ()));
     1.6  
     1.7 -fun print_outer_syntax () =
     1.8 +fun help_outer_syntax () =
     1.9    let
    1.10      fun pretty_cmd (name, comment, _, _) =
    1.11        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.12      val (int_cmds, cmds) = partition #4 (dest_parsers ());
    1.13    in
    1.14 -    Pretty.writeln (Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())));
    1.15 -    Pretty.writeln (Pretty.big_list "proper commands:" (map pretty_cmd cmds));
    1.16 -    Pretty.writeln (Pretty.big_list "improper commands (interactive-only):"
    1.17 -      (map pretty_cmd int_cmds))
    1.18 +    [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
    1.19 +      Pretty.big_list "proper commands:" (map pretty_cmd cmds),
    1.20 +      Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)]
    1.21    end;
    1.22  
    1.23 +val print_outer_syntax = Pretty.writeln o Pretty.chunks o help_outer_syntax;
    1.24 +
    1.25  val print_help =
    1.26    Toplevel.keep (fn state =>
    1.27      let val opt_thy = try Toplevel.theory_of state in
    1.28 -      print_outer_syntax ();
    1.29 -      Method.help_methods opt_thy;
    1.30 +      help_outer_syntax () @
    1.31 +      Method.help_methods opt_thy @
    1.32        Attrib.help_attributes opt_thy
    1.33 +      |> Pretty.chunks |> Pretty.writeln
    1.34      end);
    1.35  
    1.36