1/*  Title:      Pure/PIDE/command_span.scala
2    Author:     Makarius
3
4Syntactic representation of command spans.
5*/
6
7package isabelle
8
9
10import scala.collection.mutable
11
12
13object 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}
99