As of c7f6f01ede15 I noticed the following behavior. Suppose I have a
theory file with the following content
theory Foo
imports
Main
begin
end
So far so good. Now I add another import.
theory Foo
imports
Main
"~~/src/HOL/Tools/Adhoc_Overloading"
begin
end
By accident this refers to a non-existent file. Instead of a
corresponding error-message, however, the whole file maintains a lightly
red background and doesn't seem to be processed at all (i.e., I do not
get any output if I edit in between "begin" and "end").
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
