Email Gateway (Aug 18 2022 at 19:01): Email Gateway (Aug 18 2022 at 19:01):From: Jens Doll <jd@cococo.de>
Hello Isabelle,
since I was having some problems with directly using the examples from
the web site (mixture of ASCII and Unicode; the HTML page source is even
worse for reformatting), I'd suggest to offer the proof library in the
same manner as the Cobol Test Suite is presented to the users. It's two
small *.jsp pages and afterwards it looks like this:
http://cococo.de/Context_IT_GmbH/index.jsp?content=directory&lib=products/Sources/COBOL/
Just a question :
Would I be allowed to set up a mirror here for the University of Hamburg?
Jens
Email Gateway (Aug 18 2022 at 19:06):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Sonntag, den 29.01.2012, 11:41 +0100 schrieb Jens Doll:
Hello Isabelle,
since I was having some problems with directly using the examples from
the web site (mixture of ASCII and Unicode; the HTML page source is even
worse for reformatting), I'd suggest to offer the proof library in the
same manner as the Cobol Test Suite is presented to the users. It's two
small *.jsp pages and afterwards it looks like this:
http://cococo.de/Context_IT_GmbH/index.jsp?content=directory&lib=products/Sources/COBOL/
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. If you want to have a raw-file
accessd via HTTP you can also use the mercurial repository like:
http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2011-1/src/HOL/Complete_Lattices.thy
Just a question :
Would I be allowed to set up a mirror here for the University of Hamburg?
Why do you need the mirror?
I prefer to have as few mirrors as possible as they are often outdated,
have a different setup as the original page, and we can not mirror the
wiki pages.
Of course you need a mirror, you can copy the page with tools like wget
or you give us an rsync account and we duplicate our content.
Jens
Email Gateway (Aug 18 2022 at 19:08):From: Makarius <makarius@sketis.net>
I also don't quite understand the problem, nor the purpose of a "mirror".
In general the BSD-style license of Isabelle allows you to work with the
given sources in many ways, and present the results other servers, or keep
them for yourself on a private storage device, or move them to /dev/null.
Other people have done that before, while making clear that it is their
own project that happens to use Isabelle in one way or the other.
Makarius
Email Gateway (Aug 18 2022 at 19:09):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 17 2024 at 20:15 UTC