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
