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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
