From 06b0e65a5b0a3bd900197af234913d58d4b2c3fc Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 8 Feb 2012 16:33:10 +0000 Subject: Add hol-light-prog-name, restart command. --- hol-light/hol-light.el | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) (limited to 'hol-light') diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 48b6d971..3ba67eee 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -27,6 +27,14 @@ :type 'string :group 'hol-light) +(defcustom hol-light-prog-name + (or (getenv "HOLLIGHT_OCMAL") + (getenv "OCAML") + "ocaml") + "*Name of the OCaml interpreter to launch HOL Light." + :type 'string + :group 'hol-light) + (defcustom hol-light-use-custom-toplevel t "*If non-nil, we use a custom toplevel for Proof General. This configures extra annotations inside HOL Light to help @@ -42,7 +50,7 @@ You need to restart Emacs if you change this setting." :group 'hol-light) (defconst hol-light-pre-sync-cmd - (format "#use \"%s/hol-light/pg_prompt.ml\";; " proof-home-directory) + (format "#use \"%shol-light/pg_prompt.ml\";; " proof-home-directory) "Command used to configure prompt annotations for Proof General.") (defcustom hol-light-init-cmd @@ -55,8 +63,9 @@ You need to restart Emacs if you change this setting." (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:=[];;" - "let pg_forget id = ();;"))) + "let pg_kill() = current_goalstack:=[];;" + "let pg_forget id = ();;") + "let pg_restart() = print_string \"*** Session restarted.\";;")) "*Commands used to start up a running HOL Light session." :type '(list string) :group 'hol-light) @@ -118,11 +127,11 @@ You need to restart Emacs if you change this setting." "Value for `proof-shell-proof-completed-regexp' with standard top level.") (defconst hol-light-plain-message-start - "^Warning " + "^Warning \\|\\*\*\\*" "Value for `proof-shell-eager-annotation-start' with standard top level.") (defconst hol-light-annotated-message-start - "^Warning " ;; TODO + "^Warning \\|\\*\\*\\*" ;; TODO "Value for `proof-shell-eager-annotation-start' with custom top level.") (defconst hol-light-plain-message-end @@ -150,7 +159,7 @@ You need to restart Emacs if you change this setting." (proof-easy-config 'hol-light "HOL Light" proof-assistant-home-page "https://www.cl.cam.ac.uk/~jrh13/hol-light/" - proof-prog-name "ocaml" + proof-prog-name hol-light-prog-name proof-terminal-string ";;" proof-shell-pre-sync-init-cmd hol-light-pre-sync-cmd proof-shell-init-cmd hol-light-init-cmd @@ -166,7 +175,8 @@ You need to restart Emacs if you change this setting." proof-kill-goal-command "pg_kill();;" proof-undo-n-times-cmd "pg_undo %s;;" proof-forget-id-command "pg_forget \"%s\";;" - proof-showproof-command "p()" + proof-shell-restart-cmd "pg_restart();;" + proof-showproof-command "p();;" proof-auto-multiple-files t proof-shell-cd-cmd "#cd \"%s\";;" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) -- cgit v1.2.3