# HG changeset patch
# User wenzelm
# Date 1516023117 -3600
# Node ID fdb7b995974d9d30568d6256fbf791a4f12e6580
# Parent  a6bf7167c5e19f51ead105d25a7f69e6796eba2f
clarified modules;
more operations;

diff -r a6bf7167c5e1 -r fdb7b995974d src/Pure/General/comment.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/comment.scala	Mon Jan 15 14:31:57 2018 +0100
@@ -0,0 +1,71 @@
+/*  Title:      Pure/General/comment.scala
+    Author:     Makarius
+
+Formal comments.
+*/
+
+package isabelle
+
+
+object Comment
+{
+  object Kind extends Enumeration
+  {
+    val COMMENT = Value("formal comment")
+    val CANCEL = Value("canceled text")
+    val LATEX = Value("embedded LaTeX")
+  }
+
+  lazy val symbols: Set[Symbol.Symbol] =
+    Set(Symbol.comment, Symbol.comment_decoded,
+      Symbol.cancel, Symbol.cancel_decoded,
+      Symbol.latex, Symbol.latex_decoded)
+
+  def symbols_blanks(sym: Symbol.Symbol): Boolean = Symbol.is_comment(sym)
+
+  def content(source: String): String =
+  {
+    def err(): Nothing = error("Malformed formal comment: " + quote(source))
+
+    Symbol.explode(source) match {
+      case sym :: rest if symbols_blanks(sym) =>
+        val body = if (symbols_blanks(sym)) rest.dropWhile(Symbol.is_blank) else rest
+        try { Scan.Parsers.cartouche_content(body.mkString) }
+        catch { case ERROR(_) => err() }
+      case _ => err()
+    }
+  }
+
+  trait Parsers extends Scan.Parsers
+  {
+   def comment_prefix: Parser[String] =
+     one(symbols_blanks) ~ many(Symbol.is_blank) ^^ { case a ~ b => a + b.mkString } |
+     one(symbols)
+
+   def comment_cartouche: Parser[String] =
+      comment_prefix ~ cartouche ^^ { case a ~ b => a + b }
+
+    def comment_cartouche_line(ctxt: Scan.Line_Context): Parser[(String, Scan.Line_Context)] =
+    {
+      def cartouche_context(d: Int): Scan.Line_Context =
+        if (d == 0) Scan.Finished else Scan.Cartouche_Comment(d)
+
+      ctxt match {
+        case Scan.Finished =>
+          comment_prefix ~ opt(cartouche_depth(0)) ^^ {
+            case a ~ None => (a, Scan.Comment_Prefix(a))
+            case a ~ Some((c, d)) => (a + c, cartouche_context(d)) }
+        case Scan.Comment_Prefix(a) if symbols_blanks(a) =>
+          many1(Symbol.is_blank) ~ opt(cartouche_depth(0)) ^^ {
+            case b ~ None => (b.mkString, Scan.Comment_Prefix(a))
+            case b ~ Some((c, d)) => (b.mkString + c, cartouche_context(d)) } |
+          cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) }
+        case Scan.Comment_Prefix(_) =>
+          cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) }
+        case Scan.Cartouche_Comment(depth) =>
+          cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) }
+        case _ => failure("")
+      }
+    }
+  }
+}
diff -r a6bf7167c5e1 -r fdb7b995974d src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Mon Jan 15 10:46:41 2018 +0100
+++ b/src/Pure/General/scan.scala	Mon Jan 15 14:31:57 2018 +0100
@@ -27,7 +27,7 @@
   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 Comment_Prefix(symbol: Symbol.Symbol) extends Line_Context
   case class Cartouche_Comment(depth: Int) extends Line_Context
   case class Comment(depth: Int) extends Line_Context
 
@@ -174,7 +174,7 @@
 
     /* nested text cartouches */
 
