[isabelle-dev] abbreviation (output)
makarius at sketis.net
Thu Jan 23 17:13:42 CET 2014
On Thu, 23 Jan 2014, Tobias Nipkow wrote:
> abbreviation (output)
> leq_le :: "int => int => int => bool" ("_ ≤ _ < _")
> "a ≤ b < c == a ≤ b & b < c"
> This used to work until recently, but now (parent: 55123:a389b50e6a42 tip) I get
> *** Inner syntax error: unexpected end of input
> It looks like the annotation ("_ ≤ _ < _") is ignored. If I remove
> (output) it works again.
See also this changeset:
date: Wed Jan 22 22:32:28 2014 +0100
observe local syntax mode (according to e3a39dae2004, which was lost in
0f3ad56548bc), e.g. relevant for "abbreviation (output)" with
The source also contained a (* FIXME ?!? *) from some years ago that was
deleted here, because the unclear position of
Proof_Context.set_syntax_mode in the source was explained by the accident
The question is what is the scope of the syntax print mode specification,
i.e. "(output)" above. In 9ca72949ebac it is both the notation and the
abbreviation table, i.e. the notation is not available when reading the
I've come across that detail yesterday, when experimenting with Fin /
No_Fin, and running into unexpected non-termination of the parser:
No_Fin ("_") where "No_Fin == Fin"
It is still not fully clear what is right, and as usual the words "bug"
and "fix" make no sense at all.
BTW, in the example above you can just use "leq_le" instead of the
notation to write down that abbreviation.
More information about the isabelle-dev