diff options
| author | Pierre-Marie Pédrot | 2014-12-03 20:34:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-12-16 13:15:12 +0100 |
| commit | bff51607cfdda137d7bc55d802895d7f794d5768 (patch) | |
| tree | 1a159136a88ddc6561b814fb4ecbacdf9de0dd70 /ide | |
| parent | 37ed28dfe253615729763b5d81a533094fb5425e (diff) | |
Getting rid of Exninfo hacks.
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 10 | ||||
| -rw-r--r-- | ide/interface.mli | 2 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 1 |
3 files changed, 7 insertions, 6 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index b4757c8f76..3d2676f14e 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -322,7 +322,7 @@ let about () = { Interface.compile_date = Coq_config.compile_date; } -let handle_exn e = +let handle_exn (e, info) = let dummy = Stateid.dummy in let loc_of e = match Loc.get_loc e with | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) @@ -332,9 +332,9 @@ let handle_exn e = | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" | e -> - match Stateid.get e with - | Some (valid, _) -> valid, loc_of e, mk_msg e - | None -> dummy, loc_of e, mk_msg e + match Stateid.get info with + | Some (valid, _) -> valid, loc_of info, mk_msg e + | None -> dummy, loc_of info, mk_msg e let init = let initialized = ref false in @@ -421,7 +421,7 @@ let print_xml = fun oc xml -> Mutex.lock m; try Xml_printer.print oc xml; Mutex.unlock m - with e -> let e = Errors.push e in Mutex.unlock m; raise e + with e -> let e = Errors.push e in Mutex.unlock m; iraise e let slave_logger xml_oc level message = diff --git a/ide/interface.mli b/ide/interface.mli index 77a875b7d2..cbaa027508 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -200,7 +200,7 @@ type init_rty = state_id type about_sty = unit type about_rty = coq_info -type handle_exn_sty = exn +type handle_exn_sty = Exninfo.iexn type handle_exn_rty = state_id * location * string (* Retrocompatibility stuff *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index da0bcaf0b9..0cd7e7b818 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -578,6 +578,7 @@ let abstract_eval_call handler (c : 'a call) : 'a value = | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) with any -> + let any = Errors.push any in Fail (handler.handle_exn any) (** brain dead code, edit if protocol messages are added/removed *) |