1/*  Title:      Pure/General/comment.scala
2    Author:     Makarius
3
4Formal comments.
5*/
6
7package isabelle
8
9
10object Comment
11{
12  object Kind extends Enumeration
13  {
14    val COMMENT = Value("formal comment")
15    val CANCEL = Value("canceled text")
16    val LATEX = Value("embedded LaTeX")
17    val MARKER = Value("document marker")
18  }
19
20  lazy val symbols: Set[Symbol.Symbol] =
21    Set(Symbol.comment, Symbol.comment_decoded,
22      Symbol.cancel, Symbol.cancel_decoded,
23      Symbol.latex, Symbol.latex_decoded,
24      Symbol.marker, Symbol.marker_decoded)
25
26  lazy val symbols_blanks: Set[Symbol.Symbol] =
27    Set(Symbol.comment, Symbol.comment_decoded)
28
29  def content(source: String): String =
30  {
31    def err(): Nothing = error("Malformed formal comment: " + quote(source))
32
33    Symbol.explode(source) match {
34      case sym :: rest if symbols_blanks(sym) =>
35        val body = if (symbols_blanks(sym)) rest.dropWhile(Symbol.is_blank) else rest
36        try { Scan.Parsers.cartouche_content(body.mkString) }
37        catch { case ERROR(_) => err() }
38      case _ => err()
39    }
40  }
41
42  trait Parsers extends Scan.Parsers
43  {
44   def comment_prefix: Parser[String] =
45     one(symbols_blanks) ~ many(Symbol.is_blank) ^^ { case a ~ b => a + b.mkString } |
46     one(symbols)
47
48   def comment_cartouche: Parser[String] =
49      comment_prefix ~ cartouche ^^ { case a ~ b => a + b }
50
51    def comment_cartouche_line(ctxt: Scan.Line_Context): Parser[(String, Scan.Line_Context)] =
52    {
53      def cartouche_context(d: Int): Scan.Line_Context =
54        if (d == 0) Scan.Finished else Scan.Cartouche_Comment(d)
55
56      ctxt match {
57        case Scan.Finished =>
58          comment_prefix ~ opt(cartouche_depth(0)) ^^ {
59            case a ~ None => (a, Scan.Comment_Prefix(a))
60            case a ~ Some((c, d)) => (a + c, cartouche_context(d)) }
61        case Scan.Comment_Prefix(a) if symbols_blanks(a) =>
62          many1(Symbol.is_blank) ~ opt(cartouche_depth(0)) ^^ {
63            case b ~ None => (b.mkString, Scan.Comment_Prefix(a))
64            case b ~ Some((c, d)) => (b.mkString + c, cartouche_context(d)) } |
65          cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) }
66        case Scan.Comment_Prefix(_) =>
67          cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) }
68        case Scan.Cartouche_Comment(depth) =>
69          cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) }
70        case _ => failure("")
71      }
72    }
73  }
74}
75