Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts




El 9/5/20 a las 06:44, Manuel Eberl escribió:
On 09/05/2020 11:29, Makarius wrote:
At some point the standard Isabelle document output for HTML needs to be
improved analogously, but the underlying web technologies are still unclear to me.
Absolutely. I personally find those PDF documents that we produce at the
moment completely useless. They are not very readable and the arbitrary
restriction to A4 PDFs introduces arbitrary and nonpredictable line
breaks that make this even worse.

Ideally, I think, we would have heavily hyperlinked HTML where you can
click on stuff to get to the definition (like in Isabelle/jEdit), hover
to see information like types (like in Isabelle/jEdit), and have maths
rendered more nicely using LaTeX.
Indeed. I link the source code of my projects in a very primitive way (by modifying the produced HTMLs, for example in here <https://cs.famaf.unc.edu.ar/~pedro/forcing/Forcing/html/Forcing_Notions.html>). This also alleviates the "pink screen" phenomenon (that you can't Crtl-click on a definition of sources of the current running logic).

I also have been wondering for a while whether we should have something
like an optional "handwavy output mode", where things are printed in
more casual notation (e.g. integrals are just printed as integrals) with
no regard for ambiguities or lost detail – just to give the user a
better impression of what the "real" content of the statement is. This
might also make big goals more readable.

Another nice feature would be (un)folding sections. If you are writing a sensible proof document (especially math), it would be desirable to be presented with an "eagle's eye" view of proofs, understandable/palatable by specialists, and with the possibility of diving into details by unfolding. Actually, I do not know if Isabelle documenting capabilities allow to select what depth of an argument is to be shown.




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