[isabelle] jEdit: cursor movement and goal display



I was trying the jEdit interface in Isabelle 2012 for the first time
today. To me, the vision and its execution are superb.

But, I had one or two questions over very minor details:

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?

2. I had to manually add shortcuts for "-->" and "/\", but I noticed
   that "and" at least works for the latter. Is this expected
   behaviour? Are these new shortcuts recommended over the old ones?

Tim.

Attachment: signature.asc
Description: Digital signature



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