[isabelle] Finishing all proofs in use_thy



Hello,

I have the following setting:

   - In an external program I load an Isabelle theory Test (via
   libisabelle). From the Isabelle point of view, this is a call to
   Thy_Info.use_thy.
   - If Test.thy contains errors, Thy_Info.use_thy will usually fail. This
   is desired from my side.
   - However, in some cases (e.g., a "by" that fails, or a use of "sorry"
   without quick_and_dirty mode), errors occur inside futures (I think). Then
   Thy_Info.use_thy will succeed. This is not desired because I want to give
   an error message when loading fails.

How can I, on the Isabelle/ML level, force all futures involved in a theory
to finish in order to throw any potential exceptions? (Something like "val
_ = Thy_Info.use_thy "Draft.Test"; val thy = Thy_Info.get_theory
"Draft.Test"; val _ = join_theory thy (* This one does not exist *)")

I believe this should be possible because the build process does give
errors when a proof fails, after all, instead of simply storing a failing
future in the heap image.

To avoid misunderstandings: I am not working in the bootstrap
ML-environment, but the proper Isabelle/ML environment.

Best wishes,
Dominique.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.