src/Pure/Thy/thy_syntax.scala
author wenzelm
Sun Mar 04 16:02:14 2012 +0100 (2012-03-04)
changeset 46811 03a2dc9e0624
parent 46749 042c546d2bac
child 46941 c0f776b661fa
permissions -rw-r--r--
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
simplified signatures;
wenzelm@34268
     1
/*  Title:      Pure/Thy/thy_syntax.scala
wenzelm@34268
     2
    Author:     Makarius
wenzelm@34268
     3
wenzelm@38374
     4
Superficial theory syntax: tokens and spans.
wenzelm@34268
     5
*/
wenzelm@34268
     6
wenzelm@34268
     7
package isabelle
wenzelm@34268
     8
wenzelm@34268
     9
wenzelm@38239
    10
import scala.collection.mutable
wenzelm@38374
    11
import scala.annotation.tailrec
wenzelm@38239
    12
wenzelm@38239
    13
wenzelm@34303
    14
object Thy_Syntax
wenzelm@34268
    15
{
wenzelm@40454
    16
  /** nested structure **/
wenzelm@40454
    17
wenzelm@40454
    18
  object Structure
wenzelm@40454
    19
  {
wenzelm@40478
    20
    sealed abstract class Entry { def length: Int }
wenzelm@40454
    21
    case class Block(val name: String, val body: List[Entry]) extends Entry
wenzelm@40454
    22
    {
wenzelm@40454
    23
      val length: Int = (0 /: body)(_ + _.length)
wenzelm@40454
    24
    }
wenzelm@40454
    25
    case class Atom(val command: Command) extends Entry
wenzelm@40454
    26
    {
wenzelm@40454
    27
      def length: Int = command.length
wenzelm@40454
    28
    }
wenzelm@40454
    29
wenzelm@46811
    30
    def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
wenzelm@40454
    31
    {
wenzelm@40454
    32
      /* stack operations */
wenzelm@40454
    33
wenzelm@40454
    34
      def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
wenzelm@44615
    35
      var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
wenzelm@44615
    36
        List((0, "theory " + node_name.theory, buffer()))
wenzelm@40454
    37
wenzelm@40454
    38
      @tailrec def close(level: Int => Boolean)
wenzelm@40454
    39
      {
wenzelm@40454
    40
        stack match {
wenzelm@40454
    41
          case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
wenzelm@40454
    42
            body2 += Block(name, body.toList)
wenzelm@40454
    43
            stack = stack.tail
wenzelm@40454
    44
            close(level)
wenzelm@40454
    45
          case _ =>
wenzelm@40454
    46
        }
wenzelm@40454
    47
      }
wenzelm@40454
    48
wenzelm@40454
    49
      def result(): Entry =
wenzelm@40454
    50
      {
wenzelm@40454
    51
        close(_ => true)
wenzelm@40454
    52
        val (_, name, body) = stack.head
wenzelm@40454
    53
        Block(name, body.toList)
wenzelm@40454
    54
      }
wenzelm@40454
    55
wenzelm@40454
    56
      def add(command: Command)
wenzelm@40454
    57
      {
wenzelm@40454
    58
        syntax.heading_level(command) match {
wenzelm@40454
    59
          case Some(i) =>
wenzelm@40457
    60
            close(_ >= i)
wenzelm@40454
    61
            stack = (i, command.source, buffer()) :: stack
wenzelm@40454
    62
          case None =>
wenzelm@40454
    63
        }
wenzelm@40454
    64
        stack.head._3 += Atom(command)
wenzelm@40454
    65
      }
wenzelm@40454
    66
wenzelm@40454
    67
wenzelm@40454
    68
      /* result structure */
wenzelm@40454
    69
wenzelm@40454
    70
      val spans = parse_spans(syntax.scan(text))
wenzelm@45644
    71
      spans.foreach(span => add(Command(node_name, span)))
wenzelm@40454
    72
      result()
wenzelm@40454
    73
    }
wenzelm@40454
    74
  }
wenzelm@40454
    75
wenzelm@40454
    76
wenzelm@40454
    77
wenzelm@38374
    78
  /** parse spans **/
wenzelm@38374
    79
wenzelm@38373
    80
  def parse_spans(toks: List[Token]): List[List[Token]] =
wenzelm@34268
    81
  {
wenzelm@38373
    82
    val result = new mutable.ListBuffer[List[Token]]
wenzelm@38239
    83
    val span = new mutable.ListBuffer[Token]
wenzelm@34268
    84
wenzelm@46811
    85
    def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
wenzelm@46811
    86
    for (tok <- toks) { if (tok.is_command) flush(); span += tok }
wenzelm@46811
    87
    flush()
wenzelm@38239
    88
    result.toList
wenzelm@34268
    89
  }
wenzelm@38374
    90
wenzelm@38374
    91
wenzelm@38374
    92
wenzelm@44436
    93
  /** perspective **/
wenzelm@44388
    94
wenzelm@44388
    95
  def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
wenzelm@44388
    96
  {
wenzelm@44474
    97
    if (perspective.is_empty) Command.Perspective.empty
wenzelm@44388
    98
    else {
wenzelm@44388
    99
      val result = new mutable.ListBuffer[Command]
wenzelm@44388
   100
      @tailrec
wenzelm@44388
   101
      def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
wenzelm@44388
   102
      {
wenzelm@44388
   103
        (ranges, commands) match {
wenzelm@44388
   104
          case (range :: more_ranges, (command, offset) #:: more_commands) =>
wenzelm@44388
   105
            val command_range = command.range + offset
wenzelm@44388
   106
            range compare command_range match {
wenzelm@44388
   107
              case -1 => check_ranges(more_ranges, commands)
wenzelm@44388
   108
              case 0 =>
wenzelm@44388
   109
                result += command
wenzelm@44388
   110
                check_ranges(ranges, more_commands)
wenzelm@44388
   111
              case 1 => check_ranges(ranges, more_commands)
wenzelm@44388
   112
            }
wenzelm@44388
   113
          case _ =>
wenzelm@44388
   114
        }
wenzelm@44388
   115
      }
wenzelm@44473
   116
      check_ranges(perspective.ranges, node.command_range(perspective.range).toStream)
wenzelm@44474
   117
      Command.Perspective(result.toList)
wenzelm@44388
   118
    }
wenzelm@44388
   119
  }
wenzelm@44388
   120
wenzelm@44615
   121
  def update_perspective(nodes: Document.Nodes,
wenzelm@44615
   122
      name: Document.Node.Name, text_perspective: Text.Perspective)
wenzelm@44436
   123
    : (Command.Perspective, Option[Document.Nodes]) =
wenzelm@44436
   124
  {
wenzelm@44436
   125
    val node = nodes(name)
wenzelm@44436
   126
    val perspective = command_perspective(node, text_perspective)
wenzelm@44436
   127
    val new_nodes =
wenzelm@44474
   128
      if (node.perspective same perspective) None
wenzelm@46680
   129
      else Some(nodes + (name -> node.update_perspective(perspective)))
wenzelm@44436
   130
    (perspective, new_nodes)
wenzelm@44436
   131
  }
wenzelm@44436
   132
wenzelm@44615
   133
  def edit_perspective(previous: Document.Version,
wenzelm@44615
   134
      name: Document.Node.Name, text_perspective: Text.Perspective)
wenzelm@44436
   135
    : (Command.Perspective, Document.Version) =
wenzelm@44436
   136
  {
wenzelm@44436
   137
    val nodes = previous.nodes
wenzelm@44436
   138
    val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
wenzelm@46681
   139
    val version = Document.Version.make(new_nodes getOrElse nodes)
wenzelm@44436
   140
    (perspective, version)
wenzelm@44436
   141
  }
wenzelm@44436
   142
wenzelm@44388
   143
wenzelm@44388
   144
wenzelm@38374
   145
  /** text edits **/
wenzelm@38374
   146
wenzelm@43722
   147
  def text_edits(
wenzelm@43722
   148
      syntax: Outer_Syntax,
wenzelm@43722
   149
      previous: Document.Version,
wenzelm@44157
   150
      edits: List[Document.Edit_Text])
wenzelm@44157
   151
    : (List[Document.Edit_Command], Document.Version) =
wenzelm@38374
   152
  {
wenzelm@38374
   153
    /* phase 1: edit individual command source */
wenzelm@38374
   154
wenzelm@38425
   155
    @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
wenzelm@38374
   156
        : Linear_Set[Command] =
wenzelm@38374
   157
    {
wenzelm@38374
   158
      eds match {
wenzelm@38374
   159
        case e :: es =>
wenzelm@38374
   160
          Document.Node.command_starts(commands.iterator).find {
wenzelm@38374
   161
            case (cmd, cmd_start) =>
wenzelm@38374
   162
              e.can_edit(cmd.source, cmd_start) ||
wenzelm@38374
   163
                e.is_insert && e.start == cmd_start + cmd.length
wenzelm@38374
   164
          } match {
wenzelm@38374
   165
            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
wenzelm@38374
   166
              val (rest, text) = e.edit(cmd.source, cmd_start)
wenzelm@38374
   167
              val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
wenzelm@38374
   168
              edit_text(rest.toList ::: es, new_commands)
wenzelm@38374
   169
wenzelm@38374
   170
            case Some((cmd, cmd_start)) =>
wenzelm@38374
   171
              edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
wenzelm@38374
   172
wenzelm@38374
   173
            case None =>
wenzelm@38374
   174
              require(e.is_insert && e.start == 0)
wenzelm@38374
   175
              edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
wenzelm@38374
   176
          }
wenzelm@38374
   177
        case Nil => commands
wenzelm@38374
   178
      }
wenzelm@38374
   179
    }
wenzelm@38374
   180
wenzelm@38374
   181
wenzelm@38374
   182
    /* phase 2: recover command spans */
wenzelm@38374
   183
wenzelm@44615
   184
    @tailrec def recover_spans(node_name: Document.Node.Name, commands: Linear_Set[Command])
wenzelm@44607
   185
      : Linear_Set[Command] =
wenzelm@38374
   186
    {
wenzelm@44385
   187
      commands.iterator.find(cmd => !cmd.is_defined) match {
wenzelm@38374
   188
        case Some(first_unparsed) =>
wenzelm@38374
   189
          val first =
wenzelm@38878
   190
            commands.reverse_iterator(first_unparsed).
wenzelm@38878
   191
              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
wenzelm@38374
   192
          val last =
wenzelm@38878
   193
            commands.iterator(first_unparsed).
wenzelm@38878
   194
              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
wenzelm@38374
   195
          val range =
wenzelm@38374
   196
            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
wenzelm@38374
   197
wenzelm@38374
   198
          val sources = range.flatMap(_.span.map(_.source))
wenzelm@43647
   199
          val spans0 = parse_spans(syntax.scan(sources.mkString))
wenzelm@38374
   200
wenzelm@38374
   201
          val (before_edit, spans1) =
wenzelm@38374
   202
            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
wenzelm@38374
   203
              (Some(first), spans0.tail)
wenzelm@38374
   204
            else (commands.prev(first), spans0)
wenzelm@38374
   205
wenzelm@38374
   206
          val (after_edit, spans2) =
wenzelm@38374
   207
            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
wenzelm@38374
   208
              (Some(last), spans1.take(spans1.length - 1))
wenzelm@38374
   209
            else (commands.next(last), spans1)
wenzelm@38374
   210
wenzelm@45644
   211
          val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
wenzelm@38374
   212
          val new_commands =
wenzelm@38374
   213
            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
wenzelm@44607
   214
          recover_spans(node_name, new_commands)
wenzelm@38374
   215
wenzelm@38374
   216
        case None => commands
wenzelm@38374
   217
      }
wenzelm@38374
   218
    }
wenzelm@38374
   219
wenzelm@38374
   220
wenzelm@38374
   221
    /* resulting document edits */
wenzelm@38374
   222
wenzelm@38374
   223
    {
wenzelm@40479
   224
      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
wenzelm@38417
   225
      var nodes = previous.nodes
wenzelm@38374
   226
wenzelm@40478
   227
      edits foreach {
wenzelm@44185
   228
        case (name, Document.Node.Clear()) =>
wenzelm@44185
   229
          doc_edits += (name -> Document.Node.Clear())
wenzelm@44443
   230
          nodes += (name -> nodes(name).clear)
wenzelm@40478
   231
wenzelm@44156
   232
        case (name, Document.Node.Edits(text_edits)) =>
wenzelm@43697
   233
          val node = nodes(name)
wenzelm@43697
   234
          val commands0 = node.commands
wenzelm@40478
   235
          val commands1 = edit_text(text_edits, commands0)
wenzelm@44607
   236
          val commands2 = recover_spans(name, commands1)   // FIXME somewhat slow
wenzelm@38374
   237
wenzelm@40478
   238
          val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
wenzelm@40478
   239
          val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
wenzelm@38374
   240
wenzelm@40478
   241
          val cmd_edits =
wenzelm@40478
   242
            removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
wenzelm@40478
   243
            inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
wenzelm@38374
   244
wenzelm@44156
   245
          doc_edits += (name -> Document.Node.Edits(cmd_edits))
wenzelm@46680
   246
          nodes += (name -> node.update_commands(commands2))
wenzelm@43722
   247
wenzelm@44182
   248
        case (name, Document.Node.Header(header)) =>
wenzelm@44157
   249
          val node = nodes(name)
wenzelm@44157
   250
          val update_header =
wenzelm@44182
   251
            (node.header, header) match {
wenzelm@46749
   252
              case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
wenzelm@44160
   253
              case _ => true
wenzelm@44157
   254
            }
wenzelm@44180
   255
          if (update_header) {
wenzelm@44182
   256
            doc_edits += (name -> Document.Node.Header(header))
wenzelm@46680
   257
            nodes += (name -> node.update_header(header))
wenzelm@44180
   258
          }
wenzelm@44385
   259
wenzelm@44385
   260
        case (name, Document.Node.Perspective(text_perspective)) =>
wenzelm@44436
   261
          update_perspective(nodes, name, text_perspective) match {
wenzelm@44436
   262
            case (_, None) =>
wenzelm@44436
   263
            case (perspective, Some(nodes1)) =>
wenzelm@44436
   264
              doc_edits += (name -> Document.Node.Perspective(perspective))
wenzelm@44436
   265
              nodes = nodes1
wenzelm@44385
   266
          }
wenzelm@38374
   267
      }
wenzelm@46681
   268
      (doc_edits.toList, Document.Version.make(nodes))
wenzelm@38374
   269
    }
wenzelm@38374
   270
  }
wenzelm@34268
   271
}