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