Isabelle/Isar 中的编码风格约定

Question

TL;DR：Isar 语言有编码约定吗？是否有必要尊重jEdit的折叠策略？

---

我的团队正在研究数学的形式化，因此我们的主要目的之一是获得可读的证明。考虑到这一点，我们尝试以中间事实（和标签，如果有的话）脱颖而出的方式编写证明：

from fact1 have
  1: "Foo"
  using Thm1 Thm2 by auto
then have
  2: "Bar = FooBar"
  by simp
also from 1 have
  " ... = BarFoo"
  by blast 

除了有时这会产生大量“短线”（顺便说一句，我不知道这是否真的是一个问题）之外，它在某种程度上与 jEdit 折叠策略不兼容；折叠后，之前的代码块将如下所示：

from fact1 have
then have
also from 1 have

完全掩盖了论点。下面的格式也许更好：

from fact1
have 1: "Foo"
  using Thm1 Thm2 by auto
then 
have 2: "Bar = FooBar"
  by simp
also from 1 
have " ... = BarFoo"
  by blast 

并且，折叠之后，

from fact1
have 1: "Foo"
then 
have 2: "Bar = FooBar"
also from 1 
have " ... = BarFoo"

这使得论证的流程变得明确。

无论如何，在我提出 5 个新的格式约定之前，我肯定想知道是否存在一些事实上的标准，或者至少是否有人考虑过这一点。