src/Pure/General/antiquote.scala

clarified signature;

/*  Title:      Pure/General/antiquote.scala
    Author:     Makarius

Antiquotations within plain text.
*/

package isabelle


object Antiquote {
  sealed abstract class Antiquote { def source: String }
  case class Text(source: String) extends Antiquote
  case class Control(source: String) extends Antiquote
  case class Antiq(source: String) extends Antiquote


  /* parsers */

  object Parsers extends Parsers

  trait Parsers extends Scan.Parsers {
    private val txt: Parser[String] =
      rep1(many1(s => !Symbol.is_control(s) && !Symbol.is_open(s) && s != "@") |
        "@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)

    val control: Parser[String] =
      opt(one(Symbol.is_control)) ~ cartouche ^^ { case Some(x) ~ y => x + y case None ~ x => x } |
      one(Symbol.is_control)

    val antiq_other: Parser[String] =
      many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s))

    private val antiq_body: Parser[String] =
      quoted("\"") | (quoted("`") | (cartouche | antiq_other))

    val antiq: Parser[String] =
      "@{" ~ rep(antiq_body) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z }

    val antiquote: Parser[Antiquote] =
      txt ^^ (x => Text(x)) | (control ^^ (x => Control(x)) | antiq ^^ (x => Antiq(x)))

    def antiquote_special(special: Symbol.Symbol => Boolean): Parser[Antiquote] =
      many1(s => !special(s)) ^^ Text.apply |
      one(special) ~ opt(cartouche) ^^
        { case x ~ Some(y) => Control(x + y) case x ~ None => Control(x) }
  }


  /* read */

  def read(input: CharSequence): List[Antiquote] = {
    val result = Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input))
    (result : @unchecked) match {
      case Parsers.Success(xs, _) => xs
      case Parsers.NoSuccess(_, next) =>
        error("Malformed quotation/antiquotation source" +
          Position.here(Position.Line(next.pos.line)))
    }
  }

  def read_antiq_body(input: CharSequence): Option[String] = {
    read(input) match {
      case List(Antiq(source)) => Some(source.substring(2, source.length - 1))
      case _ => None
    }
  }
}