src/Pure/Thy/thy_syntax.scala
changeset 56316 b1cf8ddc2e04
parent 56315 c20053f67093
child 56335 8953d4cc060a
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 10:17:09 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 10:49:32 2014 +0100
     1.3 @@ -156,7 +156,8 @@
     1.4      base_syntax: Outer_Syntax,
     1.5      previous: Document.Version,
     1.6      edits: List[Document.Edit_Text]):
     1.7 -    ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
     1.8 +    (Outer_Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
     1.9 +      List[Document.Edit_Command]) =
    1.10    {
    1.11      var updated_imports = false
    1.12      var updated_keywords = false
    1.13 @@ -178,7 +179,7 @@
    1.14        case _ =>
    1.15      }
    1.16  
    1.17 -    val syntax =
    1.18 +    val (syntax, syntax_changed) =
    1.19        if (previous.is_init || updated_keywords) {
    1.20          val syntax =
    1.21            (base_syntax /: nodes.entries) {
    1.22 @@ -193,7 +194,7 @@
    1.23          nodes.descendants(doc_edits.iterator.map(_._1).toList)
    1.24        else Nil
    1.25  
    1.26 -    (syntax, reparse, nodes, doc_edits.toList)
    1.27 +    (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList)
    1.28    }
    1.29  
    1.30  
    1.31 @@ -431,62 +432,59 @@
    1.32      }
    1.33    }
    1.34  
    1.35 -  def parse_edits(
    1.36 +  def parse_change(
    1.37        resources: Resources,
    1.38        reparse_limit: Int,
    1.39        previous: Document.Version,
    1.40        doc_blobs: Document.Blobs,
    1.41        edits: List[Document.Edit_Text]): Session.Change =
    1.42    {
    1.43 -    val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
    1.44 +    val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
    1.45        header_edits(resources.base_syntax, previous, edits)
    1.46  
    1.47 -    if (edits.isEmpty)
    1.48 -      Session.Change(previous, doc_blobs, false, Nil, Document.Version.make(syntax, previous.nodes))
    1.49 -    else {
    1.50 -      val reparse =
    1.51 -        (reparse0 /: nodes0.entries)({
    1.52 -          case (reparse, (name, node)) =>
    1.53 -            if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
    1.54 -              name :: reparse
    1.55 -            else reparse
    1.56 -          })
    1.57 -      val reparse_set = reparse.toSet
    1.58 +    val (doc_edits, version) =
    1.59 +      if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
    1.60 +      else {
    1.61 +        val reparse =
    1.62 +          (reparse0 /: nodes0.entries)({
    1.63 +            case (reparse, (name, node)) =>
    1.64 +              if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
    1.65 +                name :: reparse
    1.66 +              else reparse
    1.67 +            })
    1.68 +        val reparse_set = reparse.toSet
    1.69  
    1.70 -      var nodes = nodes0
    1.71 -      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
    1.72 +        var nodes = nodes0
    1.73 +        val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
    1.74  
    1.75 -      val node_edits =
    1.76 -        (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
    1.77 -          .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
    1.78 +        val node_edits =
    1.79 +          (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
    1.80 +            .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
    1.81  
    1.82 -      node_edits foreach {
    1.83 -        case (name, edits) =>
    1.84 -          val node = nodes(name)
    1.85 -          val commands = node.commands
    1.86 +        node_edits foreach {
    1.87 +          case (name, edits) =>
    1.88 +            val node = nodes(name)
    1.89 +            val commands = node.commands
    1.90  
    1.91 -          val node1 =
    1.92 -            if (reparse_set(name) && !commands.isEmpty)
    1.93 -              node.update_commands(
    1.94 -                reparse_spans(resources, syntax, doc_blobs,
    1.95 -                  name, commands, commands.head, commands.last))
    1.96 -            else node
    1.97 -          val node2 = (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
    1.98 +            val node1 =
    1.99 +              if (reparse_set(name) && !commands.isEmpty)
   1.100 +                node.update_commands(
   1.101 +                  reparse_spans(resources, syntax, doc_blobs,
   1.102 +                    name, commands, commands.head, commands.last))
   1.103 +              else node
   1.104 +            val node2 =
   1.105 +              (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
   1.106  
   1.107 -          if (!(node.same_perspective(node2.perspective)))
   1.108 -            doc_edits += (name -> node2.perspective)
   1.109 +            if (!(node.same_perspective(node2.perspective)))
   1.110 +              doc_edits += (name -> node2.perspective)
   1.111  
   1.112 -          doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
   1.113 +            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
   1.114  
   1.115 -          nodes += (name -> node2)
   1.116 +            nodes += (name -> node2)
   1.117 +        }
   1.118 +        (doc_edits.toList, Document.Version.make(syntax, nodes))
   1.119        }
   1.120  
   1.121 -      Session.Change(
   1.122 -        previous,
   1.123 -        doc_blobs,
   1.124 -        syntax_changed,
   1.125 -        doc_edits.toList,
   1.126 -        Document.Version.make(syntax, nodes))
   1.127 -    }
   1.128 +    Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
   1.129    }
   1.130  }