diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-02-07 16:52:52 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-07 16:52:52 +0000 |
| commit | 17fa92717a8c9facc3e5c529c25dbce93b22f3c3 (patch) | |
| tree | c24969a5f52cd99f2c853170a461fddb57ae4c39 /hol-light | |
| parent | de3deb9ecbee3b1dbb08ac77cf2572aac1cddcc6 (diff) | |
Attempt to rebind failwith, which fails, with...errors
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;; +*) + |