tuned msg;
authorwenzelm
Tue, 12 Jan 1999 15:19:09 +0100
changeset 6095 9f75a45384dd
parent 6094 fd0f737b1956
child 6096 3451f9e88528
tuned msg;
src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jan 12 15:18:47 1999 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jan 12 15:19:09 1999 +0100
@@ -85,8 +85,9 @@
     val (int_cmds, cmds) = partition (#1 o #2 o #2) (Symtab.dest (! global_parsers));
   in
     Pretty.writeln (Pretty.strs ("keywords:" :: map quote keywords));
-    Pretty.writeln (Pretty.big_list "general commands:" (map pretty_cmd cmds));
-    Pretty.writeln (Pretty.big_list "interactive commands:" (map pretty_cmd int_cmds))
+    Pretty.writeln (Pretty.big_list "proper commands:" (map pretty_cmd cmds));
+    Pretty.writeln (Pretty.big_list "improper commands (interactive-only):"
+      (map pretty_cmd int_cmds))
   end;