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 MHonArc.