Re: [isabelle-dev] NEWS: State panel

2015-12-07 Thread Makarius
On Tue, 10 Nov 2015, Fabian Immler wrote: I noticed some strange behavior: if one triggers state output on the same command but after changing the state, the state output does not change. Consider this example: lemma assumes False shows "False ∧ False" (*using assms*) apply simp If you

Re: [isabelle-dev] NEWS: State panel

2015-12-07 Thread Makarius
On Tue, 10 Nov 2015, Mathias Fleury wrote: As a side question, is there a way to have two different panels docked at bottom open at the same time (i.e. splitting the bottom area into two parts and have two different panels in each)? According to current Isabelle/ba051060d46b, the default

Re: [isabelle-dev] NEWS: State panel

2015-11-10 Thread Mathias Fleury
Hello Makarius, this might be intended, but in Isabelle/a99125aa964f from this morning the errors and warnings still goes to the output panel, which means that both panel have to be opened at the same time. Could you give us some insights about your workflow (for theorem proving) with the

Re: [isabelle-dev] NEWS: State panel

2015-11-10 Thread Gerwin Klein
> On 9 Nov 2015, at 9:41 pm, Makarius wrote: > > * The State panel manages explicit proof state output, with jEdit action > "isabelle.update-state" (shortcut S+ENTER) to trigger update according > to cursor position. > > * The Output panel no longer shows proof state output

Re: [isabelle-dev] NEWS: State panel

2015-11-10 Thread Fabian Immler
Hi Makarius, I noticed some strange behavior: if one triggers state output on the same command but after changing the state, the state output does not change. Consider this example: lemma assumes False shows "False ∧ False" (*using assms*) apply simp If you trigger output on the

Re: [isabelle-dev] NEWS: State panel

2015-11-10 Thread Tobias Nipkow
On 10/11/2015 14:20, Gerwin Klein wrote: On 9 Nov 2015, at 9:41 pm, Makarius wrote: * The State panel manages explicit proof state output, with jEdit action "isabelle.update-state" (shortcut S+ENTER) to trigger update according to cursor position. * The Output panel no

[isabelle-dev] NEWS: State panel

2015-11-09 Thread Makarius
* The State panel manages explicit proof state output, with jEdit action "isabelle.update-state" (shortcut S+ENTER) to trigger update according to cursor position. * The Output panel no longer shows proof state output by default. This reduces resource requirements of prover time and GUI space.