[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