Email Gateway (Aug 18 2022 at 19:45): Email Gateway (Aug 18 2022 at 19:45):From: Holger Blasum <hbl@sysgo.com>
Dear Makarius,
This is the last chance to report any problems before the official
release of Isabelle2012.
if, using RC-3 (linux 32 bit), and jedit I edit a new theory, say "test.thy":
theory test
imports Main
begin
lemma shows "True" proof-
And then intend to outcomment the proof attempt by inserting "(*" before the
lemma, and "*)" after the lemma, that is I want to get
theory test
imports Main
begin
(* lemma shows "True" proof- *)
then after inserting the "(*", I get "Outer syntax error:
command expected, but bad input (* was found". Apparently this is
because jedit still assumes that in this scenario I want to be in
prove mode, while of course by outcommenting it I wanted to abandon
the proof attempt. While this is sth I can live with, is it
desired or necessary behavior or sth that ought to be reported?
Best,
Email Gateway (Aug 18 2022 at 19:46):From: Makarius <makarius@sketis.net>
The behaviour is a consequence how the parser of text changes works, so it
is necessary in that sense. It is also officially specified as a feature
in the REAME:
Incremental reparsing sometimes produces unexpected command spans.
Workaround: Cut/paste larger parts or reload buffer.
This does not mean the specification could not be improved. Compared to
Isabelle2011-1 it is already slightly better in Isabelle2012, and is
anticipated to improve further.
Makarius
Email Gateway (Aug 18 2022 at 19:46):From: Holger Blasum <hbl@sysgo.com>
Incremental reparsing sometimes produces unexpected command spans.
Workaround: Cut/paste larger parts or reload buffer.
Ok, thanks, works. For the record:
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.
Best,
Email Gateway (Aug 18 2022 at 19:48):From: Makarius <makarius@sketis.net>
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).
This is probably an instance of the known incident where the Output panel
is not updated automatically as expected. One needs to press the "Update"
button manually in such situations.
The coupling of the output window with the cursor movement in the source
buffer is sub-optimal in several ways. E.g. it is often unclear to which
part of the source text the output actually refers.
This arrangement stems from very early versions of Isabelle/jEdit from
about 2-3 years ago.
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.
Note that it can only happen when you change the "polarity" of quoted
material, especially (* ... ) and { ... *}. The current line is always
reparsed fully.
Your original motivation was to abandom a proof attempt temporarily.
This can be done formally via the 'oops' command. Comments are relatively
rare in formal text anyway, more like % in latex. (Which does not mean
that formal text {* ... *} is not subject to the same problem.)
Makarius
Email Gateway (Aug 18 2022 at 19:50):From: Lars Noschinski <noschinl@in.tum.de>
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
Email Gateway (Aug 18 2022 at 19:51):From: Tobias Nipkow <nipkow@in.tum.de>
I am afraid I was in this situation earlier on and I just gave up on jedit. The
theory was small, so it was not a question of cut-and-paste vs reload, but my
workflow was seriously disrupted by having to do something special every few
minutes to make jedit happy. It is also confusing to novices because you keep
staring at your text thinking there is something wrong with it although there isn't.
Tobias
Email Gateway (Aug 18 2022 at 19:51):From: Makarius <makarius@sketis.net>
I need to recall some Isabelle/jEdit history here: for 4 years or so I've
been trying desparately make a future beyond Proof General / Emacs happen.
In Isabelle2012 it is now the second stable release of it, after the one
of Isabelle2011-1. The quality of the result critically depends on
feedback by early adopters, not silently giving things up.
So far I've often had the impression that many peoples don't want to go
beyond Proof General at all. This is fine. They only need to organize
themselves to maintain Proof General in the future, because I have stopped
working on it myself in October 2011. (For the Isabelle2012 release I've
invested the canonical 2 weeks of brushing up PG/Emacs into the Windows
installer.)
So for me there is no way looking back. I hope to get more constructive
feedback on Isabelle/jEdit in the future, and find time to work on the
small and big things that still need to be done.
Makarius
Email Gateway (Aug 18 2022 at 19:51):From: Tobias Nipkow <nipkow@in.tum.de>
Am 22/05/2012 10:46, schrieb Makarius:
On Tue, 22 May 2012, Tobias Nipkow wrote:
(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).I am afraid I was in this situation earlier on and I just gave up on jedit.
The quality of the result critically depends on feedback by
early adopters, not silently giving things up.
I don't think my email was silent, or was it? It was the direct reaction to a
jedit session. And to clarify what I said: I gave up on jedit for that session,
not for good. I have no doubt that these problems can be surmounted.
So far I've often had the impression that many peoples don't want to go beyond
Proof General at all.
I do, otherwise I wouldn't be using jedit in teaching and have also started to
use it for my research.
I hope to get more constructive
feedback on Isabelle/jEdit in the future, and find time to work on the small and
big things that still need to be done.
I'm not sure what kind of contructive criticism I am supposed to give if
something does not work. My email was meant emphasize what Lars had already
expressed: namely that what you call "exceptional situations of incremental
parsing" can occur frequently. Lars is happy with the cut-and-repaste
workaround, but I prefer not needing a workaround.
Tobias
Email Gateway (Aug 18 2022 at 19:52):From: Makarius <makarius@sketis.net>
I also prefer not requiring such workarounds, but for me this feature only
occurrs in exceptional situations. This is why it got a lower priority in
the list of things to work on.
Since the balancing problem of quotes/comments is a common problem of
IDEs, maybe someone on the mailing list can point to solutions that other
people have found for it. For example, Netbeans makes it hard to type
unbalanced quotes/comments at all by closing the range immediately, but I
did not like the mechanics of it very much.
Makarius
Email Gateway (Aug 18 2022 at 19:52):From: Tobias Nipkow <nipkow@in.tum.de>
For quotes such an auto-closing feature sounds fairly natural and useful,
although this is just a gut reaction. For comments it won't be so helpful
because one often wants to comment out already existing text (whereas I never
want to quote existing unquoted text).
Tobias
Last updated: Nov 21 2024 at 12:39 UTC