[isabelle-dev] Where are the error messages?

Makarius makarius at sketis.net
Wed Apr 3 23:00:04 CEST 2013

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 

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.


More information about the isabelle-dev mailing list