Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: antiquote.scala Sprache: Scala

Original von: Isabelle^©

/*  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)))
  }

  /* read */

  def read(input: CharSequence): List[Antiquote] =
  {
    Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input)) 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
    }
  }
}

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.