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