Re: [isabelle] Supporting native Unicode input in Isabelle/jEdit



2013-03-01 12:30 Makarius:
> On Thu, 28 Feb 2013, Christoph LANGE wrote:
>> I wonder why Isabelle/jEdit does not support native Unicode input, but
>> only uses Unicode for display?
>
> Taking this question in isolation, it actually should work both for
> input and display.

Indeed it does.  I'm no longer sure how I came up with this question a
few months back.  Maybe it didn't work in the 2012 version?  I don't
remember.

> The prover sources are stored in a certain text
> format as Isabelle "symbols", but that is treated as "encoding" by
> jEdit, so you will edit the text in UTF-16 of the JVM.  This is not
> fundamentally different from having external files in UTF-8, UTF-16,
> UTF-32 etc. all recoded to the UTF-16 of Java before editing it.

Given all these different encodings I agree that it does not make sense
to arbitrarily choose one of them as the preferred one for *.thy files,
as this does not ensure that there won't be some text editor messing it
up, e.g. an editor that only supports UTF-8 and that assumes any file to
be in UTF-8.

Cheers,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ SePublica Workshop @ ESWC 2013.  Montpellier, France, 26-30 May.
  Deadline 4 Mar; http://sepublica.mywikipaper.org
→ Intelligent Computer Mathematics, 7–12 Jul, Bath, UK; Deadline 8 Mar
  http://cicm-conference.org/2013/
→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  3–5 April 2013, Exeter, UK.  3 Hands-on Tutorials on Economics
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/





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