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