Re: [isabelle] jEdit: cursor movement and goal display
On Wed, 23 May 2012, Timothy Bourke wrote:
1. I understand that the output panel synchronizes with the line
selected in the edit panel. But sometimes I seem to lose the goal
display when entering a new line.
For instance, if I type
lemma "A & B"
where ^H is a backspace, the goal is updated to:
Unknown proof method: "_"
Is something on my computer misconfigured? Should the current goal
(i.e., the one associated with the previous line) normally always
be visible when editing a subsequent line?
The auto update follows the command span of the caret, which means the
user needs to know what a command span is (former PG users still do, but
it will soon be forgotten).
There are situations where the Output view does not follow as expected, it
requires a separate "Update" by the button. This is one of the many
boundary cases of the editor event model and the continous updates of the
prover document model disagree about the time/space continuum. There used
to be many NPEs from jEdit in the past, but a few anomalies are still left
Above you probably have yet another boundary case: if the command is the
last one in the buffer, jEdit makes a special case for the text address in
the buffer -- it strips of the last newline. Thus your caret actually
points to nowhere, and the display is conservative in not updating itself.
In reality you usually have at least an 'end' command following.
In the next round if refinements, the relation of the Output panel(s) --
there can be multiple -- to the source needs to be made more explicit, and
the connection to editor events made more robust. Recently on Google maps
I've seen some nice ways to indicate the boundary of an area (municipality
etc.) as the search result. It should also be made easy to type in one
spot while watching output from another spot.
This archive was generated by a fusion of
Pipermail (Mailman edition) and