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