700 (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); |
700 (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); |
701 |
701 |
702 val kill_thyP = |
702 val kill_thyP = |
703 OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database" |
703 OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database" |
704 K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); |
704 K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); |
|
705 |
|
706 val display_draftsP = |
|
707 OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" |
|
708 K.diag (Scan.repeat1 P.name >> (Toplevel.no_timing oo IsarCmd.display_drafts)); |
|
709 |
|
710 val print_draftsP = |
|
711 OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" |
|
712 K.diag (Scan.repeat1 P.name >> (Toplevel.no_timing oo IsarCmd.print_drafts)); |
705 |
713 |
706 val opt_limits = |
714 val opt_limits = |
707 Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat); |
715 Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat); |
708 |
716 |
709 val prP = |
717 val prP = |
785 print_casesP, print_introsP, print_thmsP, print_prfsP, print_full_prfsP, |
793 print_casesP, print_introsP, print_thmsP, print_prfsP, print_full_prfsP, |
786 print_propP, print_termP, print_typeP, |
794 print_propP, print_termP, print_typeP, |
787 (*system commands*) |
795 (*system commands*) |
788 cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, |
796 cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, |
789 touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, |
797 touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, |
790 kill_thyP, prP, disable_prP, enable_prP, commitP, quitP, exitP, |
798 kill_thyP, display_draftsP, print_draftsP, prP, disable_prP, |
791 init_toplevelP, welcomeP]; |
799 enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP]; |
792 |
800 |
793 end; |
801 end; |
794 |
802 |
795 |
803 |
796 (*install the Pure outer syntax*) |
804 (*install the Pure outer syntax*) |