From a5546dff72259d03360e54e8c7de0f070c554e03 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 6 Jan 2012 16:58:43 +0000
Subject: Make configuration settings. Tweak error regexp.

---
 hol-light/hol-light.el | 26 ++++++++++++++++++++------
 1 file changed, 20 insertions(+), 6 deletions(-)

diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index c2fc60b5..6cb7fddd 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -14,13 +14,27 @@
 (require 'proof-easy-config)            ; easy configure mechanism
 (require 'proof-syntax)			; functions for making regexps
 
+(defcustom hol-light-home "/home/da/hol_light"
+  "*Directory holding the installation of HOL Light."
+  :type 'string
+  :group 'hol-light)
+
+(defcustom hol-light-startup-cmds 
+  (list (concat "#cd \"" hol-light-home "\"") 
+	"#use \"hol.ml\"")
+  "*Commands used to start up a running HOL Light session."
+  :type '(list string)
+  :group 'hol-light)
+
+
+
 (defvar hol-light-keywords nil)
 (defvar hol-light-rules nil)
 (defvar hol-light-tactics nil)
 (defvar hol-light-tacticals nil)
 
 (proof-easy-config  'hol-light "HOL Light"
- proof-prog-name		 "/usr/local/bin/ocaml" ;; std: "ocaml"
+ proof-prog-name		 "ocaml"
  proof-terminal-string           ";;"
  proof-script-comment-start      "(*"
  proof-script-comment-end        "*)"
@@ -49,12 +63,12 @@
 		   "^[ \t]*: GoalstackPure.proofs")
  proof-assistant-home-page           "https://www.cl.cam.ac.uk/~jrh13/hol-light/"
  proof-shell-annotated-prompt-regexp "# "
- proof-shell-error-regexp "Characters [0-9]+-[0-9]+:"
+ proof-shell-error-regexp 
+ (proof-regexp-alt "Characters [0-9]+-[0-9]+:" "Exception: Failure")
  proof-shell-init-cmd
- '("#cd \"/Users/da/hol_light\"" 
-   "#use \"hol.ml\""
-   "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1))"
-   "let pg_top_thm_and_drop () = let t = top_thm() in ((let _ = b() in ()); t)")
+ (append hol-light-startup-cmds
+	 '("let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1))"
+	   "let pg_top_thm_and_drop () = let t = top_thm() in ((let _ = b() in ()); t)"))
 
  ;; FIXME: add optional help topic parameter to help command.
  proof-info-command		    "help \"hol\""
-- 
cgit v1.2.3