1/*  Title:      Pure/General/antiquote.scala
2    Author:     Makarius
3
4Antiquotations within plain text.
5*/
6
7package isabelle
8
9
10object Antiquote
11{
12  sealed abstract class Antiquote { def source: String }
13  case class Text(source: String) extends Antiquote
14  case class Control(source: String) extends Antiquote
15  case class Antiq(source: String) extends Antiquote
16
17
18  /* parsers */
19
20  object Parsers extends Parsers
21
22  trait Parsers extends Scan.Parsers
23  {
24    private val txt: Parser[String] =
25      rep1(many1(s => !Symbol.is_control(s) && !Symbol.is_open(s) && s != "@") |
26        "@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
27
28    val control: Parser[String] =
29      opt(one(Symbol.is_control)) ~ cartouche ^^ { case Some(x) ~ y => x + y case None ~ x => x } |
30      one(Symbol.is_control)
31
32    val antiq_other: Parser[String] =
33      many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s))
34
35    private val antiq_body: Parser[String] =
36      quoted("\"") | (quoted("`") | (cartouche | antiq_other))
37
38    val antiq: Parser[String] =
39      "@{" ~ rep(antiq_body) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z }
40
41    val antiquote: Parser[Antiquote] =
42      txt ^^ (x => Text(x)) | (control ^^ (x => Control(x)) | antiq ^^ (x => Antiq(x)))
43  }
44
45
46  /* read */
47
48  def read(input: CharSequence): List[Antiquote] =
49  {
50    Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input)) match {
51      case Parsers.Success(xs, _) => xs
52      case Parsers.NoSuccess(_, next) =>
53        error("Malformed quotation/antiquotation source" +
54          Position.here(Position.Line(next.pos.line)))
55    }
56  }
57
58  def read_antiq_body(input: CharSequence): Option[String] =
59  {
60    read(input) match {
61      case List(Antiq(source)) => Some(source.substring(2, source.length - 1))
62      case _ => None
63    }
64  }
65}
66