From af00bfad9b14dd182259d376f11ad7af046d4444 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 8 Feb 2012 17:54:21 +0000
Subject: Add print_exn for marked up error messages.

---
 hol-light/pg_prompt.ml | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/hol-light/pg_prompt.ml b/hol-light/pg_prompt.ml
index a6342872..0ae28992 100644
--- a/hol-light/pg_prompt.ml
+++ b/hol-light/pg_prompt.ml
@@ -24,7 +24,7 @@ let pg_prompt_info = ref (fun () -> "");;
 
 
 (* ------------------------------------------------------------------------- *)
-(* Adjust the OCaml prompt to carry information for Proof General.           *)
+(* Adjust the OCaml prompt to carry information for Proof General            *)
 (* ------------------------------------------------------------------------- *)
 
 let original_prompt_fn = !Toploop.read_interactive_input in
@@ -40,17 +40,15 @@ let original_prompt_fn = !Toploop.read_interactive_input in
 
 
 (* ------------------------------------------------------------------------- *)
-(* Adjust error printing to markup error message			     *)
+(* Adjust error printing to markup error messages			     *)
 (* ------------------------------------------------------------------------- *)
 
-(* FIXME: rebinding failwith has an odd effect on top level, triggering
-   new errors which were perhaps previously caught?*)
-
-(*
-let plain_failwith = failwith
-
-let failwith s = if (!pg_mode)
-		  then plain_failwith ("<error>" ^ s ^ "</error>")
-		 else plain_failwith s;;
-*)
+let print_exn e =
+    match e with
+      Failure x -> Format.print_string 
+		     (if (!pg_mode) then 
+		         "<error>" ^ x ^ "</error>"
+		      else x)
+    | _  -> Format.print_string (Printexc.to_string e);;
 
+#install_printer print_exn;;
-- 
cgit v1.2.3