Email Gateway (Aug 18 2022 at 13:36): Email Gateway (Aug 18 2022 at 13:36):From: David Trachtenherz <trachten@in.tum.de>
Hello,
when generating Isabelle theories from CASE tools (written in Java), is
there a way to invoke a pretty printer, like the one used in Proof
Generator, to make the generated theories look readable (w.r.t.
indentation and line breaks)?
Thank You in advance.
David
Email Gateway (Aug 18 2022 at 13:36):From: Makarius <makarius@sketis.net>
You probably mean the automatic indentation mode built into Proof General,
not the theory source pretty printing for LaTeX output (which does not
change indentation).
The Emacs Lisp code for indentation merely does some educated guessing
based on command keyword categories (see also
ProofGeneral/generic/proof-indent.el and the specific configuration in
ProofGeneral/isar/isar-syntax.el). I do not know of any other
implementation of the same (very simple) ideas for Isabelle theories, but
this can be done (if not in Java, then maybe in Scala, or even just in
Python).
Makarius
Last updated: May 03 2024 at 04:19 UTC