[isabelle-dev] Mysterious error message

[Makarius]

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 
positions explicitly.

You can also try PG 4.0, which passes source positions, but has many other 
problems.


 	Makarius