Email Gateway (Apr 14 2026 at 19:31): Email Gateway (Apr 14 2026 at 19:31):From: Bartosz Glowacki <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle developers,
I found an issue in XML.Output.string (src/Pure/PIDE/xml.scala, line ~195) where a null text value is appended literally as the four characters "null" instead of being safely ignored.
The method contains a defensive null check, but the action taken is incorrect: builder ++= str with str == null calls Java's StringBuilder.append(null: String), which appends the ASCII characters n, u, l, l. The else branch that would normally HTML-escape the string is never reached.
Call chain:
XML.string_of_tree → XML.Output.text(s) → XML.Output.string(s)
→ str == null → builder ++= str → "null" appended to output
This means any XML.Text node whose content is null (possible via Java interop or an ML prover malfunction) produces corrupt serialised output. This can corrupt protocol messages between the PIDE session manager and the ML prover or insert the literal word "null" into rendered proof output visible in editors (making developers wondering where did it come from with ctrl+f 'null' and no output).
Minimal fix - in the null branch, do nothing instead of appending (xml.scala, line ~195):
Patch is attached to this email.
The else branch already produces correct output for non-null strings. For null, the correct output is nothing - an empty text node contributes zero characters. Skipping the append entirely restores that contract.
I have a test function that confirms this issue:
def test_xml_null_string_output(): Boolean = {
val result = XML.string_of_tree(XML.Text(null))
result == "null"
}
Logs from manual testing:
// Unpatched behavior ("null" string appended):
bartek1301@BGlowacki:~$ isabelle scala -e 'println("OUTPUT: [" + isabelle.XML.string_of_tree(isabelle.XML.Text(null)) + "]")'
OUTPUT: [null]
// Fixed behavior (Missing value safely ignored):
bartek1301@BGlowacki:~$ isabelle scala -e 'println("OUTPUT: [" + isabelle.XML.string_of_tree(isabelle.XML.Text(null)) + "]")'
OUTPUT: []
I am happy to provide the full test code or any additional information. This was found as part of my dissertation work on frontend testing of the Isabelle platform.
Kindest regards,
Bartosz Glowacki
King's College London
Email Gateway (Apr 17 2026 at 09:31):From: Makarius <makarius@sketis.net>
On 14/04/2026 21:24, Bartosz Glowacki (via cl-isabelle-users Mailing List) wrote:
I found an issue in XML.Output.string (src/Pure/PIDE/xml.scala, line ~195)
where a null text value is appended literally as the four characters "null"
instead of being safely ignored.
I am not sure what you mean by "safely ignored". That is a very bad approach
to work with nulls.
As an exercise: look up the point in time where I introduced the != null
check, and try to understand what I was up to at that historical context. Then
we can continue the discussion.
(Any change of the Isabelle sources need to be explained in terms of the
history that lead to the current status-quo).
Minimal fix
Again the dirty word ...
Makarius
Last updated: May 02 2026 at 13:17 UTC