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