Re: [isabelle] Indent command in JEDIT/ISabelle
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and