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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and