Re: [isabelle] jEdit: cursor movement and goal display
On 05/23/2012 03:23 PM, Timothy Bourke wrote:
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.
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"
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?
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.
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 do you mean by "and" works for the latter. The word "and" should
not expand to the symbol "∧".
This archive was generated by a fusion of
Pipermail (Mailman edition) and