[isabelle-dev] Errors in right bar shadowed by warnings

Lars Noschinski noschinl at in.tum.de
Thu May 15 15:03:20 CEST 2014


while porting some larger theory (~5800 lines) to the repository version
(23a9cb098ccb), I noticed that sometimes the red error bars in the right
status bar are shadowed by warnings; that is, I see in the theory panel
that there are errors in this theory, but I have to carefully scroll
through the theory file until I find the location.

I haven't cooked up a small example, but this can be seen in
WordLemmaBucket.thy in 6789d4b8379e in


A video (slightly bad quality, the state of options to do simple video
cropping in Linux seems kind of ... bad):


  -- Lars

More information about the isabelle-dev mailing list