On 04/04/2012 14:33, Makarius wrote:
On Wed, 4 Apr 2012, Rob Arthan wrote:
I've now reduced the error message to a warning since it seems Isabelle has "op" in signatures.
Tut, tut :-). Somewhat to my surprise, the ProofPower source does comply with the standard syntax, even though I was completely unaware that "op" wasn't allowed in signatures.
Historically, we've always tried to minimize the problems in the grey areas of the SML standard, with its occasional changes that were not immediately clear from outside.
I have no problems to remove inappropriate "op" occurrences from the Isabelle sources, if it does not break SML/NJ or old versions of Poly/ML (5.2.1, 5.3.0, 5.4.x). On the other hand it will make testing of old Isabelle versions with brand new Poly/ML versions more difficult.
It's probably worth summarising the current and previous situation.
There's no change to the handling of patterns or expressions. Poly/ML produces warnings if it is able to parse an infix operator without "op". So "(+)" and "map (+)" will continue to be accepted but produce a warning.
"op" is now allowed in exception declarations but not in signatures. So exception op y exception op x = op y are accepted. The "op" is simply ignored; there's no warning if it is missing for infix operators.
In a datatype constructor previously a warning was produced if a value constructor was declared which had infix status but "op" was not used. That warning has been removed so "op" is simply ignored.
In a datatype specification (i.e. in a signature) "op" used to be allowed but ignored. No warning was produced for constructors with infix status. This has changed. Now a warning is produced if "op" is used at all. This is the only place where a warning is produced when it wasn't previously. Since I've now realised that the ML syntax does not allow an "op" here it seems sensible to produce some sort of message. It could cause compatibility problems if other compilers stick to the letter of the ML standard, although it doesn't look like they do. It should be possible get rid of this warning by removing the "op" and still retain compatibility with older versions of Poly/ML since they never complained about a missing "op".
In any case this is just the current SVN and I'm open to suggestions for changes.
Regards, David