[isabelle-dev] Commands not in scope fail to cause errors

[Andreas Lochbihler]

Dear all,

Today, I spent quite a while to figure out why in Isabelle/e936c2828bec one of my theories 
did not process completely in Isabelle/jEdit. Starting with a simps_of_case command, the 
rest of the theory stayed in the orange-ish color which indicates that this part had not 
yet been processed. poly kept running with full speed on all cores, but no progress was 
visible - not even one of the purple regions was visible.

Ultimately, I found out that I had forgot to import the theory Simps_Case_Conv which 
defines the simps_of_case command (my base image already contains this theory, so the 
mark-up in jEdit was as usual and the theory goes through with Isabelle2014, as 
Isabelle2014 did not support local command scopes).

Unfortunately, there was no error message at all or any other indication that an import is 
missing. I found this very confusing and suggest that this should be changed before the 
next release.

I have attached an example theory which is supposed to be loaded with image HOL-Library. 
Without the import of Simps_Case_Conv, you should be able to observe the described behaviour.

Best,
Andreas
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Scratch.thy
Type: application/x-extension-thy
Size: 234 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150410/d8d5641d/attachment.bin>