# HG changeset patch
# User wenzelm
# Date 1165616753 -3600
# Node ID d64cb19c79e2fa33db59b429f1a1c8af4eb08fa9
# Parent  85722dc0fc815bdddf1e3ee20944de939dbc877c
added 'help' command (same of 'print_commands');

diff -r 85722dc0fc81 -r d64cb19c79e2 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Dec 08 23:25:52 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 08 23:25:53 2006 +0100
@@ -673,8 +673,12 @@
   OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
     K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
 
+val helpP =
+  OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
+    (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
+
 val print_commandsP =
-  OuterSyntax.improper_command "print_commands" "print outer syntax (global)" K.diag
+  OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
 
 val print_contextP =
@@ -933,14 +937,14 @@
   cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
   interpretationP, interpretP,
   (*diagnostic commands*)
-  pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
-  print_syntaxP, print_factsP, print_theoremsP, print_localesP,
-  print_localeP, print_registrationsP, print_attributesP,
-  print_simpsetP, print_rulesP, print_induct_rulesP,
-  print_trans_rulesP, print_methodsP, print_antiquotationsP,
-  class_depsP, thm_depsP, find_theoremsP, print_bindsP, print_casesP,
-  print_stmtsP, print_thmsP, print_prfsP, print_full_prfsP,
-  print_propP, print_termP, print_typeP,
+  pretty_setmarginP, helpP, print_commandsP, print_contextP,
+  print_theoryP, print_syntaxP, print_factsP, print_theoremsP,
+  print_localesP, print_localeP, print_registrationsP,
+  print_attributesP, print_simpsetP, print_rulesP,
+  print_induct_rulesP, print_trans_rulesP, print_methodsP,
+  print_antiquotationsP, class_depsP, thm_depsP, find_theoremsP,
+  print_bindsP, print_casesP, print_stmtsP, print_thmsP, print_prfsP,
+  print_full_prfsP, print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,