diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-08 20:44:54 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-08 20:44:54 +0000 |
| commit | 13f7729f5d448bcb8aecf21c8fad7a7506a0cf2a (patch) | |
| tree | cdf1046d547790b05f0721dd54e82078f4ac7373 /library/globnames.ml | |
| parent | 6254115b358899886163da4a4add6d419a55b1e9 (diff) | |
Coqide: handle possible fragmentation in xml answers
Experimentally, this occurs at least in win32 when sending commands
quickly enough: one handle_input callback received only a part of an xml
answer, the rest was available only during the next handle_input.
So we store unterminated xml fragments across handle_input invocations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16050 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/globnames.ml')
0 files changed, 0 insertions, 0 deletions