diff options
author | 2000-05-29 15:48:03 +0000 | |
---|---|---|
committer | 2000-05-29 15:48:03 +0000 | |
commit | 800ed3b35745f7c003c5d02f570532bd0e2500ff (patch) | |
tree | e823270593ae37cd288d71c0f85b27ea297ebc24 | |
parent | 57f456593a4de60e177e43121b289266f58424a2 (diff) |
Add explicit terminators to commands. Generalized isabelle-set-default-cmd.
-rw-r--r-- | isa/isa.el | 13 |
1 files changed, 7 insertions, 6 deletions
@@ -106,11 +106,11 @@ and script mode." proof-indent-commands-regexp (proof-ids-to-regexp isa-keywords) ;; proof engine commands - proof-showproof-command "pr()" + proof-showproof-command "pr();" proof-goal-command "Goal \"%s\";" proof-save-command "qed \"%s\";" - proof-context-command "ProofGeneral.show_context()" - proof-info-command "ProofGeneral.help()" + proof-context-command "ProofGeneral.show_context();" + proof-info-command "ProofGeneral.help();" proof-kill-goal-command "ProofGeneral.kill_goal();" proof-find-theorems-command "ProofGeneral.thms_containing (space_explode \",\" \"%s\");" proof-shell-start-silent-cmd "proofgeneral_disable_pr();" @@ -148,7 +148,7 @@ and script mode." proof-shell-prompt-pattern "^2?[ML-=#>]>? \372?" ;; for issuing command, not used to track cwd in any way. - proof-shell-cd-cmd "Library.cd \"%s\"" + proof-shell-cd-cmd "Library.cd \"%s\";" ;; Escapes for filenames inside ML strings. ;; We also make a hack for Isabelle, by switching from backslashes @@ -183,10 +183,11 @@ and script mode." ;; FIXME: temporary hack for almost enabling/disabling printing. ;; Also for setting default values. proof-shell-pre-sync-init-cmd "ProofGeneral.init false;" - proof-shell-init-cmd (concat (isabelle-set-default-cmd) + proof-shell-init-cmd (concat + (proof-assistant-settings-cmd) "val pg_saved_gl = ref (!goals_limit); fun proofgeneral_enable_pr () = goals_limit:= !pg_saved_gl; fun proofgeneral_disable_pr() = (pg_saved_gl := (if (!goals_limit)>0 then !goals_limit else !pg_saved_gl); goals_limit := 0);") ; FIXME improved version for Isabelle99-1: - ;proof-shell-init-cmd (isabelle-set-default-cmd) + ;proof-shell-init-cmd (proof-assistant-settings-cmd) proof-shell-restart-cmd "ProofGeneral.isa_restart();" proof-shell-quit-cmd "quit();" |