TL;DR: Are there any coding conventions for the Isar language? Is it necessary to respect jEdit's folding strategy?
My team is working on the formalization of mathematics, so one of our main purposes is to obtain readable proofs. Looking into that, we tried to code proofs in a way that intermediate facts (and labels, if any) stand out:
from fact1 have
1: "Foo"
using Thm1 Thm2 by auto
then have
2: "Bar = FooBar"
by simp
also from 1 have
" ... = BarFoo"
by blast
etc. Apart from the fact that sometimes this produces a proliferation of "short lines" (btw, I don't know if this is really a problem), it is somehow not compatible with jEdit folding strategy; after folding, the previous code block would look like this:
from fact1 have
then have
also from 1 have
completely obscuring the argument. The following format perhaps is better:
from fact1
have 1: "Foo"
using Thm1 Thm2 by auto
then
have 2: "Bar = FooBar"
by simp
also from 1
have " ... = BarFoo"
by blast
And, after folding,
from fact1
have 1: "Foo"
then
have 2: "Bar = FooBar"
also from 1
have " ... = BarFoo"
which makes the flow of the argument explicit.
In any case, before I come up with 5 new formatting conventions, I'd definitely like to know if there is some de facto standard, or at least if someone thought about this.