src/Pure/Thy/thy_syntax.scala
author wenzelm
Mon Aug 11 22:43:26 2014 +0200 (2014-08-11)
changeset 57902 3f1fd41ee821
parent 57901 e1abca2527da
child 57904 922273b7bf8a
permissions -rw-r--r--
tuned output, in accordance to transaction name in ML;
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@57901
    16
  /** spans **/
wenzelm@38374
    17
wenzelm@57902
    18
  sealed abstract class Span_Kind {
wenzelm@57902
    19
    override def toString: String =
wenzelm@57902
    20
      this match {
wenzelm@57902
    21
        case Command_Span(name) => if (name != "") name else "<command>"
wenzelm@57902
    22
        case Ignored_Span => "<ignored>"
wenzelm@57902
    23
        case Malformed_Span => "<malformed>"
wenzelm@57902
    24
      }
wenzelm@57902
    25
  }
wenzelm@57901
    26
  case class Command_Span(name: String) extends Span_Kind
wenzelm@57901
    27
  case object Ignored_Span extends Span_Kind
wenzelm@57901
    28
  case object Malformed_Span extends Span_Kind
wenzelm@57901
    29
wenzelm@57901
    30
  sealed case class Span(kind: Span_Kind, content: List[Token])
wenzelm@34268
    31
  {
wenzelm@57901
    32
    def compact_source: (String, Span) =
wenzelm@57901
    33
    {
wenzelm@57901
    34
      val source: String =
wenzelm@57901
    35
        content match {
wenzelm@57901
    36
          case List(tok) => tok.source
wenzelm@57901
    37
          case toks => toks.map(_.source).mkString
wenzelm@57901
    38
        }
wenzelm@57901
    39
wenzelm@57901
    40
      val content1 = new mutable.ListBuffer[Token]
wenzelm@57901
    41
      var i = 0
wenzelm@57901
    42
      for (Token(kind, s) <- content) {
wenzelm@57901
    43
        val n = s.length
wenzelm@57901
    44
        val s1 = source.substring(i, i + n)
wenzelm@57901
    45
        content1 += Token(kind, s1)
wenzelm@57901
    46
        i += n
wenzelm@57901
    47
      }
wenzelm@57901
    48
      (source, Span(kind, content1.toList))
wenzelm@57901
    49
    }
wenzelm@57901
    50
  }
wenzelm@57901
    51
wenzelm@57901
    52
  val empty_span: Span = Span(Ignored_Span, Nil)
wenzelm@57901
    53
wenzelm@57901
    54
  def unparsed_span(source: String): Span =
wenzelm@57901
    55
    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
wenzelm@57901
    56
wenzelm@57901
    57
wenzelm@57901
    58
  /* parse */
wenzelm@57901
    59
wenzelm@57901
    60
  def parse_spans(toks: List[Token]): List[Span] =
wenzelm@57901
    61
  {
wenzelm@57901
    62
    val result = new mutable.ListBuffer[Span]
wenzelm@57901
    63
    val content = new mutable.ListBuffer[Token]
wenzelm@53843
    64
    val improper = new mutable.ListBuffer[Token]
wenzelm@34268
    65
wenzelm@57901
    66
    def ship(span: List[Token])
wenzelm@57901
    67
    {
wenzelm@57901
    68
      val kind =
wenzelm@57901
    69
        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
wenzelm@57901
    70
          Command_Span(span.head.source)
wenzelm@57901
    71
        else if (span.forall(_.is_improper)) Ignored_Span
wenzelm@57901
    72
        else Malformed_Span
wenzelm@57901
    73
      result += Span(kind, span)
wenzelm@57901
    74
    }
wenzelm@57901
    75
wenzelm@53843
    76
    def flush()
wenzelm@53843
    77
    {
wenzelm@57901
    78
      if (!content.isEmpty) { ship(content.toList); content.clear }
wenzelm@57901
    79
      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
wenzelm@53843
    80
    }
wenzelm@57901
    81
wenzelm@53843
    82
    for (tok <- toks) {
wenzelm@57901
    83
      if (tok.is_command) { flush(); content += tok }
wenzelm@53843
    84
      else if (tok.is_improper) improper += tok
wenzelm@57901
    85
      else { content ++= improper; improper.clear; content += tok }
wenzelm@53843
    86
    }
wenzelm@46811
    87
    flush()
wenzelm@53843
    88
wenzelm@38239
    89
    result.toList
wenzelm@34268
    90
  }
