diff options
| author | gareuselesinge | 2013-10-11 09:10:54 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-11 09:10:54 +0000 |
| commit | 8a180135842ff098e5c997d711061cf99864d671 (patch) | |
| tree | 86329f64878ae16600b0a2c567325b2b132ac1fb | |
| parent | 2af8edadfdd87c4cea63ce7d386f0304631977e9 (diff) | |
More comments in ide_slave
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16879 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/ide_slave.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 88674545ff..fc0f4f22aa 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -346,7 +346,11 @@ let eval_call xml_oc log c = in Serialize.abstract_eval_call handler c -(** Message dispatching. *) +(** Message dispatching. + Since coqtop -ideslave -coq-slaves on starts 1 thread per slave, and each + thread forwards feedback messages from the slave to the GUI on the same + xml channel, we need mutual exclusion. The mutex should be per-channel, but + here we only use 1 channel. *) let print_xml = let m = Mutex.create () in fun oc xml -> |