History log of /seL4-l4v-master/HOL4/help/src-sml/Asynt.sml
Revision Date Author Comments
# dd02811a 07-Jun-2011 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix parser used in help so that sigs can contain structure foo : sig .. end

Also report errors by file. For the moment, no errors are reported in
the system's collected signature files, which is nice.


# 8547d904 07-Jul-2009 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix for the SML signature parser that helps to create the online help.
In particular, it was failing to parse

include foo where type ty1 = ty2

Indeed, the lexer didn't even know that "where" was a keyword.

The fix is hackish. In particular, you start to get shift/reduce
errors if you do this naively, because it is legitimate to write

structure M1 : SIG1 and M2 : SIG2

inside a signature. I have unilaterally turned that into a syntax
error because it can be rewritten to

structure M1 : SIG1
structure M2 : SIG2

Moreover, it is not an idiom used in any of our sources. If and when
we decide this needs fixing, I recommend looking at the parser code
inside the Hamlet interpreter. That is where the two forms of INCLUDE
production in the new version of Parser.grm comes from, along with the
idea of having a non-terminal corresponding to a list of identifiers
that is at least two elements long. These are cute ideas. The other
contortions that Hamlet parser has to go through to get the full
language properly supported are not.


# d76f367d 09-Dec-2008 Scott Owens <Scott.Owens@cl.cam.ac.uk>

Got the help build system working on PolyML.


# e58a33ef 09-Dec-2008 Scott Owens <Scott.Owens@cl.cam.ac.uk>

Start working on porting the doc building system to SML (i.e., not Moscow ML)
to get it working with Poly ML.