diff options
Diffstat (limited to 'hol-light')
| -rw-r--r-- | hol-light/pg_prompt.ml | 15 |
1 files changed, 15 insertions, 0 deletions
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 ("<error>" ^ s ^ "</error>") + else plain_failwith s;; +*) + |