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.
Description: Digital signature