[isabelle-dev] Mysterious error message
makarius at sketis.net
Fri May 14 15:17:20 CEST 2010
On Thu, 13 May 2010, Lawrence Paulson wrote:
> Has anybody seen the error message attached below? I get it
> (intermittently) when using proof general to step forward at the very
> top of a file. I get it on two different computers and it doesn't seem
> to be connected with a particular revision of the sources.
> Particularly aggravating is that the first line of the message is
> truncated as shown, so that I cannot even locate the file that contains
> the alleged error.
> *** SML lexical error: missing quote at end of string at /Users/lp1 ...
> *** The error(s) above occurred in ML source
> *** At command "ML_command".
The system outputs detailed position information, but Proof General 3.7.x
does not provide any start positions to work with.
You can bypass Proof General via use_thy, which should give you the
You can also try PG 4.0, which passes source positions, but has many other
More information about the isabelle-dev