src/Pure/PIDE/command_span.scala
author wenzelm
Mon, 20 Mar 2017 20:43:26 +0100
changeset 65335 7634d33c1a79
parent 63606 fc3a23763617
child 65717 556c34fd0554
permissions -rw-r--r--
support to encode/decode command state; support to merge full contents of command state;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/PIDE/command_span.scala
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     3
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     4
Syntactic representation of command spans.
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     5
*/
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     6
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     7
package isabelle
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     8
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
     9
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    10
import scala.collection.mutable
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    11
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    12
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    13
object Command_Span
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    14
{
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    15
  sealed abstract class Kind {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    16
    override def toString: String =
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    17
      this match {
57910
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 57905
diff changeset
    18
        case Command_Span(name, _) => if (name != "") name else "<command>"
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    19
        case Ignored_Span => "<ignored>"
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    20
        case Malformed_Span => "<malformed>"
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    21
      }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    22
  }
57910
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 57905
diff changeset
    23
  case class Command_Span(name: String, pos: Position.T) extends Kind
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    24
  case object Ignored_Span extends Kind
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    25
  case object Malformed_Span extends Kind
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    26
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    27
  sealed case class Span(kind: Kind, content: List[Token])
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    28
  {
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59707
diff changeset
    29
    def name: String =
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59707
diff changeset
    30
      kind match { case Command_Span(name, _) => name case _ => "" }
58802
3cc68ec558b0 find command span in buffer;
wenzelm
parents: 57910
diff changeset
    31
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59707
diff changeset
    32
    def position: Position.T =
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59707
diff changeset
    33
      kind match { case Command_Span(_, pos) => pos case _ => Position.none }
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59707
diff changeset
    34
63606
fc3a23763617 support for context block structure in Sidekick;
wenzelm
parents: 59735
diff changeset
    35
    def is_begin: Boolean = content.exists(_.is_begin)
fc3a23763617 support for context block structure in Sidekick;
wenzelm
parents: 59735
diff changeset
    36
    def is_end: Boolean = content.exists(_.is_end)
fc3a23763617 support for context block structure in Sidekick;
wenzelm
parents: 59735
diff changeset
    37
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59707
diff changeset
    38
    def length: Int = (0 /: content)(_ + _.source.length)
59707
740a0ca7e09b clarified span position;
wenzelm
parents: 59689
diff changeset
    39
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    40
    def compact_source: (String, Span) =
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    41
    {
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59707
diff changeset
    42
      val source = Token.implode(content)
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    43
      val content1 = new mutable.ListBuffer[Token]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    44
      var i = 0
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    45
      for (Token(kind, s) <- content) {
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    46
        val n = s.length
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59707
diff changeset
    47
        val s1 = source.substring(i, i + n)
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    48
        content1 += Token(kind, s1)
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    49
        i += n
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    50
      }
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59707
diff changeset
    51
      (source, Span(kind, content1.toList))
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    52
    }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    53
  }
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    54
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    55
  val empty: Span = Span(Ignored_Span, Nil)
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    56
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    57
  def unparsed(source: String): Span =
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    58
    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
65335
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    59
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    60
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    61
  /* XML data representation */
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    62
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    63
  def encode: XML.Encode.T[Span] = (span: Span) =>
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    64
  {
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    65
    import XML.Encode._
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    66
    val kind: T[Kind] =
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    67
      variant(List(
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    68
        { case Command_Span(a, b) => (List(a), properties(b)) },
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    69
        { case Ignored_Span => (Nil, Nil) },
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    70
        { case Malformed_Span => (Nil, Nil) }))
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    71
    pair(kind, list(Token.encode))((span.kind, span.content))
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    72
  }
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    73
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    74
  def decode: XML.Decode.T[Span] = (body: XML.Body) =>
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    75
  {
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    76
    import XML.Decode._
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    77
    val kind: T[Kind] =
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    78
      variant(List(
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    79
        { case (List(a), b) => Command_Span(a, properties(b)) },
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    80
        { case (Nil, Nil) => Ignored_Span },
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    81
        { case (Nil, Nil) => Malformed_Span }))
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    82
    val (k, toks) = pair(kind, list(Token.decode))(body)
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    83
    Span(k, toks)
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 63606
diff changeset
    84
  }
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff changeset
    85
}