diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-02-07 17:19:05 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-07 17:19:05 +0000 |
| commit | 22bc319440ee852246a5ff67fbc684e0be9d80ac (patch) | |
| tree | c998006e3479eb21db451d5721ec0772983820da /hol-light | |
| parent | d971c47d69e3ff35b2c03a2bec86f4ab227efc97 (diff) | |
Load pg_tactics, fix proof-undo-n-times-cmd again.
Diffstat (limited to 'hol-light')
| -rw-r--r-- | hol-light/hol-light.el | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 9c9dbc5c..d7ab7385 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -41,14 +41,17 @@ You need to restart Emacs if you change this setting." :type 'boolean :group 'hol-light) - (defconst hol-light-pre-sync-cmd (format "#use \"%s/hol-light/pg_prompt.ml\";; " proof-home-directory) "Command used to configure prompt annotations for Proof General.") (defcustom hol-light-init-cmd - (list (format "#cd \"%s\"" hol-light-home) - "#use \"hol.ml\"") + (append + (list (format "#cd \"%s\"" hol-light-home) + "#use \"hol.ml\"") + (if hol-light-use-custom-toplevel + (list (format "#use \"%shol-light/pg_tactics.ml\"" + proof-home-directory)))) "*Commands used to start up a running HOL Light session." :type '(list string) :group 'hol-light) @@ -158,7 +161,7 @@ You need to restart Emacs if you change this setting." proof-save-command "val %s = top_thm();;" proof-kill-goal-command "current_goalstack:=[];;" ; for cleanliness proof-showproof-command "p()" - proof-undo-n-times-cmd "(funpow %s b; p());;" + proof-undo-n-times-cmd "(funpow %s (fun ()->let _ = b() in ()); p());;" proof-auto-multiple-files t proof-shell-cd-cmd "#cd \"%s\";;" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) |