Email Gateway (Jan 10 2021 at 18:48): Email Gateway (Jan 10 2021 at 18:48):From: Makarius <makarius@sketis.net>
As usual, the "Documentation" section of the website refers to "Theory
libraries" in HTML, e.g. see
https://isabelle.in.tum.de/website-Isabelle2021-RC2/dist/library/HOL/HOL/index.html
This is now based on formal PIDE markup produced in batch-builds; so there is
much more fancy coloring and a few more hyperlinks. Further presentation of
markup will come eventually, after this release.
Moreover, formally included Isabelle/ML files get proper attention:
Isabelle/HOL consists of theory specifications and ML tool implementations in
a complex bootstrap process that winds itself towards theory "Main" (or
"Complex_Main").
The overall HTML presentation style is still somewhat crude: like
syntax/semantics highlighting in Isabelle/jEdit.
Eventually, I would like to see journal-quality rendering of formal
mathematical text (not "code"). This requires suitable web-technology that
lasts more than just 6 months as a "cool" or "hot" thing.
Makarius
Email Gateway (Jan 10 2021 at 22:13):From: Jakub Kądziołka <kuba@kadziolka.net>
On Sun Jan 10, 2021 at 7:47 PM CET, Makarius wrote:
On 10/01/2021 16:52, Makarius wrote:
The current release candidate website is
https://isabelle.in.tum.de/website-Isabelle2021-RC2As usual, the "Documentation" section of the website refers to "Theory
libraries" in HTML, e.g. see
https://isabelle.in.tum.de/website-Isabelle2021-RC2/dist/library/HOL/HOL/index.htmlThis is now based on formal PIDE markup produced in batch-builds; so
there is
much more fancy coloring and a few more hyperlinks. Further presentation
of
markup will come eventually, after this release.
Ah, what a coincidence! Just three days ago I started developing a tool
to do this based on the output of 'isabelle dump'.
Some remarks:
The generated files seem to lack a closing </html> tag
The semi-transparent background color on .quoted is a bit inconsistent,
as sometimes (indeed, most of the time) Isabelle generates two nested
quoted tags. Thus, when only a single tag is generated (see for example
the line "code_datatype holds" in Tools/Code_Generator), the highlight
is very faint.
In my case, I resolved this by pre-baking the transparency, i.e.
background-color: #f3f3f3;
Moreover, formally included Isabelle/ML files get proper attention:
Isabelle/HOL consists of theory specifications and ML tool
implementations in
a complex bootstrap process that winds itself towards theory "Main" (or
"Complex_Main").
Interesting! Does the PIDE markup for included ML files get included in
the output of 'isabelle dump' somewhere?
The overall HTML presentation style is still somewhat crude: like
syntax/semantics highlighting in Isabelle/jEdit.Eventually, I would like to see journal-quality rendering of formal
mathematical text (not "code"). This requires suitable web-technology
that
lasts more than just 6 months as a "cool" or "hot" thing.Makarius
I suppose I should also say something about my own implementation. The
end goal is to integrate it into a blog authoring tool, so I'm going to
continue my out-of-tree efforts.
As I've mentioned, I get my semantic information from the output of
'isabelle dump'. I have found two small deficiencies in this command:
The root causes of both seem to be very similar - the pure_base and
skip_base arguments to Context in src/Pure/Tools/dump.scala are both
hardcoded as false, with no commandline flag to control them.
I'm currently halfway through duplicating the tooltips mechanism of
Isabelle/jEdit, and go-to-definition is next on the list. When that is
ready, I will make a proper announcement on this mailing list.
One feature I'm particularily fond of is not even present in
Isabelle/jEdit: when you hover over a non-ASCII symbol, a tooltip will
tell you its name, as well as any abbreviations - as far as I am aware,
the only ways to learn the name of a symbol when you first encounter it,
is to either open a .thy file with Notepad to see the escape code, or a
game of where's waldo in the Symbols tab of jEdit.
Though it's nothing particularily flashy yet, you can see a preview here:
https://niedzejkob.github.io/isabelle-markup/HOL/HOL.html
The corresponding code is available here:
https://github.com/NieDzejkob/isabelle-markup
Kind regards,
Jakub Kądziołka
Email Gateway (Jan 11 2021 at 15:18):From: Makarius <makarius@sketis.net>
On 10/01/2021 21:39, Jakub Kądziołka wrote:
The generated files seem to lack a closing </html> tag
Oops, I have now changed that in
https://isabelle.sketis.net/repos/isabelle-release/rev/ff9cd62d2d20
The semi-transparent background color on .quoted is a bit inconsistent,
as sometimes (indeed, most of the time) Isabelle generates two nested
quoted tags. Thus, when only a single tag is generated (see for example
the line "code_datatype holds" in Tools/Code_Generator), the highlight
is very faint.In my case, I resolved this by pre-baking the transparency, i.e.
background-color: #f3f3f3;
That is an interesting fine-point.
In Isabelle/jEdit the underlying PIDE rendering works differently:
snapshot.select in
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021-RC2/src/Pure/PIDE/rendering.scala#l495
traverses the markup tree, such that only one markup element per text interval
take precedence. So there is no stacking-up of markups of the same kind (here
"foreground" color).
I wonder if CSS can imitate the snapshot.select traversal. Otherwise one could
try to generate "flat" HTML markup from rendering.foreground (and other
rendering selectors), instead of taking the full XML document.
Yet another possibility: quite different HTML presentation with less colors
and more typography (high-quality math fonts). It could be a combination of
parsing in the context of PIDE rendering results. (I will pursue this later,
to see how far we can approximate actual math journal quality, e.g. via
MathJax 3).
Moreover, formally included Isabelle/ML files get proper attention:
Isabelle/HOL consists of theory specifications and ML tool
implementations in
a complex bootstrap process that winds itself towards theory "Main" (or
"Complex_Main").Interesting! Does the PIDE markup for included ML files get included in
the output of 'isabelle dump' somewhere?
Probably not. Behind "isabelle dump" is a rather complex "headless PIDE"
session with its own rules what works well and what doesn't.
It is better to switch your application to plain "isabelle build" + retrieval
of the PIDE markup from the build database.
See also the implementation of the new "isabelle document" tool:
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021-RC2/src/Pure/Thy/presentation.scala#l699
--- it first makes a regular Build.build (the Scala function behind "isabelle
build) to ensure that the sources are consistent with the session databases;
then it accesses the build artefacts (exported tex sources) via
db_context.get_export.
For your application, the database access can work via Build_Job.read_theory,
just like Presentation.session_html, which is the implementation behind
"isabelle build -P:".
Makarius
Email Gateway (Jan 11 2021 at 15:26):From: Makarius <makarius@sketis.net>
Side-remark: reading Isabelle/Scala sources works best with IntelliJ IDEA. See
the Isabelle "system" manual about the "isabelle scala_project" tool, with
links and hints about Gradle and IntelliJ.
Maybe "isabelle scala_project" should eventually support user-space projects
as well. Right now you have to tinker manually, and then use suitable
"isabelle_scala_service" invocations in your etc/settings: e.g. see
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021-RC2/etc/settings#l23
Makarius
Email Gateway (Jan 18 2021 at 16:14):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Dear Makarius & all,
While testing an AFP entry, I noticed some odd behavior in the rendering
of sub/superscripts in HTML output. It looks that <sub> and <sup> tags
get mixed with surrounding <span> tags.
The output of RC2 looks like
in contrast to Isabelle2020:
(the underlining is there because I crosslink the html afterwards "by
hand").
By the way, I'm still curious about the decision about (not) having
multicharacter sub/supercript rendering support at jEdit.
Thank you very much in advance.
piampcnohlhgobcd.png
kcoipckjdlapompp.png
Email Gateway (Jan 24 2021 at 19:06):From: Makarius <makarius@sketis.net>
On 18/01/2021 17:14, Pedro Sánchez Terraf wrote:
While testing an AFP entry, I noticed some odd behavior in the rendering of
sub/superscripts in HTML output. It looks that <sub> and <sup> tags get mixed
with surrounding <span> tags.
This should work better in Isabelle2021-RC3. The relevant change is
https://isabelle.sketis.net/repos/isabelle-release/rev/624c2b98860a based on
earlier workarounds for pretty-printed output with markup.
By the way, I'm still curious about the decision about (not) having
multicharacter sub/supercript rendering support at jEdit.
You mean Isabelle/jEdit: plain jEdit cannot even render single-symbol
controls. Likewise other editors, like VSCode: I don't want to depend too much
on the peculiar rendering model of Isabelle/jEdit.
In the HTML breakdown we see that there is a conceptual mismatch: the
block-control symbols pretend to be markup, but should not do this.
I will nonetheless reconsider the whole affair eventually, maybe as
single-control symbol for a cartouche.
Makarius
Email Gateway (Jan 25 2021 at 20:50):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
El 24/1/21 a las 16:06, Makarius escribió:
On 18/01/2021 17:14, Pedro Sánchez Terraf wrote:
While testing an AFP entry, I noticed some odd behavior in the rendering of
sub/superscripts in HTML output. It looks that <sub> and <sup> tags get mixed
with surrounding <span> tags.
This should work better in Isabelle2021-RC3. The relevant change is
https://isabelle.sketis.net/repos/isabelle-release/rev/624c2b98860a based on
earlier workarounds for pretty-printed output with markup.
Thanks for your work.
By the way, I'm still curious about the decision about (not) having
multicharacter sub/supercript rendering support at jEdit.
I will nonetheless reconsider the whole affair eventually, maybe as
single-control symbol for a cartouche.
This is great.
Last updated: Apr 19 2024 at 04:17 UTC