Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bypass PIDE error Bad name: "__"⌂

Email Gateway (Feb 27 2023 at 09:28):

From: Walther Neuper <walther.neuper@jku.at>
Working on an educational software which exploits Isabelle/Isar's
generic tools we run into the error <Bad name: "__"⌂> and in a more
complex context seemingly the same reason led to the error <Malformed
YXML: unbalanced element "inpu">.

The error <Bad name: "__"⌂> is thrown by the attached "Test_Input.thy,
the latter error can be found at
https://hg.risc.uni-linz.ac.at/wneuper/isa/diff/f7795240462a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy#l1.84
.

The "__" results from the requirement to give students a hint for the
input format; we have

val template_empty = ‹Constants [__=__, __=__]›
val input_complete = ‹Constants [r = 7]›

In the sources we see <Bad name: "__"⌂> being thrown in
Pure/Isar/proof_context.ML and in Pure/name.ML -- both not appealing
locations for a patch.

So our question in order to understand more of PIDE's internals: How can
we bypass errors with "__" in the input for terms?

Thank you for help, Walther

Test_Input.thy

Email Gateway (Feb 27 2023 at 10:26):

From: Peter Lammich <lammich@in.tum.de>
Hi Walter,

I usually do something along the lines:

notation (input) undefined ("'_'_")

This will declare __ as an (input only) alias for undefined.

Email Gateway (Feb 27 2023 at 11:30):

From: Walther Neuper <walther.neuper@jku.at>
On 27.02.23 11:23, Peter Lammich wrote:

Hi Walter,

I usually do something along the lines:

notation (input) undefined ("'_'_")

thanks, so simple is the use of Isabelle/Isar if one knows it.

This will declare __ as an (input only) alias for undefined.

Your hint works perfectly; now we'll turn to the error  Malformed YXML:
unbalanced element "input", which is still present.

--

Peter

Walther

On 27/02/2023 10:06, Walther Neuper wrote:

Working on an educational software which exploits Isabelle/Isar's
generic tools we run into the error <Bad name: "__"⌂> and in a more
complex context seemingly the same reason led to the error <Malformed
YXML: unbalanced element "inpu">.

The error <Bad name: "__"⌂> is thrown by the attached
"Test_Input.thy, the latter error can be found at
https://hg.risc.uni-linz.ac.at/wneuper/isa/diff/f7795240462a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy#l1.84
.

The "__" results from the requirement to give students a hint for the
input format; we have

val template_empty = ‹Constants [__=__, __=__]›
val input_complete = ‹Constants [r = 7]›

In the sources we see <Bad name: "__"⌂> being thrown in
Pure/Isar/proof_context.ML and in Pure/name.ML -- both not appealing
locations for a patch.

So our question in order to understand more of PIDE's internals: How
can we bypass errors with "__" in the input for terms?

Thank you for help, Walther

Last updated: Apr 25 2024 at 01:08 UTC