-    private def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
+    def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
     {
       require(depth >= 0)
 
@@ -230,34 +230,6 @@
         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 a6bf7167c5e1 -r fdb7b995974d src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Jan 15 10:46:41 2018 +0100
+++ b/src/Pure/General/symbol.scala	Mon Jan 15 14:31:57 2018 +0100
@@ -486,10 +486,8 @@
 
     val newline_decoded = decode(newline)
     val comment_decoded = decode(comment)
-
-
-    /* cartouches */
-
+    val cancel_decoded = decode(cancel)
+    val latex_decoded = decode(latex)
     val open_decoded = decode(open)
     val close_decoded = decode(close)
 
@@ -561,7 +559,7 @@
   def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
 
 
-  /* misc symbols */
+  /* symbolic newline */
 
   val newline: Symbol = "\\<newline>"
   def newline_decoded: Symbol = symbols.newline_decoded
@@ -571,8 +569,20 @@
       (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString
     else str
 
+
+  /* formal comments */
+
   val comment: Symbol = "\\<comment>"
   def comment_decoded: Symbol = symbols.comment_decoded
+  def is_comment(sym: Symbol): Boolean = sym == comment || sym == comment_decoded
+
+  val cancel: Symbol = "\\<^cancel>"
+  def cancel_decoded: Symbol = symbols.cancel_decoded
+  def is_cancel(sym: Symbol): Boolean = sym == cancel || sym == cancel_decoded
+
+  val latex: Symbol = "\\<^latex>"
+  def latex_decoded: Symbol = symbols.latex_decoded
+  def is_latex(sym: Symbol): Boolean = sym == latex || sym == latex_decoded
 
 
   /* cartouches */
diff -r a6bf7167c5e1 -r fdb7b995974d src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Mon Jan 15 10:46:41 2018 +0100
+++ b/src/Pure/ML/ml_lex.scala	Mon Jan 15 14:31:57 2018 +0100
@@ -50,8 +50,8 @@
     val CHAR = Value("character")
     val STRING = Value("quoted string")
     val SPACE = Value("white space")
-    val COMMENT = Value("comment text")
-    val COMMENT_CARTOUCHE = Value("comment cartouche")
+    val INFORMAL_COMMENT = Value("informal comment")
+    val FORMAL_COMMENT = Value("formal comment")
     val CONTROL = Value("control symbol antiquotation")
     val ANTIQ = Value("antiquotation")
     val ANTIQ_START = Value("antiquotation: start")
@@ -68,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 || kind == Kind.COMMENT_CARTOUCHE
+    def is_comment: Boolean = kind == Kind.INFORMAL_COMMENT || kind == Kind.FORMAL_COMMENT
   }
 
 
@@ -78,7 +78,7 @@
   case object ML_String extends Scan.Line_Context
   case class Antiq(ctxt: Scan.Line_Context) extends Scan.Line_Context
 
-  private object Parsers extends Scan.Parsers with Antiquote.Parsers
+  private object Parsers extends Scan.Parsers with Antiquote.Parsers with Comment.Parsers
   {
     /* string material */
 
@@ -140,17 +140,17 @@
     /* ML comment */
 
     private val ml_comment: Parser[Token] =
-      comment ^^ (x => Token(Kind.COMMENT, x))
+      comment ^^ (x => Token(Kind.INFORMAL_COMMENT, x))
 
     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) }
+      comment_line(ctxt) ^^ { case (x, c) => (Token(Kind.INFORMAL_COMMENT, x), c) }
 
-    private val ml_comment_cartouche: Parser[Token] =
-      comment_cartouche ^^ (x => Token(Kind.COMMENT_CARTOUCHE, x))
+    private val ml_formal_comment: Parser[Token] =
+      comment_cartouche ^^ (x => Token(Kind.FORMAL_COMMENT, x))
 
-    private def ml_comment_cartouche_line(ctxt: Scan.Line_Context)
+    private def ml_formal_comment_line(ctxt: Scan.Line_Context)
         : Parser[(Token, Scan.Line_Context)] =
-      comment_cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT_CARTOUCHE, x), c) }
+      comment_cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.FORMAL_COMMENT, x), c) }
 
 
     /* antiquotations (line-oriented) */
@@ -252,7 +252,7 @@
     }
 
     def token: Parser[Token] =
-      ml_char | (ml_string | (ml_comment | (ml_comment_cartouche | other_token)))
+      ml_char | (ml_string | (ml_comment | (ml_formal_comment | other_token)))
 
     def token_line(SML: Boolean, ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
     {
@@ -262,7 +262,7 @@
       else {
         ml_string_line(ctxt) |
           (ml_comment_line(ctxt) |
-            (ml_comment_cartouche_line(ctxt) |
+            (ml_formal_comment_line(ctxt) |
               (ml_cartouche_line(ctxt) |
                 (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))))
       }
diff -r a6bf7167c5e1 -r fdb7b995974d src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Jan 15 10:46:41 2018 +0100
+++ b/src/Pure/build-jars	Mon Jan 15 14:31:57 2018 +0100
@@ -44,6 +44,7 @@
   General/antiquote.scala
   General/bytes.scala
   General/codepoint.scala
+  General/comment.scala
   General/completion.scala
   General/date.scala
   General/exn.scala
diff -r a6bf7167c5e1 -r fdb7b995974d src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Jan 15 10:46:41 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Jan 15 14:31:57 2018 +0100
@@ -88,8 +88,8 @@
       ML_Lex.Kind.CHAR -> LITERAL2,
       ML_Lex.Kind.STRING -> LITERAL1,
       ML_Lex.Kind.SPACE -> NULL,
-      ML_Lex.Kind.COMMENT -> COMMENT1,
-      ML_Lex.Kind.COMMENT_CARTOUCHE -> COMMENT1,
+      ML_Lex.Kind.INFORMAL_COMMENT -> COMMENT1,
+      ML_Lex.Kind.FORMAL_COMMENT -> COMMENT1,
       ML_Lex.Kind.ANTIQ -> NULL,
       ML_Lex.Kind.ANTIQ_START -> LITERAL4,
       ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,