[MLton] getting String.fromString to return NONE

[Michael Norrish]

Stephen Weeks writes:
 
> Short answer: don't use String.fromString.  

Thanks for this (I appreciate the extra detail of the long answer).  I
ended up writing my function from scratch.

I wanted to emulate the SML lexing rules for HOL's own type of
strings.  Moscow ML's behaviour of accepting "\n" and "\t" (and others
no doubt) meant that I couldn't use Moscow ML's fromString.  Further,
having fromString return the prefix is not a great deal of use either.
I hadn't appreciated that there was a scan function (the fault lies
with Moscow ML implementing just the old Basis), which would at least
have given me the suffix too.

But I totally agree that your intuition is the right one.  You'd think
that the Basis Library would make writing an SML lexer/parser easy.
It also seems to be a great case study in the ambiguity of prose
specifications.

Michael.