*To*: Manuel Eberl <eberlm at in.tum.de>, Makarius <makarius at sketis.net>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts*From*: Pedro Sánchez Terraf <sterraf at famaf.unc.edu.ar>*Date*: Sat, 9 May 2020 14:37:24 -0300*In-reply-to*: <2b796d83-e0cf-98f0-5b31-d47db666c653@in.tum.de>*References*: <95fdafb6-0ccc-9b64-e7d0-ad4b17a4fff2@in.tum.de> <2f658c65-9699-d255-27ae-743c2d5828d9@sketis.net> <2b796d83-e0cf-98f0-5b31-d47db666c653@in.tum.de>*Reply-to*: sterraf at famaf.unc.edu.ar*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1

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.

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.

**References**:**Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts***From:*Makarius

**Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Question about "isabelle scala"
- Next by Date: Re: [isabelle] Question about "isabelle scala"
- Previous by Thread: Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts
- Next by Thread: [isabelle] New in the AFP: Matrices for ODEs
- Cl-isabelle-users May 2020 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list