wenzelm@38374
    91
wenzelm@38374
    92
wenzelm@38374
    93
wenzelm@44436
    94
  /** perspective **/
wenzelm@44388
    95
wenzelm@52861
    96
  def command_perspective(
wenzelm@52861
    97
      node: Document.Node,
wenzelm@52861
    98
      perspective: Text.Perspective,
wenzelm@52887
    99
      overlays: Document.Node.Overlays): (Command.Perspective, Command.Perspective) =
wenzelm@44388
   100
  {
wenzelm@52861
   101
    if (perspective.is_empty && overlays.is_empty)
wenzelm@52861
   102
      (Command.Perspective.empty, Command.Perspective.empty)
wenzelm@44388
   103
    else {
wenzelm@52861
   104
      val has_overlay = overlays.commands
wenzelm@52861
   105
      val visible = new mutable.ListBuffer[Command]
wenzelm@52861
   106
      val visible_overlay = new mutable.ListBuffer[Command]
wenzelm@44388
   107
      @tailrec
wenzelm@44388
   108
      def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
wenzelm@44388
   109
      {
wenzelm@44388
   110
        (ranges, commands) match {
wenzelm@44388
   111
          case (range :: more_ranges, (command, offset) #:: more_commands) =>
wenzelm@44388
   112
            val command_range = command.range + offset
wenzelm@44388
   113
            range compare command_range match {
wenzelm@44388
   114
              case 0 =>
wenzelm@52861
   115
                visible += command
wenzelm@52861
   116
                visible_overlay += command
wenzelm@44388
   117
                check_ranges(ranges, more_commands)
wenzelm@52861
   118
              case c =>
wenzelm@52861
   119
                if (has_overlay(command)) visible_overlay += command
wenzelm@52861
   120
wenzelm@52861
   121
                if (c < 0) check_ranges(more_ranges, commands)
wenzelm@52861
   122
                else check_ranges(ranges, more_commands)
wenzelm@44388
   123
            }
wenzelm@52861
   124
wenzelm@52861
   125
          case (Nil, (command, _) #:: more_commands) =>
wenzelm@52861
   126
            if (has_overlay(command)) visible_overlay += command
wenzelm@52861
   127
wenzelm@52861
   128
            check_ranges(Nil, more_commands)
wenzelm@52861
   129
wenzelm@44388
   130
          case _ =>
wenzelm@44388
   131
        }
wenzelm@44388
   132
      }
wenzelm@52861
   133
wenzelm@52861
   134
      val commands =
wenzelm@56373
   135
        (if (overlays.is_empty) node.command_iterator(perspective.range)
wenzelm@56373
   136
         else node.command_iterator()).toStream
wenzelm@56373
   137
      check_ranges(perspective.ranges, commands)
wenzelm@52861
   138
      (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
wenzelm@44388
   139
    }
wenzelm@44388
   140
  }
wenzelm@44388
   141
wenzelm@44388
   142
wenzelm@44388
   143
wenzelm@46946
   144
  /** header edits: structure and outer syntax **/
wenzelm@46946
   145
wenzelm@46946
   146
  private def header_edits(
wenzelm@56394
   147
    resources: Resources,
wenzelm@46946
   148
    previous: Document.Version,
wenzelm@55134
   149
    edits: List[Document.Edit_Text]):
wenzelm@56393
   150
    (Prover.Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
wenzelm@56316
   151
      List[Document.Edit_Command]) =
wenzelm@46946
   152
  {
wenzelm@47987
   153
    var updated_imports = false
wenzelm@47987
   154
    var updated_keywords = false
wenzelm@46946
   155
    var nodes = previous.nodes
wenzelm@46946
   156
    val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
wenzelm@46946
   157
wenzelm@46946
   158
    edits foreach {
wenzelm@48707
   159
      case (name, Document.Node.Deps(header)) =>
wenzelm@46946
   160
        val node = nodes(name)
wenzelm@46946
   161
        val update_header =
wenzelm@48707
   162
          !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
wenzelm@46946
   163
        if (update_header) {
wenzelm@46946
   164
          val node1 = node.update_header(header)
wenzelm@48707
   165
          updated_imports = updated_imports || (node.header.imports != node1.header.imports)
wenzelm@48707
   166
          updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords)
wenzelm@46946
   167
          nodes += (name -> node1)
wenzelm@48707
   168
          doc_edits += (name -> Document.Node.Deps(header))
wenzelm@46946
   169
        }
wenzelm@46946
   170
      case _ =>
wenzelm@46946
   171
    }
wenzelm@46946
   172
wenzelm@56316
   173
    val (syntax, syntax_changed) =
wenzelm@56394
   174
      previous.syntax match {
wenzelm@56394
   175
        case Some(syntax) if !updated_keywords =>
wenzelm@56394
   176
          (syntax, false)
wenzelm@56394
   177
        case _ =>
wenzelm@56394
   178
          val syntax =
wenzelm@56394
   179
            (resources.base_syntax /: nodes.iterator) {
wenzelm@56394
   180
              case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
wenzelm@56394
   181
            }
wenzelm@56394
   182
          (syntax, true)
wenzelm@55134
   183
      }
wenzelm@46946
   184
wenzelm@46946
   185
    val reparse =
wenzelm@47987
   186
      if (updated_imports || updated_keywords)
wenzelm@47987
   187
        nodes.descendants(doc_edits.iterator.map(_._1).toList)
wenzelm@46946
   188
      else Nil
wenzelm@46946
   189
wenzelm@56316
   190
    (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList)
wenzelm@46946
   191
  }
wenzelm@46946
   192
wenzelm@46946
   193
wenzelm@46946
   194
wenzelm@38374
   195
  /** text edits **/
wenzelm@38374
   196
wenzelm@48755
   197
  /* edit individual command source */
wenzelm@46946
   198
wenzelm@50761
   199
  @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@46946
   200
  {
wenzelm@46946
   201
    eds match {
wenzelm@46946
   202
      case e :: es =>
wenzelm@52901
   203
        Document.Node.Commands.starts(commands.iterator).find {
wenzelm@46946
   204
          case (cmd, cmd_start) =>
wenzelm@46946
   205
            e.can_edit(cmd.source, cmd_start) ||
wenzelm@46946
   206
              e.is_insert && e.start == cmd_start + cmd.length
wenzelm@46946
   207
        } match {
wenzelm@46946
   208
          case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
wenzelm@46946
   209
            val (rest, text) = e.edit(cmd.source, cmd_start)
wenzelm@46946
   210
            val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
wenzelm@46946
   211
            edit_text(rest.toList ::: es, new_commands)
wenzelm@46946
   212
wenzelm@46946
   213
          case Some((cmd, cmd_start)) =>
wenzelm@46946
   214
            edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
wenzelm@46946
   215
wenzelm@46946
   216
          case None =>
wenzelm@46946
   217
            require(e.is_insert && e.start == 0)
wenzelm@46946
   218
            edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
wenzelm@46946
   219
        }
wenzelm@46946
   220
      case Nil => commands
wenzelm@46946
   221
    }
wenzelm@46946
   222
  }
wenzelm@46946
   223
wenzelm@46946
   224
wenzelm@54513
   225
  /* inlined files */
wenzelm@54513
   226
wenzelm@54513
   227
  private def find_file(tokens: List[Token]): Option[String] =
wenzelm@54513
   228
  {
wenzelm@54513
   229
    def clean(toks: List[Token]): List[Token] =
wenzelm@54513
   230
      toks match {
wenzelm@54513
   231
        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
wenzelm@54513
   232
        case t :: ts => t :: clean(ts)
wenzelm@54513
   233
        case Nil => Nil
wenzelm@54513
   234
      }
wenzelm@55118
   235
    clean(tokens.filter(_.is_proper)) match {
wenzelm@55118
   236
      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
wenzelm@55118
   237
      case _ => None
wenzelm@55118
   238
    }
wenzelm@54513
   239
  }
wenzelm@54513
   240
wenzelm@57901
   241
  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
wenzelm@57901
   242
    span.kind match {
wenzelm@57901
   243
      case Command_Span(name) =>
wenzelm@57901
   244
        syntax.load_command(name) match {
wenzelm@57901
   245
          case Some(exts) =>
wenzelm@57901
   246
            find_file(span.content) match {
wenzelm@57901
   247
              case Some(file) =>
wenzelm@57901
   248
                if (exts.isEmpty) List(file)
wenzelm@57901
   249
                else exts.map(ext => file + "." + ext)
wenzelm@57901
   250
              case None => Nil
wenzelm@57901
   251
            }
wenzelm@54513
   252
          case None => Nil
wenzelm@54513
   253
        }
wenzelm@57901
   254
      case _ => Nil
wenzelm@54513
   255
    }
wenzelm@54513
   256
wenzelm@54513
   257
  def resolve_files(
wenzelm@56208
   258
      resources: Resources,
wenzelm@56393
   259
      syntax: Prover.Syntax,
wenzelm@54517
   260
      node_name: Document.Node.Name,
wenzelm@57901
   261
      span: Span,
wenzelm@56336
   262
      get_blob: Document.Node.Name => Option[Document.Blob])
wenzelm@54519
   263
    : List[Command.Blob] =
wenzelm@54513
   264
  {
wenzelm@55431
   265
    span_files(syntax, span).map(file_name =>
wenzelm@54517
   266
      Exn.capture {
wenzelm@54517
   267
        val name =
wenzelm@56208
   268
          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
wenzelm@56473
   269
        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
wenzelm@55431
   270
        (name, blob)
wenzelm@55783
   271
      })
wenzelm@54513
   272
  }
wenzelm@54513
   273
wenzelm@54513
   274
wenzelm@48755
   275
  /* reparse range of command spans */
wenzelm@46946
   276
wenzelm@48748
   277
  @tailrec private def chop_common(
wenzelm@55779
   278
      cmds: List[Command],
wenzelm@57901
   279
      blobs_spans: List[(List[Command.Blob], Span)])
wenzelm@57901
   280
    : (List[Command], List[(List[Command.Blob], Span)]) =
wenzelm@55779
   281
  {
wenzelm@55779
   282
    (cmds, blobs_spans) match {
wenzelm@55779
   283
      case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
wenzelm@55779
   284
        chop_common(cmds, rest)
wenzelm@55779
   285
      case _ => (cmds, blobs_spans)
wenzelm@48748
   286
    }
wenzelm@55779
   287
  }
wenzelm@48748
   288
wenzelm@48754
   289
  private def reparse_spans(
wenzelm@56208
   290
    resources: Resources,
wenzelm@56393
   291
    syntax: Prover.Syntax,
wenzelm@56336
   292
    get_blob: Document.Node.Name => Option[Document.Blob],
wenzelm@48754
   293
    name: Document.Node.Name,
wenzelm@48754
   294
    commands: Linear_Set[Command],
wenzelm@48754
   295
    first: Command, last: Command): Linear_Set[Command] =
wenzelm@48748
   296
  {
wenzelm@48754
   297
    val cmds0 = commands.iterator(first, last).toList
wenzelm@55779
   298
    val blobs_spans0 =
wenzelm@54513
   299
      parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
wenzelm@56336
   300
        map(span => (resolve_files(resources, syntax, name, span, get_blob), span))
wenzelm@48754
   301
wenzelm@55779
   302
    val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
wenzelm@48754
   303
wenzelm@55779
   304
    val (rev_cmds2, rev_blobs_spans2) = chop_common(cmds1.reverse, blobs_spans1.reverse)
wenzelm@48754
   305
    val cmds2 = rev_cmds2.reverse
wenzelm@55779
   306
    val blobs_spans2 = rev_blobs_spans2.reverse
wenzelm@48754
   307
wenzelm@48754
   308
    cmds2 match {
wenzelm@48754
   309
      case Nil =>
wenzelm@55779
   310
        assert(blobs_spans2.isEmpty)
wenzelm@48754
   311
        commands
wenzelm@48754
   312
      case cmd :: _ =>
wenzelm@48754
   313
        val hook = commands.prev(cmd)
wenzelm@54462
   314
        val inserted =
wenzelm@55779
   315
          blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
wenzelm@48754
   316
        (commands /: cmds2)(_ - _).append_after(hook, inserted)
wenzelm@48754
   317
    }
wenzelm@48748
   318
  }
wenzelm@48748
   319
wenzelm@48754
   320
wenzelm@48755
   321
  /* recover command spans after edits */
wenzelm@48754
   322
wenzelm@48755
   323
  // FIXME somewhat slow
wenzelm@48746
   324
  private def recover_spans(
wenzelm@56208
   325
    resources: Resources,
wenzelm@56393
   326
    syntax: Prover.Syntax,
wenzelm@56336
   327
    get_blob: Document.Node.Name => Option[Document.Blob],
wenzelm@48754
   328
    name: Document.Node.Name,
wenzelm@48748
   329
    perspective: Command.Perspective,
wenzelm@48754
   330
    commands: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@46946
   331
  {
wenzelm@48754
   332
    val visible = perspective.commands.toSet
wenzelm@48748
   333
wenzelm@48754
   334
    def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
wenzelm@48754
   335
      cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
wenzelm@48754
   336
        .find(_.is_command) getOrElse cmds.last
wenzelm@48746
   337
wenzelm@48754
   338
    @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@48754
   339
      cmds.find(_.is_unparsed) match {
wenzelm@48754
   340
        case Some(first_unparsed) =>
wenzelm@48754
   341
          val first = next_invisible_command(cmds.reverse, first_unparsed)
wenzelm@48754
   342
          val last = next_invisible_command(cmds, first_unparsed)
wenzelm@56336
   343
          recover(reparse_spans(resources, syntax, get_blob, name, cmds, first, last))
wenzelm@48754
   344
        case None => cmds
wenzelm@48746
   345
      }
wenzelm@48754
   346
    recover(commands)
wenzelm@46946
   347
  }
wenzelm@46946
   348
wenzelm@46946
   349
wenzelm@48755
   350
  /* consolidate unfinished spans */
wenzelm@46946
   351
wenzelm@48754
   352
  private def consolidate_spans(
wenzelm@56208
   353
    resources: Resources,
wenzelm@56393
   354
    syntax: Prover.Syntax,
wenzelm@56336
   355
    get_blob: Document.Node.Name => Option[Document.Blob],
wenzelm@49524
   356
    reparse_limit: Int,
wenzelm@48754
   357
    name: Document.Node.Name,
wenzelm@48754
   358
    perspective: Command.Perspective,
wenzelm@46946
   359
    commands: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@46946
   360
  {
wenzelm@48754
   361
    if (perspective.commands.isEmpty) commands
wenzelm@48754
   362
    else {
wenzelm@48754
   363
      commands.find(_.is_unfinished) match {
wenzelm@48754
   364
        case Some(first_unfinished) =>
wenzelm@48754
   365
          val visible = perspective.commands.toSet
wenzelm@48754
   366
          commands.reverse.find(visible) match {
wenzelm@48754
   367
            case Some(last_visible) =>
wenzelm@49524
   368
              val it = commands.iterator(last_visible)
wenzelm@49524
   369
              var last = last_visible
wenzelm@49524
   370
              var i = 0
wenzelm@49524
   371
              while (i < reparse_limit && it.hasNext) {
wenzelm@49524
   372
                last = it.next
wenzelm@49524
   373
                i += last.length
wenzelm@49524
   374
              }
wenzelm@56336
   375
              reparse_spans(resources, syntax, get_blob, name, commands, first_unfinished, last)
wenzelm@48754
   376
            case None => commands
wenzelm@48754
   377
          }
wenzelm@48754
   378
        case None => commands
wenzelm@48754
   379
      }
wenzelm@48754
   380
    }
wenzelm@46946
   381
  }
wenzelm@46946
   382
wenzelm@46946
   383
wenzelm@48755
   384
  /* main */
wenzelm@46946
   385
wenzelm@50761
   386
  def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
wenzelm@52849
   387
    : List[Command.Edit] =
wenzelm@48754
   388
  {
wenzelm@48754
   389
    val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
wenzelm@48754
   390
    val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
wenzelm@48754
   391
wenzelm@48754
   392
    removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) :::
wenzelm@48754
   393
    inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
wenzelm@48754
   394
  }
wenzelm@48754
   395
wenzelm@54513
   396
  private def text_edit(
wenzelm@56208
   397
    resources: Resources,
wenzelm@56393
   398
    syntax: Prover.Syntax,
wenzelm@56336
   399
    get_blob: Document.Node.Name => Option[Document.Blob],
wenzelm@54513
   400
    reparse_limit: Int,
wenzelm@48755
   401
    node: Document.Node, edit: Document.Edit_Text): Document.Node =
wenzelm@48755
   402
  {
wenzelm@48755
   403
    edit match {
wenzelm@48755
   404
      case (_, Document.Node.Clear()) => node.clear
wenzelm@48755
   405
wenzelm@56335
   406
      case (_, Document.Node.Blob(blob)) => node.init_blob(blob)
wenzelm@54562
   407
wenzelm@48755
   408
      case (name, Document.Node.Edits(text_edits)) =>
wenzelm@56335
   409
        if (name.is_theory) {
wenzelm@55435
   410
          val commands0 = node.commands
wenzelm@55435
   411
          val commands1 = edit_text(text_edits, commands0)
wenzelm@55435
   412
          val commands2 =
wenzelm@56336
   413
            recover_spans(resources, syntax, get_blob, name, node.perspective.visible, commands1)
wenzelm@55435
   414
          node.update_commands(commands2)
wenzelm@55435
   415
        }
wenzelm@56335
   416
        else node
wenzelm@48755
   417
wenzelm@48755
   418
      case (_, Document.Node.Deps(_)) => node
wenzelm@48755
   419
wenzelm@52849
   420
      case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
wenzelm@52861
   421
        val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
wenzelm@52849
   422
        val perspective: Document.Node.Perspective_Command =
wenzelm@52861
   423
          Document.Node.Perspective(required, visible_overlay, overlays)
wenzelm@52808
   424
        if (node.same_perspective(perspective)) node
wenzelm@48755
   425
        else
wenzelm@49524
   426
          node.update_perspective(perspective).update_commands(
wenzelm@56336
   427
            consolidate_spans(resources, syntax, get_blob, reparse_limit,
wenzelm@54517
   428
              name, visible, node.commands))
wenzelm@48755
   429
    }
wenzelm@48755
   430
  }
wenzelm@48755
   431
wenzelm@56316
   432
  def parse_change(
wenzelm@56208
   433
      resources: Resources,
wenzelm@49524
   434
      reparse_limit: Int,
wenzelm@43722
   435
      previous: Document.Version,
wenzelm@54521
   436
      doc_blobs: Document.Blobs,
wenzelm@56315
   437
      edits: List[Document.Edit_Text]): Session.Change =
wenzelm@38374
   438
  {
wenzelm@56336
   439
    def get_blob(name: Document.Node.Name) =
wenzelm@56336
   440
      doc_blobs.get(name) orElse previous.nodes(name).get_blob
wenzelm@56336
   441
wenzelm@56316
   442
    val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
wenzelm@56394
   443
      header_edits(resources, previous, edits)
wenzelm@54518
   444
wenzelm@56316
   445
    val (doc_edits, version) =
wenzelm@56394
   446
      if (edits.isEmpty) (Nil, Document.Version.make(Some(syntax), previous.nodes))
wenzelm@56316
   447
      else {
wenzelm@56316
   448
        val reparse =
wenzelm@56372
   449
          (reparse0 /: nodes0.iterator)({
wenzelm@56316
   450
            case (reparse, (name, node)) =>
wenzelm@56316
   451
              if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
wenzelm@56316
   452
                name :: reparse
wenzelm@56316
   453
              else reparse
wenzelm@56316
   454
            })
wenzelm@56316
   455
        val reparse_set = reparse.toSet
wenzelm@46946
   456
wenzelm@56316
   457
        var nodes = nodes0
wenzelm@56316
   458
        val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
wenzelm@54521
   459
wenzelm@56316
   460
        val node_edits =
wenzelm@56316
   461
          (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
wenzelm@56316
   462
            .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
wenzelm@38374
   463
wenzelm@56316
   464
        node_edits foreach {
wenzelm@56316
   465
          case (name, edits) =>
wenzelm@56316
   466
            val node = nodes(name)
wenzelm@56316
   467
            val commands = node.commands
wenzelm@48754
   468
wenzelm@56316
   469
            val node1 =
wenzelm@56316
   470
              if (reparse_set(name) && !commands.isEmpty)
wenzelm@56316
   471
                node.update_commands(
wenzelm@56336
   472
                  reparse_spans(resources, syntax, get_blob,
wenzelm@56316
   473
                    name, commands, commands.head, commands.last))
wenzelm@56316
   474
              else node
wenzelm@56316
   475
            val node2 =
wenzelm@56336
   476
              (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
wenzelm@54521
   477
wenzelm@56316
   478
            if (!(node.same_perspective(node2.perspective)))
wenzelm@56316
   479
              doc_edits += (name -> node2.perspective)
wenzelm@54521
   480
wenzelm@56316
   481
            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
wenzelm@54521
   482
wenzelm@56316
   483
            nodes += (name -> node2)
wenzelm@56316
   484
        }
wenzelm@57625
   485
        (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes))
wenzelm@54513
   486
      }
wenzelm@54513
   487
wenzelm@57842
   488
    Session.Change(previous, syntax_changed, deps_changed, doc_edits, version)
wenzelm@38374
   489
  }
wenzelm@34268
   490
}