src/Pure/PIDE/command_span.scala
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 63606 fc3a23763617
child 65335 7634d33c1a79
permissions -rw-r--r--
clarified modules;
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@57910
    18
        case Command_Span(name, _) => if (name != "") name else "<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@63606
    35
    def is_begin: Boolean = content.exists(_.is_begin)
wenzelm@63606
    36
    def is_end: Boolean = content.exists(_.is_end)
wenzelm@63606
    37
wenzelm@59735
    38
    def length: Int = (0 /: content)(_ + _.source.length)
wenzelm@59707
    39
wenzelm@57905
    40
    def compact_source: (String, Span) =
wenzelm@57905
    41
    {
wenzelm@59735
    42
      val source = Token.implode(content)
wenzelm@57905
    43
      val content1 = new mutable.ListBuffer[Token]
wenzelm@57905
    44
      var i = 0
wenzelm@57905
    45
      for (Token(kind, s) <- content) {
wenzelm@57905
    46
        val n = s.length
wenzelm@59735
    47
        val s1 = source.substring(i, i + n)
wenzelm@57905
    48
        content1 += Token(kind, s1)
wenzelm@57905
    49
        i += n
wenzelm@57905
    50
      }
wenzelm@59735
    51
      (source, Span(kind, content1.toList))
wenzelm@57905
    52
    }
wenzelm@57905
    53
  }
wenzelm@57905
    54
wenzelm@57905
    55
  val empty: Span = Span(Ignored_Span, Nil)
wenzelm@57905
    56
wenzelm@57905
    57
  def unparsed(source: String): Span =
wenzelm@57905
    58
    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
wenzelm@57905
    59
}