--- a/src/Tools/jEdit/src/token_markup.scala Tue Mar 25 15:15:33 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Mar 25 16:11:00 2014 +0100
@@ -204,7 +204,7 @@
{
val (styled_tokens, context1) =
if (mode == "isabelle-ml" || mode == "sml") {
- val (tokens, ctxt1) = ML_Lex.tokenize_line(line, line_ctxt.get)
+ val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, line_ctxt.get)
val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
(styled_tokens, new Line_Context(Some(ctxt1)))
}