--- a/src/Pure/ML/ml_lex.scala Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala Mon Dec 08 22:42:12 2014 +0100
@@ -50,6 +50,7 @@
val CHAR = Value("character")
val STRING = Value("quoted string")
val SPACE = Value("white space")
+ val CARTOUCHE = Value("text cartouche")
val COMMENT = Value("comment text")
val ANTIQ = Value("antiquotation")
val ANTIQ_START = Value("antiquotation: start")
@@ -133,6 +134,15 @@
}
+ /* ML cartouche */
+
+ private val ml_cartouche: Parser[Token] =
+ cartouche ^^ (x => Token(Kind.CARTOUCHE, x))
+
+ private def ml_cartouche_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
+ cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.CARTOUCHE, x), c) }
+
+
/* ML comment */
private val ml_comment: Parser[Token] =
@@ -145,10 +155,11 @@
/* delimited token */
private def delimited_token: Parser[Token] =
- ml_char | (ml_string | ml_comment)
+ ml_char | (ml_string | (ml_cartouche | ml_comment))
private val recover_delimited: Parser[Token] =
- (recover_ml_char | (recover_ml_string | recover_comment)) ^^ (x => Token(Kind.ERROR, x))
+ (recover_ml_char | (recover_ml_string | (recover_cartouche | recover_comment))) ^^
+ (x => Token(Kind.ERROR, x))
private def other_token: Parser[Token] =
@@ -246,8 +257,9 @@
if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other)
else
ml_string_line(ctxt) |
- (ml_comment_line(ctxt) |
- (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
+ (ml_cartouche_line(ctxt) |
+ (ml_comment_line(ctxt) |
+ (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))))
}
}