Re: [isabelle] Library of Proofs



On Wed, 1 Feb 2012, Johannes Hölzl wrote:

Are you referring to the theory documentation like:

 https://isabelle.in.tum.de/dist/library/HOL/Complete_Lattices.html

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 solution.

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.


	Makarius


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