diff options
| author | coqbot-app[bot] | 2021-04-12 12:34:16 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-12 12:34:16 +0000 |
| commit | 271445decd0fc1a37da3009f148f2e68c7168fe1 (patch) | |
| tree | 631d9976d17d6573b0f348cfd6fdbd83bb779ddb /ide/coqide | |
| parent | 7ce1c4844b077adb25d14cf1bbd2d22548b1e935 (diff) | |
| parent | 520ac61dfe5a6e865cb7b10f4a822c0d72f3ded9 (diff) | |
Merge PR #14046: make critical sections safe in the presence of exceptions
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: SkySkimmer
Ack-by: gadmm
Diffstat (limited to 'ide/coqide')
| -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 72b54d329f..0a0b932c46 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -489,11 +489,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 |