src/Pure/PIDE/command_span.scala
changeset 65335 7634d33c1a79
parent 63606 fc3a23763617
child 65717 556c34fd0554
equal deleted inserted replaced
65334:264a3904ab5a 65335:7634d33c1a79
    54 
    54 
    55   val empty: Span = Span(Ignored_Span, Nil)
    55   val empty: Span = Span(Ignored_Span, Nil)
    56 
    56 
    57   def unparsed(source: String): Span =
    57   def unparsed(source: String): Span =
    58     Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
    58     Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
       
    59 
       
    60 
       
    61   /* XML data representation */
       
    62 
       
    63   def encode: XML.Encode.T[Span] = (span: Span) =>
       
    64   {
       
    65     import XML.Encode._
       
    66     val kind: T[Kind] =
       
    67       variant(List(
       
    68         { case Command_Span(a, b) => (List(a), properties(b)) },
       
    69         { case Ignored_Span => (Nil, Nil) },
       
    70         { case Malformed_Span => (Nil, Nil) }))
       
    71     pair(kind, list(Token.encode))((span.kind, span.content))
       
    72   }
       
    73 
       
    74   def decode: XML.Decode.T[Span] = (body: XML.Body) =>
       
    75   {
       
    76     import XML.Decode._
       
    77     val kind: T[Kind] =
       
    78       variant(List(
       
    79         { case (List(a), b) => Command_Span(a, properties(b)) },
       
    80         { case (Nil, Nil) => Ignored_Span },
       
    81         { case (Nil, Nil) => Malformed_Span }))
       
    82     val (k, toks) = pair(kind, list(Token.decode))(body)
       
    83     Span(k, toks)
       
    84   }
    59 }
    85 }