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
Email Gateway (Jul 20 2026 at 19:24):From: Bartosz Glowacki <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] [ISSUE] XML.Output.string(null) appends literal "null" to output
Dear Isabelle developers,
I am writing to follow up on the discussion in this thread regarding the handling of 'null' string input in PIDE.
I noticed that commit 98810e4d19d9 (https://isabelle.in.tum.de/repos/isabelle/rev/98810e4d19d9), made on April 19 after my original email, introduces an improvement to the design of the codebase by making null handling much more explicit.
From what I understand of the recent changes, rather than hiding nulls, the code now utilizes static type checking with explicit null types in most sources, and explicitly maps nulls to error values elsewhere.
Could you confirm whether this design improvement was made in response to the observations I shared?
I am asking as I am writing a paper describing the project.
Thank you.
Kindest regards,
Bartosz
From: Bartosz Glowacki <bartosz.gowacki@kcl.ac.uk>
Sent: Friday, July 3, 2026 1:03 PM
To: Karine Even-Mendoza <karine.even_mendoza@kcl.ac.uk>; Mohammad Ahmad Abdulaziz Ali Mansour <mohammad.abdulaziz@kcl.ac.uk>
Subject: Fw: [isabelle] [ISSUE] XML.Output.string(null) appends literal "null" to output
From: Makarius <makarius@sketis.net>
Sent: Friday, 17 April 2026 11:31:38
To: Bartosz Glowacki <bartosz.gowacki@kcl.ac.uk>; cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Cc: Mohammad Ahmad Abdulaziz Ali Mansour <mohammad.abdulaziz@kcl.ac.uk>; Karine Even-Mendoza <karine.even_mendoza@kcl.ac.uk>
Subject: Re: [isabelle] [ISSUE] XML.Output.string(null) appends literal "null" to output
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
Email Gateway (Jul 20 2026 at 21:37):From: Makarius <makarius@sketis.net>
Subject: [isabelle] [ISSUE] XML.Output.string(null) appends literal "null" to output
On 20/07/2026 20:15, Bartosz Glowacki (via cl-isabelle-users Mailing List) wrote:
Dear Isabelle developers,
I am writing to follow up on the discussion in this thread regarding the
handling of 'null' string input in PIDE.
I noticed that commit 98810e4d19d9 (https://isabelle.in.tum.de/repos/isabelle/
rev/98810e4d19d9 <https://isabelle.in.tum.de/repos/isabelle/
rev/98810e4d19d9>), made on April 19 after my original email, introduces an
improvement to the design of the codebase by making null handling much more
explicit.
From what I understand of the recent changes, rather than hiding nulls, the
code now utilizes static type checking with explicit null types in most
sources, and explicitly maps nulls to error values elsewhere.
Could you confirm whether this design improvement was made in response to the
observations I shared?
I am asking as I am writing a paper describing the project.
Hi Bartosz,
I can confirm that your post was the reason to revisit the question of nulls
in Scala values (case classes). Note that from the viewpoint of empirical
science it does not yet prove anything about your experimental setup: You
would have to explain, why it is better than randomly pointing at sources.
Actually, random re-reading and re-writing of Isabelle sources happens
routinely. Thus we usually improve the overall situation, but it can also
degrade: Sometimes it is better to leave things as they are.
Nulls in plain data of Scala are very annoying, it is a legacy of the Java
platform. The Scala guys did not do anything special for many years. In 2009,
shortly after getting started with Scala in 2008, I made some experiments in
that respect and was disappointed. These experiments also explain my adhoc
change ada5098506af to let the REPL output some nulls in XML.Tree without
crashing, but not all possible nulls. My recent change 98810e4d19d9 explains
the situation, in the laconic prose of the Isabelle changelog.
In correlation with change 98810e4d19d9, I've spent an unreasonable amount of
time to experiment with recent Scala3 type-system features, to cover null vs.
non-null more explicitly. I am unsure if that is really an improvement at that
unfinished stage on the Scala side. Still, it will be in the coming
Isabelle2026 release, according to this NEWS entry in Isabelle/df310d989be6:
Isabelle/Scala now uses more static type-checking by default, notably
Explicit Nulls (as explained in
https://docs.scala-lang.org/scala3/reference/experimental/explicit-nulls.html).
Notable INCOMPATIBILITY: need to be careful about type T vs. T | Null.
The following operations may help to get rid of the Null part:
proper_value: A | Null => Option[A]
_.nn: A | Null => A
The "nn" (non-null) operation is written postfix, like regular method
application. This partial operation will throw NullPointerException on
null. Excessive use of "nn" may indicate a Java-centric programming
style: it is better to use null-free operations from the libraries of
Scala and Isabelle/Scala. As last resort, it also possible to opt-out
from Explicit Nulls for Scala modules as follows:
import scala.language.unsafeNulls
Note: This extension of Scala3 is not yet a "safe" type-system. Even
with type-checking of Explicit Nulls enabled, the Java/VM can produce
null values by other means, e.g. during object initialization.
In the months after the Isabelle2026 release, we shall see how users of
Isabelle/Scala will cope with this extra complication of the type-system. It
is a typical "academic" improvement: nice to have when it really works, but
problems are to be expected in practice. Here the Scala3 type-system is closer
to the "soft" type-system of TypeScript, rather than the hard and fast
type-system of ML.
Generally note that a null value in Isabelle/Scala is usually a programming
error --- except for Java/Swing programming, where that is to be expected.
Such errors must be reported somehow, and not silently ignored like your
original proposal to address the situation.
We even make that explicit in exception Scala.Null in Isabelle/ML, in the
Scala function invocation protocol: a null from the Isabelle/Scala side
becomes an explicit exception in Isabelle/ML. Thus the programming error is
indeed explicit. (Not that I have ever seen that case in practice, because our
Isabelle/Scala library avoids null most of the time.)
Makarius
Last updated: Jul 22 2026 at 14:00 UTC