aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light/pg_prompt.ml
diff options
context:
space:
mode:
Diffstat (limited to 'hol-light/pg_prompt.ml')
-rw-r--r--hol-light/pg_prompt.ml5
1 files changed, 5 insertions, 0 deletions
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;;
+
+*)