[isabelle-dev] Where are the error messages?

2013-04-03 Thread Dmitriy Traytel 

Hi,

theory Scratch
imports Main
begin

term True x
thm TrueI[OF TrueI]

end

behaves very strangely in jedit with Isabelle/5dbe537087aa. For both 
commands there is no indication of errors (except of the absence of a 
popup). This seams to apply to all Isar commands involving 
Toplevel.no_timing.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Where are the error messages?

2013-04-03 Thread Makarius 

On Wed, 3 Apr 2013, Dmitriy Traytel wrote:


theory Scratch
imports Main
begin

term True x
thm TrueI[OF TrueI]

end

behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands 
there is no indication of errors (except of the absence of a popup). This 
seams to apply to all Isar commands involving Toplevel.no_timing.


This is bad.  I will take a look as soon as possible.

If you need a quick workaround, you can set parallel proofs to 0 in 
Isabelle/jEdit.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Where are the error messages?

2013-04-03 Thread Makarius 

On Wed, 3 Apr 2013, Dmitriy Traytel wrote:


theory Scratch
imports Main
begin

term True x
thm TrueI[OF TrueI]

end

behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands 
there is no indication of errors (except of the absence of a popup). This 
seams to apply to all Isar commands involving Toplevel.no_timing.


I had messed that up yesterday in 8e9746e584c9.  It was an adverse effect 
on diag commands, and Toplevel.no_timing is just just another 
coincidence.  (Early adopters might have noticed already that commands 
like 'thm', 'ML_val', 'quickcheck', 'sledgehammer' are now forked by 
default.)


I've made various refinements leading up to ee3398dfee9a, so this detail 
should work again.  There are further things involved, and it all needs a 
bit more convergence to just 1 way of doing certain things, not 2 or 3 
slightly different ways.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev