diff options
| author | letouzey | 2012-11-12 13:55:31 +0000 |
|---|---|---|
| committer | letouzey | 2012-11-12 13:55:31 +0000 |
| commit | 8a0d8cfd776650ff08235209792bf32ff55960f4 (patch) | |
| tree | 24ee08512f59943976a7197e895f7f1d69d46b4a /toplevel | |
| parent | d7f0d75164c4d48b5dc3a6773a8c25b58ca8db4d (diff) | |
Xml_parser: detect immediate EOF + disable check_eof by default
Without this immediate EOF detection, coqtop -ideslave loops
when its input channel is closed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15959 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ide_slave.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 93ef6596c1..473b532dc2 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -367,7 +367,6 @@ let loop () = let xml_answer = try let p = Xml_parser.make (Xml_parser.SChannel stdin) in - let () = Xml_parser.check_eof p false in let xml_query = Xml_parser.parse p in let q = Serialize.to_call xml_query in let () = pr_debug ("<-- " ^ Serialize.pr_call q) in @@ -375,6 +374,9 @@ let loop () = let () = pr_debug ("--> " ^ Serialize.pr_full_value q r) in Serialize.of_answer q r with + | Xml_parser.Error (Xml_parser.Empty, _) -> + pr_debug ("End of input, exiting"); + exit 0 | Xml_parser.Error (err, loc) -> let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in fail msg |