Re: [isabelle] Unicode tokens in jedit



On Wed, 25 Jul 2012, Christian Sternagel wrote:

On 07/25/2012 05:37 AM, Lars Noschinski wrote:
On 24.07.2012 17:57, Manuel Eberl wrote:
There is one thing about jedit that really annoys me: when I type in an
abbreviation of a Unicode token (well, not all of them are Unicode
tokens, but you know what I mean), such as -_ or !!, I always have to
wait for the auto completion window and then press return for it to be
converted to the corresponding Unicode token.

You can set completion popup delay to 0ms (and then preferable change
completion keys from "\n\t " to "\t"); this makes input much more
comfortable.


Maybe I did not get the original question right. I thought it was: how to obtain unicode tokens faster / by default?

BTW, "uncode token" is terminology from Proof General 4.x, and in Proof General 3.x it was called "x-symbol".

Isabelle has always called things like \<forall> "Isabelle symbol" (since 1998, even before Proof General). In the current Isabelle/Scala/jEdit technology, a finite selection of the infinitely many Isabelle symbols are mapped to Unicode for "poor man's mathematical rendering" -- including sub/superscripts/bold. This makes the text buffer physically unicode, but the prover sources behind that are independent of it, using plain Isabelle symbols as before.

Such fine points are occasionally relevant even for users, to avoid surprises that things are slightly different than first anticipated.


	Makarius





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