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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
