From 17fa92717a8c9facc3e5c529c25dbce93b22f3c3 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 7 Feb 2012 16:52:52 +0000 Subject: Attempt to rebind failwith, which fails, with...errors --- hol-light/pg_prompt.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'hol-light') diff --git a/hol-light/pg_prompt.ml b/hol-light/pg_prompt.ml index f52dc76e..a6342872 100644 --- a/hol-light/pg_prompt.ml +++ b/hol-light/pg_prompt.ml @@ -39,3 +39,18 @@ let original_prompt_fn = !Toploop.read_interactive_input in original_prompt_fn prompt' buffer len);; +(* ------------------------------------------------------------------------- *) +(* Adjust error printing to markup error message *) +(* ------------------------------------------------------------------------- *) + +(* 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 ("" ^ s ^ "") + else plain_failwith s;; +*) + -- cgit v1.2.3