Email Gateway (Aug 22 2022 at 16:21): Email Gateway (Aug 22 2022 at 16:21):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear list,
In Isabelle2017, the auto-indentation feature feels weird when there is I abort a proof
with oops. In detail, if there are command like section and text directly after an oops,
then Isabelle/jEdit always wants to indent the section or text command as far as the oops.
Here are two examples:
lemma False
oops
section foo
lemma False
proof -
have False
oops
section bar
What I would like is the following:
lemma False
oops
section foo
lemma False
proof -
have False
oops
section bar
Am I doing something wrong here or is this indentation behaviour just something that could
be improved in future releases?
Andreas
Email Gateway (Aug 22 2022 at 16:23):From: Makarius <makarius@sketis.net>
The 'oops' command is always apt to odd special cases. I don't know a
better way for Isabelle2017. It is something to be improved eventually.
BTW, commands like 'text' or 'section' were once more restricted in
there occurrences. Now they can occur anywhere and don't enforce a
particular indentation on there own, in contrast to theory commands like
'definition' or 'theorem'.
Makarius
Email Gateway (Aug 22 2022 at 19:20):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
just to revive this old thread, I came upon this odd indentation after
"oops" again today (using Isabelle2018). In my case I was surprised
about the indentation of "term" after "oops".
lemma "A ⟹ B"
oops
term C
cheers
chris
Last updated: Apr 20 2024 at 04:19 UTC