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
