author | wenzelm |
Wed, 20 Mar 2019 23:06:51 +0100 | |
changeset 69933 | c15ee153dec1 |
parent 69891 | def3ec9cdb7e |
child 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 |
||
10 |
object 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") |
|
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67449
diff
changeset
|
17 |
val MARKER = Value("document marker") |
67438 | 18 |
} |
19 |
||
20 |
lazy val symbols: Set[Symbol.Symbol] = |
|
21 |
Set(Symbol.comment, Symbol.comment_decoded, |
|
22 |
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
|
23 |
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
|
24 |
Symbol.marker, Symbol.marker_decoded) |
67438 | 25 |
|
67449 | 26 |
lazy val symbols_blanks: Set[Symbol.Symbol] = |
27 |
Set(Symbol.comment, Symbol.comment_decoded) |
|
67438 | 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 |
} |