added 'help' command (same of 'print_commands');
authorwenzelm
Fri Dec 08 23:25:53 2006 +0100 (2006-12-08 ago)
changeset 21714d64cb19c79e2
parent 21713 85722dc0fc81
child 21715 9c19f90272e8
added 'help' command (same of 'print_commands');
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Dec 08 23:25:52 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 08 23:25:53 2006 +0100
     1.3 @@ -673,8 +673,12 @@
     1.4    OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
     1.5      K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
     1.6  
     1.7 +val helpP =
     1.8 +  OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
     1.9 +    (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
    1.10 +
    1.11  val print_commandsP =
    1.12 -  OuterSyntax.improper_command "print_commands" "print outer syntax (global)" K.diag
    1.13 +  OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
    1.14      (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
    1.15  
    1.16  val print_contextP =
    1.17 @@ -933,14 +937,14 @@
    1.18    cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
    1.19    interpretationP, interpretP,
    1.20    (*diagnostic commands*)
    1.21 -  pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    1.22 -  print_syntaxP, print_factsP, print_theoremsP, print_localesP,
    1.23 -  print_localeP, print_registrationsP, print_attributesP,
    1.24 -  print_simpsetP, print_rulesP, print_induct_rulesP,
    1.25 -  print_trans_rulesP, print_methodsP, print_antiquotationsP,
    1.26 -  class_depsP, thm_depsP, find_theoremsP, print_bindsP, print_casesP,
    1.27 -  print_stmtsP, print_thmsP, print_prfsP, print_full_prfsP,
    1.28 -  print_propP, print_termP, print_typeP,
    1.29 +  pretty_setmarginP, helpP, print_commandsP, print_contextP,
    1.30 +  print_theoryP, print_syntaxP, print_factsP, print_theoremsP,
    1.31 +  print_localesP, print_localeP, print_registrationsP,
    1.32 +  print_attributesP, print_simpsetP, print_rulesP,
    1.33 +  print_induct_rulesP, print_trans_rulesP, print_methodsP,
    1.34 +  print_antiquotationsP, class_depsP, thm_depsP, find_theoremsP,
    1.35 +  print_bindsP, print_casesP, print_stmtsP, print_thmsP, print_prfsP,
    1.36 +  print_full_prfsP, print_propP, print_termP, print_typeP,
    1.37    (*system commands*)
    1.38    cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
    1.39    touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,