aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_notation.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-03-03 16:49:30 +0100
committerEmilio Jesus Gallego Arias2019-07-07 00:57:28 +0200
commit07abf9818a6b47bb2c2bd0a8201da9743a0c10b6 (patch)
tree0325550fcf395bad3f4951259202f97db182fbaf /plugins/syntax/string_notation.ml
parentae7fc8bc74289bd8a1eca48c8ca8ecf923888285 (diff)
[error] Remove special error printing pre-processing
We remove the special error printing pre-processing in favor of just calling the standard printers. Error printing has been a bit complex for a while due to an incomplete migration to a new printing scheme based on registering exception printers; this PR should alleviate that by completing the registration approach. After this cleanup, it should not be ever necessary for normal functions to worry a lot about catching errors and re-raising them, unless they have some very special needs. This change also allows to consolidate the `explainErr` and `himsg` modules into one, removing the need to export the error printing functions. Ideally we would make the contents of `himsg` more localized, but this can be done in a gradual way.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions