From b794252aab2673cc60ecbfcc8fe8bf454e5468ea Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 8 Feb 2012 18:00:57 +0000
Subject: Abort attempt to use special exception printing

---
 hol-light/hol-light.el | 2 +-
 hol-light/pg_prompt.ml | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'hol-light')

diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index 4b366f6c..18192ed1 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -114,7 +114,7 @@ You need to restart Emacs if you change this setting."
   "Value for `proof-shell-error-regexp' with standard top level.")
 
 (defconst hol-light-annotated-error-regexp 
-  ;; "<error>.+</error>" ;; FIXME: include new lines, also fix pg_prompt.ml
+  ;; "<error>.+</error>" ;; unfortunately not enough, this is only for failwith
   hol-light-plain-error-regexp
   "Value for `proof-shell-error-regexp' with custom top level.")
 
diff --git a/hol-light/pg_prompt.ml b/hol-light/pg_prompt.ml
index 0ae28992..b14c01ca 100644
--- a/hol-light/pg_prompt.ml
+++ b/hol-light/pg_prompt.ml
@@ -43,6 +43,9 @@ let original_prompt_fn = !Toploop.read_interactive_input in
 (* Adjust error printing to markup error messages			     *)
 (* ------------------------------------------------------------------------- *)
 
+(* Doesn't really work, as many errors are from OCaml top level and
+   not printed in this way.
+
 let print_exn e =
     match e with
       Failure x -> Format.print_string 
@@ -52,3 +55,5 @@ let print_exn e =
     | _  -> Format.print_string (Printexc.to_string e);;
 
 #install_printer print_exn;;
+
+*) 
-- 
cgit v1.2.3