diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 08:49:25 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 08:49:25 +0000 |
| commit | dee621d7243248654cef6309eee3998bd7e21a39 (patch) | |
| tree | bb993a0be087c19acb5ab0b0000d096b2de1fde4 /hol-light/hol-light.el | |
| parent | 925ef7ed385cb92c80762c3e59c5b33d1dcde05b (diff) | |
Improve handling of undo, implementing pg_kill and pg_undo.
Diffstat (limited to 'hol-light/hol-light.el')
| -rw-r--r-- | hol-light/hol-light.el | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index f773eb6e..05f1ab98 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -51,14 +51,15 @@ You need to restart Emacs if you change this setting." "#use \"hol.ml\"") (if hol-light-use-custom-toplevel (list (format "#use \"%shol-light/pg_tactics.ml\"" - proof-home-directory))) - (list - "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;")) + proof-home-directory)) + (list + "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;" + "let pg_undo n = (pg_repeat n (fun ()->let _ = b() in ()); p());;" + "let pg_kill () = current_goalstack:=[];;"))) "*Commands used to start up a running HOL Light session." :type '(list string) :group 'hol-light) - ;; ;; Regular expressions for matching output with ;; standard or custom top levels @@ -161,9 +162,9 @@ You need to restart Emacs if you change this setting." proof-non-undoables-regexp "b()" ; and others.. proof-goal-command "g `%s`;;" proof-save-command "val %s = top_thm();;" - proof-kill-goal-command "current_goalstack:=[];;" ; for cleanliness + proof-kill-goal-command "pg_kill();;" + proof-undo-n-times-cmd "pg_undo %s;;" proof-showproof-command "p()" - proof-undo-n-times-cmd "(pg_repeat b %s; p());;" proof-auto-multiple-files t proof-shell-cd-cmd "#cd \"%s\";;" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) |