[isabelle-dev] Mysterious error message

Lawrence Paulson lp15 at cam.ac.uk
Thu May 13 20:33:52 CEST 2010


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.

Larry

*** SML lexical error: missing quote at end of string at /Users/lp1 ...
*** The error(s) above occurred in ML source
*** At command "ML_command".




More information about the isabelle-dev mailing list