Re: [isabelle] Library of Proofs
On Wed, 1 Feb 2012, Johannes Hölzl wrote:
Are you referring to the theory documentation like:
You can copy the text from these pages and insert it into emacs and
jedit. jEdit has currently the problem to not transform the \<..> syntax
into unicode symbols, but you can work with it and it should be
correctly displayed if you reload the file.
Of course the generated HTML files should correctly display the unicode
symbols instead of the \<...> syntax.
Strictly speaking that behaviour is not a problem but part of the
Generally the prover maintains sources in the \<symbol> format (see also
my MKM 2011 paper for some further explanations on that). The front-ends
then tranform (and keep) things in their own "native" format, i.e. some
subset of unicode that is empirically known to work most of the time,
especially in copy-paste between different front-end programs.
For HTML one has to cope with a range of browsers and details about system
fonts, so it is less ambitious in rendering the infinitely many prover
symbols in unicode. Isabelle/jEdit does more here, according to what is
possible on the JVM, but there are also some dropouts like \<A> in jEdit
due to the imbecile "surrogate characters" of the UTF-16 standard.
For Java 7.x/8.x and JavaFx 2.x/3.x Oracle has a certain strategy to make
high-quality HTML5 rendering available as part of the standard
distribution of the Java Runtime Environment. This technology is based on
Webkit, which is also used by Apple for Safari, for example. Thus there
are reasons to believe that within 2 years we can be more ambitious in
using Unicode in HTML presentation, by using the JVM browser instead of
potentially old MS Explorers or Firefoxes that users might have already.
This will also allow to unify browser and editor views further.
This archive was generated by a fusion of
Pipermail (Mailman edition) and