[isabelle-dev] abbreviation (output)

[Makarius]

On Thu, 23 Jan 2014, Tobias Nipkow wrote:

> abbreviation (output)
>  leq_le :: "int => int => int => bool" ("_ ≤ _ < _")
> where
>  "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:

changeset:   55118:9ca72949ebac
user:        wenzelm
date:        Wed Jan 22 22:32:28 2014 +0100
files:       src/Pure/Isar/specification.ML
description:
observe local syntax mode (according to e3a39dae2004, which was lost in 
0f3ad56548bc), e.g. relevant for "abbreviation (output)" with 
non-terminating syntax;

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 
of 0f3ad56548bc.


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 
specification.

I've come across that detail yesterday, when experimenting with Fin / 
No_Fin, and running into unexpected non-termination of the parser:

   abbreviation (output)
     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.


 	Makarius