Re: [isabelle] New commands in Isabelle2012



On Tue, 19 Jun 2012, Christian Sternagel wrote:

when following section 5.8 of the Progtutorial in jEdit, I noticed that a string that was declared as keyword in the keywords-section of the header is still highlighted as such after removing it from the keywords-section.

To reproduce start with:
--------------------------------
theory Foo imports Main begin
foobar
end
--------------------------------
where "foobar" is not highlighted as keyword. Now add
--------------------------------
keywords "foobar" :: thy_decl
--------------------------------
to the header. At this point "foobar" is highlighted as keyword (and something seems to happen at foobar, since the background is highlighted from there until the end of the file, but there is no output, which is also strange).

The command is declared as a keyword, but not defined yet, so some undefined behaviour is to be expected. What happens here is that the execution of that document version stops at the undefined command, since the attempt to parse it semantically has failed.

I would say that is correct behaviour, although there could be more ambitious error messages.


Now delete "foobar" from the content and remove the keywords-section again. When typing "foobar" again, it is still highlighted as keyword (and the usual "Outer syntax error: command expected, but identifier foobar was found" is missing).

I did not quite manage to reproduce that exactly. Nonetheless, some odd effects are to be expected when declared command keywords are removed later. This is because there are several slightly different ways to manage commands at the same time: the old global table for the TTY loop (and thus for Proof General) and a new value-oriented table within the theory, moreover the the Prover IDE with its own syntax derived from the keywords declarations in the theory headers without inspecting the semantic content yet (intertwined with the editing process).

The whole affair is a bit like providing syntax highlighting for perl6, and it works surprisingly well already. After a few more years, when the TTY loop and PG are really obsolete, the old stateful way can disappear altogether and become fully value-oriented without odd effects. But that is not imminent. I have no reason to kill Proof General prematurely, after so many years of tending it.


	Makarius





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