src/Pure/PIDE/command_span.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 68845 3b2daa7bf9f4
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
     1 /*  Title:      Pure/PIDE/command_span.scala
     2     Author:     Makarius
     3 
     4 Syntactic representation of command spans.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.mutable
    11 
    12 
    13 object Command_Span
    14 {
    15   sealed abstract class Kind {
    16     override def toString: String =
    17       this match {
    18         case Command_Span(name, _) => proper_string(name) getOrElse "<command>"
    19         case Ignored_Span => "<ignored>"
    20         case Malformed_Span => "<malformed>"
    21       }
    22   }
    23   case class Command_Span(name: String, pos: Position.T) extends Kind
    24   case object Ignored_Span extends Kind
    25   case object Malformed_Span extends Kind
    26 
    27   sealed case class Span(kind: Kind, content: List[Token])
    28   {
    29     def name: String =
    30       kind match { case Command_Span(name, _) => name case _ => "" }
    31 
    32     def position: Position.T =
    33       kind match { case Command_Span(_, pos) => pos case _ => Position.none }
    34 
    35     def keyword_pos(start: Token.Pos): Token.Pos =
    36       kind match {
    37         case _: Command_Span =>
    38           (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_))
    39         case _ => start
    40       }
    41 
    42     def is_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean =
    43       keywords.kinds.get(name) match {
    44         case Some(k) => pred(k)
    45         case None => other
    46       }
    47 
    48     def is_begin: Boolean = content.exists(_.is_begin)
    49     def is_end: Boolean = content.exists(_.is_end)
    50 
    51     def length: Int = (0 /: content)(_ + _.source.length)
    52 
    53     def compact_source: (String, Span) =
    54     {
    55       val source = Token.implode(content)
    56       val content1 = new mutable.ListBuffer[Token]
    57       var i = 0
    58       for (Token(kind, s) <- content) {
    59         val n = s.length
    60         val s1 = source.substring(i, i + n)
    61         content1 += Token(kind, s1)
    62         i += n
    63       }
    64       (source, Span(kind, content1.toList))
    65     }
    66   }
    67 
    68   val empty: Span = Span(Ignored_Span, Nil)
    69 
    70   def unparsed(source: String): Span =
    71     Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
    72 
    73 
    74   /* XML data representation */
    75 
    76   def encode: XML.Encode.T[Span] = (span: Span) =>
    77   {
    78     import XML.Encode._
    79     val kind: T[Kind] =
    80       variant(List(
    81         { case Command_Span(a, b) => (List(a), properties(b)) },
    82         { case Ignored_Span => (Nil, Nil) },
    83         { case Malformed_Span => (Nil, Nil) }))
    84     pair(kind, list(Token.encode))((span.kind, span.content))
    85   }
    86 
    87   def decode: XML.Decode.T[Span] = (body: XML.Body) =>
    88   {
    89     import XML.Decode._
    90     val kind: T[Kind] =
    91       variant(List(
    92         { case (List(a), b) => Command_Span(a, properties(b)) },
    93         { case (Nil, Nil) => Ignored_Span },
    94         { case (Nil, Nil) => Malformed_Span }))
    95     val (k, toks) = pair(kind, list(Token.decode))(body)
    96     Span(k, toks)
    97   }
    98 }