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

[Makarius]

On Fri, 10 Apr 2015, Andreas Lochbihler wrote:

> 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.

That was a bad situation of parsing non-existing commands, leading to 
non-termination (no progress of the parser):  I have addressed that in 
Isabelle/76a8400a58d9.  Later, I have made yet another round over the 
error handling in Isabelle/35f626b11422. Both changes together should 
cover all odd cases described on this thread so far, also by Jasmin and 
Tobias.


Conceptually, the situation is as follows:

   (1) Theory headers declare command keywords: this is important for
     proper division of sources into command spans.  Isabelle/jEdit has a
     buffer-local syntax (which is also used for highlighting).

   (2) Outer_Syntax.command (and derivatives) define command parsers in ML:
     this is relevant to provide a semantic transaction to some keyword.

After the change 35f626b11422 above, any missing command parsers should be 
reported clearly.  Notably also commands before 'theory' and after the 
final 'end'.


A remaining potential for user confusion is a situation where keyword 
declarations are totally missing.  In principle, the theory imports need 
to be right in order to get access to outer syntax, but there is an 
old-style exception to it: the base syntax of the session is the union of 
all preloaded theories.  In ancient times, we've had the global union of 
all keywords from all theories, but this could cause other problems.

This means, with -l HOL-Library the keyword 'simps_of_case' is already a 
known keyword, but the command can only be used with the proper import. 
With -l HOL it is not a known keyword, unless theory Simps_Case_Conv is 
actually imported.  This explains the following observation:

> 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).

The -l HOL-Library case might seem luck, but the theory-local keywords 
reform was actually meant to make outer syntax as local as anything else, 
i.e. keyword-vs-ident like const-vs-free in the term language.  It won't 
change for this release, though.

Hopefully the main corner cases are already covered with the above 
robustification.


 	Makarius