Re: [isabelle] jEdit: cursor movement and goal display



Hi Timothy,

On 05/23/2012 03:23 PM, Timothy Bourke wrote:
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?
This happens from time to time and has nothing to do with your computer. The asynchronous document model is just a delicate matter, I would guess.

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?
What exactly do you mean by "shortcuts". You can get most of the logical symbols by just typing their ASCII approximation. As soon as the approximation fits a symbol a popup will show up where you can choose (maybe between several different symbols). E.g., After typing "-->" I have a popup containing just ⟶, and after typing /\ I get ∧. For some symbols there are also convenient "word"-abbreviations, like "forall" for ∀ etc.

What do you mean by "and" works for the latter. The word "and" should not expand to the symbol "∧".

cheers

chris






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