History log of /seL4-l4v-10.1.1/HOL4/tools/quote-filter/selftest.sml
Revision Date Author Comments
# f101fb0e 11-Oct-2010 Michael Norrish <Michael.Norrish@nicta.com.au>

Allow Moscow ML build to happen using (as yet unreleased) v2.10.

Basic strategy is to make adoption of basis 2002 even more
thorough. In particular, the Timer structure is now as per
the 2002 Basis.

It is possible to detect that one is working with Moscow ML 2.10 or
later by checking the Holmakefile variable $(HAVE_BASIS2002), which is
set (to value "1") when in 2.10 or later. It is unset elsewhere. See
an example of its use in help/src-sml/Holmakefile.


# e676b178 25-Jul-2006 Michael Norrish <Michael.Norrish@nicta.com.au>

Yet more changes to the quotation filter. The new way of doing things
is conceptually cleaner I think. The ^ character is an escape character
between ` ` in the same way that \ is an escape character between " "
in SML strings. Thus, one can not write
Define`quotechar = #"`"`
Instead, it is necessary to write
Define`quotechar = #"^`"`
The lexer in the quotation filter is rather simpler as a result of this
change. The new behaviour is also documented in a section of the
DESCRIPTION manual.
(Still to do: set up HOL strings and chars so that they look as much
as possible like SML strings and chars (modulo the use of ^ and `), so
that, for example, ``"\t"`` becomes a one-character string containing
a TAB character rather than a two character string containing backslash
and t. I think this change is wise for the sake of familiarity.)