Re: [isabelle] Proof mode maintained after outcommenting [Re: Isabelle2012-RC3 available for testing]



On 20.05.2012 21:28, Makarius wrote:
On Fri, 18 May 2012, Holger Blasum wrote:

Incremental reparsing sometimes produces unexpected command spans.
Workaround: Cut/paste larger parts or reload buffer.

If the cursor *is not* at the end of the theory text
(1) cutting out the entire freshly out-commented section, in our
case "(* lemma shows "True" proof- *)",
(2) then repasting it
==> Exits proof mode and also clears the output window.

If the cursor *is* at the end of the theory text
Doing (1) and (2) above,
==> Again, exits proof mode.
In this case, in the "Output" window the syntax error
message persists, but I can simply ignore it and just type
on until the system overwrites the output buffer either by a new
error message or by an empty string (e.g. after accepting a
successful declaration).
[...]
Of course, as the README mentions, there is also the option of "File
-> Reload", but it involves saving and for me feels more disruptive to
workflow.

When you say "workflow" it sounds like such exceptional situations of
incremental parsing would occur very often.

At least for my working style (I am often changing things in the middle of a theory file), this situation is far from being exceptional. Take e.g. this multi-line definition:

definition K33 :: "('a, 'a × 'a) pre_graph ⇒ bool" ("K⇣3⇣3") where
  "K33 G ≡ sym_pair_digraph G ∧ card (verts G) = 6 ∧
(∃U ⊆ verts G. ∃V ⊆ verts G. U ∪ V = verts G ∧ card U = 3 ∧ card V = 3 ∧
      (∀u ∈ U. ∀v ∈ V. (u, v) ∈ edges G ∧ (v, u) ∈ edges G) ∧
      (∀u ∈ U. ∀u' ∈ U. (u, u') ∉ edges G) ∧
      (∀v ∈ V. ∀v' ∈ V. (v, v') ∉ edges G))"

Now, if I input 'term "x', give it time to reparse and just then add the closing '"', the definition of K33 is not parsed anymore. And if I am in such a situation, the incremental reparsing goes wrong every few minutes.

(The cut-and-repaste workaround is non-disruptive enough that I am fine with it. If the only workaround I knew would be reloading (and thus reproving and losing Undo and a lot of time), I would probably switch back to Proof General).

Your original motivation was to abandom a proof attempt temporarily.
This can be done formally via the 'oops' command.

Not for nested proofs. Also, I have another common use-case for commenting out lemmas: I want to see what breaks, when a lemma is gone.

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.