Just for the record. I think I experienced something similar:


https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-January/005864.html

cheers

chris

On 03/05/2015 11:39 AM, Johannes Hölzl wrote:
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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to