[isabelle-dev] Isabelle gets stuck when imported theory is not found

Johannes Hölzl hoelzl at in.tum.de
Thu Mar 5 11:39:56 CET 2015


In rev 304ee0a475d1 I fixed a problem that only appears when one loads
~~/src/HOL/Probability interactively based on the HOL image. 
In Measure_Space the theory "Multivariate_Analysis" was imported without
the correct path. When started with "-l HOL-Multivariate_Analysis" it
worked.

Unfortunately there is no error message, it just looks like
Isabelle/jEdit gets stuck at this point.

Is there a way to show an error message at the position of the import
header? 

 - Johannes



More information about the isabelle-dev mailing list