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_begin: Boolean = content.exists(_.is_begin)
43    def is_end: Boolean = content.exists(_.is_end)
44
45    def length: Int = (0 /: content)(_ + _.source.length)
46
47    def compact_source: (String, Span) =
48    {
49      val source = Token.implode(content)
50      val content1 = new mutable.ListBuffer[Token]
51      var i = 0
52      for (Token(kind, s) <- content) {
53        val n = s.length
54        val s1 = source.substring(i, i + n)
55        content1 += Token(kind, s1)
56        i += n
57      }
58      (source, Span(kind, content1.toList))
59    }
60  }
61
62  val empty: Span = Span(Ignored_Span, Nil)
63
64  def unparsed(source: String): Span =
65    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
66
67
68  /* XML data representation */
69
70  def encode: XML.Encode.T[Span] = (span: Span) =>
71  {
72    import XML.Encode._
73    val kind: T[Kind] =
74      variant(List(
75        { case Command_Span(a, b) => (List(a), properties(b)) },
76        { case Ignored_Span => (Nil, Nil) },
77        { case Malformed_Span => (Nil, Nil) }))
78    pair(kind, list(Token.encode))((span.kind, span.content))
79  }
80
81  def decode: XML.Decode.T[Span] = (body: XML.Body) =>
82  {
83    import XML.Decode._
84    val kind: T[Kind] =
85      variant(List(
86        { case (List(a), b) => Command_Span(a, properties(b)) },
87        { case (Nil, Nil) => Ignored_Span },
88        { case (Nil, Nil) => Malformed_Span }))
89    val (k, toks) = pair(kind, list(Token.decode))(body)
90    Span(k, toks)
91  }
92}
93