Email Gateway (Aug 19 2022 at 15:55): Email Gateway (Aug 19 2022 at 15:55):From: lyj238 <lyj238@gmail.com>
Dear Isabelle users:
Who have used the Ident command in Jedit?
Is it usefult to foramt the proof scripts?
regards!
yongjian Li
2014-09-04
lyj238
Catch3A37(09-04-14-45-15).jpg
Email Gateway (Aug 19 2022 at 16:03):From: Makarius <makarius@sketis.net>
On Thu, 4 Sep 2014, lyj238 wrote:
Dear Isabelle users:
Who have used the Ident command in Jedit?
Even after more than 5 years of Isabelle/jEdit development, there is no
systematic indentation support of Isabelle/Isar proof structure according
to the nesting of sub-proofs etc.
This omission has occasionally shown up on this mailing list. You can
search the archives for "indent" or "indentation" (in that spelling, not
"ident"). Some people have come up with some macros in the past, to help
in this situation of lack of official support from the Prover IDE.
Is it usefult to foramt the proof scripts?
BTW, in Isabelle/Isar the input source is called "proof document", to
emphasize that it is not just a linear "script". Hopefully, the Prover
IDE will make this clear eventually, without requiring recurring
explanations.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC