Re: [isabelle-dev] Isabelle gets stuck when imported theory is not found
On Thu, 5 Mar 2015, Christian Sternagel wrote: Just for the record. I think I experienced something similar: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-January/005864.html Thanks for the reminder. I will try to pick up this old thread soon for the coming release. The problem is a consequence of various "improvements" done elsewhere. I did not make any attempt to change that yet, since I have already a better idea to handle the files that are referenced in theory sources, both imports and ML_files. Thus we have a chance for a genuine improvement of that aspect in the coming release. As we are moving towards it in Apr/May 2015, it will need extra sharp eyes watching out for such fine points. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle gets stuck when imported theory is not found
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
[isabelle-dev] Isabelle gets stuck when imported theory is not found
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
