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"
         apply _^H

  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 over.

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.


	Makarius





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