Hi, 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 macbroy26:/home/noschinl/repos/vcg-labeling.git A video (slightly bad quality, the state of options to do simple video cropping in Linux seems kind of ... bad): http://www21.in.tum.de/~noschinl/isabelle-shadowed-errors.m4v -- Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
