ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

ill formed XML #237

Open Matafou opened 6 years ago

Matafou commented 6 years ago

Hi, When using pg/xml on a large file I get a "ill formed xml" message, see attached file. Sorry I did not manage to minimize the example yet. I will try. P.

illformedXML.txt

Matafou commented 6 years ago

@psteckler can you just see what part of the xml is wrong please?

psteckler commented 6 years ago

I could not find an error in the text. Emacs nXML mode does not report an error. Also, I used the XML validator at https://www.w3schools.com/xml/xml_validator.asp, and it reports no errors.

It is possible that the error message was caused by some other issue, which I'll have to investigate.

psteckler commented 6 years ago

I ran the Elisp/libxml parser on that string and it successfully created an S-exp. In fact, I called the function I wrote that wraps the parser, which deletes the contents of the buffer if the parse is successful. After parsing, I verified that the buffer size is 0.

That message box is guarded by a check for a nonempty buffer. So I don't understand why that message box appears.

Is the problem reproducible?

psteckler commented 6 years ago

Maybe there's a race condition:

psteckler commented 6 years ago

Working on a fix for that possibility.

psteckler commented 6 years ago

Actually, it's not clear to me why a race might happen, because

In any case, I created #341, which uses temp buffers for XML parsing, instead of a dedicated buffer, if in fact the buffer gets additional data, somehow. If the issue can be reproduced, we can see if this fixes the problem.