Re: [isabelle-dev] Wrong position information in 3bfa28b3a5b2

[Makarius]

On 22/02/2019 22:59, Makarius wrote:
> On 22/02/2019 16:47, Manuel Eberl wrote:
>> I came upon a regrssion with the position information in terms that
>> contain calligraphic or Fraktur letters, e.g.:
>>
>> theory Scratch
>>   imports Pure
>> begin
>>
>> lemma "𝒜 𝒜 𝒜 𝒜 ()) a b c d e"
>>
>> The syntax error in this line is at the second closing parenthesis. In
>> 3bfa28b3a5b2, Isabelle/jEdit displays the error at the space between "a"
>> and "b".
> 
> This is a problem introduced by Java 11: it works fine with Java 8. (I
> will investigate it further later.)

See now the following changes:

changeset:   69840:a35033167f01
tag: tip
user:wenzelm
date:Sun Feb 24 13:00:43 2019 +0100
files:   Admin/components/components.sha1 Admin/components/main
description:
updated to jedit_build-20190224 (new patches: favorites, glyphvector);

changeset:   69839:828f3cd0dcf9
user:wenzelm
date:Sun Feb 24 12:53:23 2019 +0100
files:   src/Tools/jEdit/patches/glyphvector
description:
fallback on createGlyphVector for multi-character glyphs (e.g.
0x01d49c), as seen in Java 11;


Java 11 correctly produces a complex glyph vector layout according to
https://docs.oracle.com/en/java/javase/11/docs/api/java.desktop/java/awt/Font.html#layoutGlyphVector(java.awt.font.FontRenderContext,char[],int,int,int)
but jEdit cannot handle that. So I made a fallback to something that is
closer to the old behaviour in Java 8.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Wrong position information in 3bfa28b3a5b2

[Makarius]

On 22/02/2019 16:47, Manuel Eberl wrote:
> I came upon a regrssion with the position information in terms that
> contain calligraphic or Fraktur letters, e.g.:
> 
> theory Scratch
>   imports Pure
> begin
> 
> lemma "𝒜 𝒜 𝒜 𝒜 ()) a b c d e"
> 
> The syntax error in this line is at the second closing parenthesis. In
> 3bfa28b3a5b2, Isabelle/jEdit displays the error at the space between "a"
> and "b".

Thanks for keeping an eye on isabelle-dev versions.

This is a problem introduced by Java 11: it works fine with Java 8. (I
will investigate it further later.)


> Each "𝒜" seems to shift the offset
> further, so I guess there's an off-by-one error in there somewhere.
> Interestingly, not all letters cause this – e.g. "ℳ" seems to be fine.

The calligraphic "A" belongs to a different Unicode standard than the
calligraphc "M". E.g. see these results in Console / BeanShell or
Console / Scala:

> "𝒜".length()
2
> "ℳ".length()
1


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev