Email Gateway (Aug 23 2022 at 08:54): Email Gateway (Aug 23 2022 at 08:54):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Hi,
it is possible to typeset Isar code as it appears in Isabelle/JEdit:
https://isabelle.in.tum.de/dist/library/Doc/Prog_Prove/Isar.html
This is for the web. How can I generate this? Where is the code for it
in the source?
And, is it possible to do the same thing in LaTeX document preparation?
If not, could it be written in a few days?
Email Gateway (Aug 23 2022 at 08:55):From: Lawrence Paulson <lp15@cam.ac.uk>
A quick and easy alternative is simply to take a screenshot. Provided you have a high resolution screen (e.g. Apple retina display), the resolution will be reasonable.
Larry
Email Gateway (Aug 23 2022 at 08:56):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
2020-04-02 16:13 időpontban Lawrence Paulson ezt írta:
1st: a slight variation on that is to use headless rendering via
firefox:
As I would use a lot of this, I prefer an automated method. To have this
really usable, hooking this up into document preparation would be
beneficial.
This needs emitting html for a portion of Isar code (see the code
pointer at 2nd)
2nd: rewrite write_document and its descendants in
src/Pure/Thy/html.scala to emit LaTeX instead of HTML and hook it up
into the document preparation. This would the most thorough method but
also requires the most work. To have this as an alternative to the
standard Isar code typesetting could be a thing, so no duplication of
Isar code would be necessary.
3rd: use Jens Bürger's isabelle-listings environment:
https://gitlab.com/jens.buerger/isabelle-listings/ . This needs some
fiddling as even in a small example it fails a bit, see the attachment.
@Makarius: which one fits your ideas on Isabelle document preparation
best?
The Isabelle community might not demand this feature but if there is an
interest it would be nice to have this included in the distribution. So
please tell us if you would use this feature.
Email Gateway (Aug 23 2022 at 08:56):From: Peter Zeller <p_zeller@cs.uni-kl.de>
One option is to build with -o browser_info, for example:
isabelle build -o browser_info -v -D .
Then the output will contain a line like:
Browser info at
/home/peter/.isabelle/Isabelle2019/browser_info/Unsorted/xyz
The HTML files are in this folder.
Another option is to use the jEdit under the menu entry
"Plugins->Isabelle->Show preview in Browser".
This option actually produces the better output since it uses the
semantic highlighting information from jEdit, but I am not aware of a
way to automate this process on a headless build server.
For LaTeX document preparation it might be an option to adjust the style
definitions such that the PDF output uses the same colors as jEdit.
Regards,
Peter
Email Gateway (Aug 23 2022 at 08:57):From: Frédéric Boulanger <frederic.boulanger@lri.fr>
If it may be useful to other people, here is the Makefile I use to prepare the documentation of my theories:
https://github.com/Frederic-Boulanger-UPS/Clocks/blob/master/Makefile <https://github.com/Frederic-Boulanger-UPS/Clocks/blob/master/Makefile>
"make reboot" prepares the ROOT document (everything in the document, output and docs directories is removed).
You should do this only if you change the list of theories or of LaTeX documents.
"make browser_info" builds the documentation, in HTML and PDF, in a way suitable to use Github Pages from a Github repository (serving pages from master/docs). You may then refer to the documentation of your theories in the README.md file as shown in:
https://github.com/Frederic-Boulanger-UPS/Clocks/blob/master/README.md <https://github.com/Frederic-Boulanger-UPS/Clocks/blob/master/README.md>
"make pdf_document" just builds the PDF.
Frédéric Boulanger
CentraleSupélec - Département Informatique Laboratoire de Recherche en Informatique
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex Bât. 650 - 1 rue Raimond Castaing, 91190 Gif-sur-Yvette
+33 [0]1 69 85 14 84
Last updated: Apr 20 2024 at 04:19 UTC