diff options
| author | Lasse Blaauwbroek | 2021-04-01 09:18:00 +0200 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2021-04-09 21:05:43 +0200 |
| commit | 520ac61dfe5a6e865cb7b10f4a822c0d72f3ded9 (patch) | |
| tree | 965f41e71b205511685060a215fbaa228390be4c /ide | |
| parent | 1a64b1560ce88855a76e2faa14cec2864de2f37c (diff) | |
Make critical sections safe in the presence of exceptions
We introduce the `with_lock` combinator that locks a mutex in an atomic fashion.
This ensures that exceptions thrown by signals will not leave the system in a
deadlocked state.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide/idetop.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index a6a7f7d742..2fe57ec66c 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -490,11 +490,11 @@ let eval_call c = let print_xml = let m = Mutex.create () in fun oc xml -> - Mutex.lock m; - if !Flags.xml_debug then - Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml); - try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m - with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e + CThread.with_lock m ~scope:(fun () -> + if !Flags.xml_debug then + Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml); + try Control.protect_sigalrm (Xml_printer.print oc) xml + with e -> let e = Exninfo.capture e in Exninfo.iraise e) let slave_feeder fmt xml_oc msg = let xml = Xmlprotocol.(of_feedback fmt msg) in |