src/Pure/Thy/thy_syntax.scala
changeset 76893 7c3d50ffaece
parent 76702 94cdf6513f01
child 76903 f9de9c4b2156
equal deleted inserted replaced
76892:7fd3e461d3b6 76893:7c3d50ffaece
    17   def command_perspective(
    17   def command_perspective(
    18     node: Document.Node,
    18     node: Document.Node,
    19     perspective: Text.Perspective,
    19     perspective: Text.Perspective,
    20     overlays: Document.Node.Overlays
    20     overlays: Document.Node.Overlays
    21   ): (Command.Perspective, Command.Perspective) = {
    21   ): (Command.Perspective, Command.Perspective) = {
    22     if (perspective.is_empty && overlays.is_empty)
    22     if (perspective.is_empty && overlays.is_empty) {
    23       (Command.Perspective.empty, Command.Perspective.empty)
    23       (Command.Perspective.empty, Command.Perspective.empty)
       
    24     }
    24     else {
    25     else {
    25       val has_overlay = overlays.commands
    26       val has_overlay = overlays.commands
    26       val visible = new mutable.ListBuffer[Command]
    27       val visible = new mutable.ListBuffer[Command]
    27       val visible_overlay = new mutable.ListBuffer[Command]
    28       val visible_overlay = new mutable.ListBuffer[Command]
    28       @tailrec def check_ranges(
    29       @tailrec def check_ranges(
   213     resources: Resources,
   214     resources: Resources,
   214     syntax: Outer_Syntax,
   215     syntax: Outer_Syntax,
   215     get_blob: Document.Node.Name => Option[Document.Blob],
   216     get_blob: Document.Node.Name => Option[Document.Blob],
   216     can_import: Document.Node.Name => Boolean,
   217     can_import: Document.Node.Name => Boolean,
   217     reparse_limit: Int,
   218     reparse_limit: Int,
   218     node: Document.Node, edit: Document.Edit_Text
   219     node: Document.Node,
       
   220     edit: Document.Edit_Text
   219   ): Document.Node = {
   221   ): Document.Node = {
   220     /* recover command spans after edits */
   222     /* recover command spans after edits */
   221     // FIXME somewhat slow
   223     // FIXME somewhat slow
   222     def recover_spans(
   224     def recover_spans(
   223       name: Document.Node.Name,
   225       name: Document.Node.Name,
   311       if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
   313       if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
   312       else {
   314       else {
   313         val reparse =
   315         val reparse =
   314           nodes0.iterator.foldLeft(syntax_changed) {
   316           nodes0.iterator.foldLeft(syntax_changed) {
   315             case (reparse, (name, node)) =>
   317             case (reparse, (name, node)) =>
   316               if (node.load_commands_changed(doc_blobs) && !reparse.contains(name))
   318               if (node.load_commands_changed(doc_blobs) && !reparse.contains(name)) {
   317                 name :: reparse
   319                 name :: reparse
       
   320               }
   318               else reparse
   321               else reparse
   319           }
   322           }
   320         val reparse_set = reparse.toSet
   323         val reparse_set = reparse.toSet
   321 
   324 
   322         var nodes = nodes0
   325         var nodes = nodes0
   331             val node = nodes(name)
   334             val node = nodes(name)
   332             val syntax = resources.session_base.node_syntax(nodes, name)
   335             val syntax = resources.session_base.node_syntax(nodes, name)
   333             val commands = node.commands
   336             val commands = node.commands
   334 
   337 
   335             val node1 =
   338             val node1 =
   336               if (reparse_set(name) && commands.nonEmpty)
   339               if (reparse_set(name) && commands.nonEmpty) {
   337                 node.update_commands(
   340                 node.update_commands(
   338                   reparse_spans(resources, syntax, get_blob, can_import, name,
   341                   reparse_spans(resources, syntax, get_blob, can_import, name,
   339                     commands, commands.head, commands.last))
   342                     commands, commands.head, commands.last))
       
   343               }
   340               else node
   344               else node
   341             val node2 =
   345             val node2 =
   342               edits.foldLeft(node1)(
   346               edits.foldLeft(node1)(
   343                 text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
   347                 text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
   344             val node3 =
   348             val node3 =
   345               if (reparse_set.contains(name))
   349               if (reparse_set.contains(name)) {
   346                 text_edit(resources, syntax, get_blob, can_import, reparse_limit,
   350                 text_edit(resources, syntax, get_blob, can_import, reparse_limit,
   347                   node2, (name, node2.edit_perspective))
   351                   node2, (name, node2.edit_perspective))
       
   352               }
   348               else node2
   353               else node2
   349 
   354 
   350             if (!node.same_perspective(node3.text_perspective, node3.perspective))
   355             if (!node.same_perspective(node3.text_perspective, node3.perspective)) {
   351               doc_edits += (name -> node3.perspective)
   356               doc_edits += (name -> node3.perspective)
       
   357             }
   352 
   358 
   353             doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
   359             doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
   354 
   360 
   355             nodes += (name -> node3)
   361             nodes += (name -> node3)
   356         }
   362         }