--- /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("")
+ }
+ }
+ }
+}
--- 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 */
--- 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 */
--- 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))))))
}
--- 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
--- 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,