Re: [isabelle] Isabelle2014-RC0: symbol completion in antiquotations

On Thu, 10 Jul 2014, Christian Sternagel wrote:

On 07/09/2014 05:27 PM, Makarius wrote:
 Note that the problem would be absent, if the traditional quotes were
 replaced by the more robust cartouches.  But this is a bit speculative
 at the moment.
Does that mean that cartouches for antiquotations will not be part of Isabelle2014? Just for the record: I would like to have

 @{term ‹α something›}

since, as you said, this would avoid some problems with symbol completion.

There are many fine points like that, which I would have liked to see in forthcoming Isabelle2014, but did not make it due to still existing baggage of Proof General legacy.

Maybe after next week at Vienna we have a better impression how many remaining uses of Proof General are left over (as well as remaining users).

Everyone is invited to discuss that not just with me, but with any of the Isabelle/jEdit veterans. Early adopters have jumped on the train in October 2011 with the first stable release of the Prover IDE, and the coming one is already version 5 in the internal counting.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.