[isabelle-dev] Isabelle/jEdit: imports

Christian Sternagel c.sternagel at gmail.com
Fri Jan 16 14:15:53 CET 2015


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


More information about the isabelle-dev mailing list