# HG changeset patch
# User wenzelm
# Date 1515355491 -3600
# Node ID fb539f83683a9f5a23f52129c21fa38d0431f232
# Parent  f74672cf83c6a5eb61c0aeb8c9bf333359fcfd33
support for formal comments in ML in Isabelle/Scala;

diff -r f74672cf83c6 -r fb539f83683a src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sun Jan 07 20:44:48 2018 +0100
+++ b/src/Pure/General/scan.scala	Sun Jan 07 21:04:51 2018 +0100
@@ -27,6 +27,8 @@
   case class Quoted(quote: String) extends Line_Context
   case object Verbatim extends Line_Context
   case class Cartouche(depth: Int) extends Line_Context
+  case object Comment_Prefix extends Line_Context
+  case class Cartouche_Comment(depth: Int) extends Line_Context
   case class Comment(depth: Int) extends Line_Context
 
 
@@ -228,6 +230,34 @@
         Library.try_unsuffix(Symbol.close, source1) getOrElse err()
     }
 
+    def comment_prefix: Parser[String] =
+      (Symbol.comment | Symbol.comment_decoded) ~ many(Symbol.is_blank) ^^
+        { case a ~ b => a + b.mkString }
+
+    def comment_cartouche: Parser[String] =
+      comment_prefix ~ cartouche ^^ { case a ~ b => a + b }
+
+    def comment_cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
+    {
+      def cartouche_context(d: Int): Line_Context =
+        if (d == 0) Finished else Cartouche_Comment(d)
+
+      ctxt match {
+        case Finished =>
+          comment_prefix ~ opt(cartouche_depth(0)) ^^ {
+            case a ~ None => (a, Comment_Prefix)
+            case a ~ Some((c, d)) => (a + c, cartouche_context(d)) }
+        case Comment_Prefix =>
+          many1(Symbol.is_blank) ~ opt(cartouche_depth(0)) ^^ {
+            case b ~ None => (b.mkString, Comment_Prefix)
+            case b ~ Some((c, d)) => (b.mkString + c, cartouche_context(d)) } |
+          cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) }
+        case Cartouche_Comment(depth) =>
+          cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) }
+        case _ => failure("")
+      }
+    }
+
 
     /* nested comments */
 
diff -r f74672cf83c6 -r fb539f83683a src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Sun Jan 07 20:44:48 2018 +0100
+++ b/src/Pure/ML/ml_lex.scala	Sun Jan 07 21:04:51 2018 +0100
@@ -51,6 +51,7 @@
     val STRING = Value("quoted string")
     val SPACE = Value("white space")
     val COMMENT = Value("comment text")
+    val COMMENT_CARTOUCHE = Value("comment cartouche")
     val CONTROL = Value("control symbol antiquotation")
     val ANTIQ = Value("antiquotation")
     val ANTIQ_START = Value("antiquotation: start")
@@ -67,7 +68,7 @@
     def is_keyword: Boolean = kind == Kind.KEYWORD
     def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
     def is_space: Boolean = kind == Kind.SPACE
-    def is_comment: Boolean = kind == Kind.COMMENT
+    def is_comment: Boolean = kind == Kind.COMMENT || kind == Kind.COMMENT_CARTOUCHE
   }
 
 
@@ -144,6 +145,13 @@
     private def ml_comment_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
       comment_line(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT, x), c) }
 
+    private val ml_comment_cartouche: Parser[Token] =
+      comment_cartouche ^^ (x => Token(Kind.COMMENT_CARTOUCHE, x))
+
+    private def ml_comment_cartouche_line(ctxt: Scan.Line_Context)
+        : Parser[(Token, Scan.Line_Context)] =
+      comment_cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT_CARTOUCHE, x), c) }
+
 
     private def other_token: Parser[Token] =
     {
@@ -244,18 +252,21 @@
 
     /* token */
 
-    def token: Parser[Token] = ml_char | (ml_string | (ml_comment | other_token))
+    def token: Parser[Token] =
+      ml_char | (ml_string | (ml_comment | (ml_comment_cartouche | other_token)))
 
     def token_line(SML: Boolean, ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
     {
       val other = (ml_char | other_token) ^^ (x => (x, Scan.Finished))
 
       if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other)
-      else
+      else {
         ml_string_line(ctxt) |
           (ml_comment_line(ctxt) |
-            (ml_cartouche_line(ctxt) |
-              (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))))
+            (ml_comment_cartouche_line(ctxt) |
+              (ml_cartouche_line(ctxt) |
+                (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))))
+      }
     }
   }
 
diff -r f74672cf83c6 -r fb539f83683a src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Jan 07 20:44:48 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Jan 07 21:04:51 2018 +0100
@@ -89,6 +89,7 @@
       ML_Lex.Kind.STRING -> LITERAL1,
       ML_Lex.Kind.SPACE -> NULL,
       ML_Lex.Kind.COMMENT -> COMMENT1,
+      ML_Lex.Kind.COMMENT_CARTOUCHE -> COMMENT1,
       ML_Lex.Kind.ANTIQ -> NULL,
       ML_Lex.Kind.ANTIQ_START -> LITERAL4,
       ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,