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