--- a/src/Pure/General/scan.scala Mon Dec 06 15:10:15 2021 +0100
+++ b/src/Pure/General/scan.scala Mon Dec 06 15:34:54 2021 +0100
@@ -24,7 +24,6 @@
abstract class Line_Context
case object Finished extends Line_Context
case class Quoted(quote: String) extends Line_Context
- case object Verbatim extends Line_Context
case class Cartouche(depth: Int) extends Line_Context
case class Comment_Prefix(symbol: Symbol.Symbol) extends Line_Context
case class Cartouche_Comment(depth: Int) extends Line_Context
@@ -136,41 +135,6 @@
quote ~ quoted_body(quote) ^^ { case x ~ y => x + y }
- /* verbatim text */
-
- private def verbatim_body: Parser[String] =
- rep(many1(sym => sym != "*") | """\*(?!\})""".r) ^^ (_.mkString)
-
- def verbatim: Parser[String] =
- {
- "{*" ~ verbatim_body ~ "*}" ^^ { case x ~ y ~ z => x + y + z }
- }.named("verbatim")
-
- def verbatim_content(source: String): String =
- {
- require(parseAll(verbatim, source).successful, "no verbatim text")
- source.substring(2, source.length - 2)
- }
-
- def verbatim_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
- {
- ctxt match {
- case Finished =>
- "{*" ~ verbatim_body ~ opt_term("*}") ^^
- { case x ~ y ~ Some(z) => (x + y + z, Finished)
- case x ~ y ~ None => (x + y, Verbatim) }
- case Verbatim =>
- verbatim_body ~ opt_term("*}") ^^
- { case x ~ Some(y) => (x + y, Finished)
- case x ~ None => (x, Verbatim) }
- case _ => failure("")
- }
- }.named("verbatim_line")
-
- val recover_verbatim: Parser[String] =
- "{*" ~ verbatim_body ^^ { case x ~ y => x + y }
-
-
/* nested text cartouches */
def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]