propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
authorwenzelm
Sat Mar 29 10:49:32 2014 +0100 (2014-03-29 ago)
changeset 56316b1cf8ddc2e04
parent 56315 c20053f67093
child 56317 1147854080b4
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
tuned signature;
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sat Mar 29 10:17:09 2014 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Mar 29 10:49:32 2014 +0100
     1.3 @@ -91,15 +91,15 @@
     1.4      with_thy_text(name, check_thy_text(name, _))
     1.5  
     1.6  
     1.7 -  /* theory text edits */
     1.8 +  /* document changes */
     1.9  
    1.10 -  def parse_edits(
    1.11 +  def parse_change(
    1.12        reparse_limit: Int,
    1.13        previous: Document.Version,
    1.14        doc_blobs: Document.Blobs,
    1.15        edits: List[Document.Edit_Text]): Session.Change =
    1.16 -    Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits)
    1.17 +    Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
    1.18  
    1.19 -  def syntax_changed() { }
    1.20 +  def commit(change: Session.Change) { }
    1.21  }
    1.22  
     2.1 --- a/src/Pure/PIDE/session.scala	Sat Mar 29 10:17:09 2014 +0100
     2.2 +++ b/src/Pure/PIDE/session.scala	Sat Mar 29 10:49:32 2014 +0100
     2.3 @@ -24,6 +24,7 @@
     2.4      previous: Document.Version,
     2.5      doc_blobs: Document.Blobs,
     2.6      syntax_changed: Boolean,
     2.7 +    deps_changed: Boolean,
     2.8      doc_edits: List[Document.Edit_Command],
     2.9      version: Document.Version)
    2.10  
    2.11 @@ -190,8 +191,8 @@
    2.12          case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
    2.13            val prev = previous.get_finished
    2.14            val change =
    2.15 -            Timing.timeit("parse_edits", timing) {
    2.16 -              resources.parse_edits(reparse_limit, prev, doc_blobs, text_edits)
    2.17 +            Timing.timeit("parse_change", timing) {
    2.18 +              resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
    2.19              }
    2.20            version_result.fulfill(change.version)
    2.21            sender ! change
    2.22 @@ -402,8 +403,7 @@
    2.23        val assignment = global_state().the_assignment(change.previous).check_finished
    2.24        global_state >> (_.define_version(change.version, assignment))
    2.25        prover.get.update(change.previous.id, change.version.id, change.doc_edits)
    2.26 -
    2.27 -      if (change.syntax_changed) resources.syntax_changed()
    2.28 +      resources.commit(change)
    2.29      }
    2.30      //}}}
    2.31  
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 10:17:09 2014 +0100
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 10:49:32 2014 +0100
     3.3 @@ -156,7 +156,8 @@
     3.4      base_syntax: Outer_Syntax,
     3.5      previous: Document.Version,
     3.6      edits: List[Document.Edit_Text]):
     3.7 -    ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
     3.8 +    (Outer_Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
     3.9 +      List[Document.Edit_Command]) =
    3.10    {
    3.11      var updated_imports = false
    3.12      var updated_keywords = false
    3.13 @@ -178,7 +179,7 @@
    3.14        case _ =>
    3.15      }
    3.16  
    3.17 -    val syntax =
    3.18 +    val (syntax, syntax_changed) =
    3.19        if (previous.is_init || updated_keywords) {
    3.20          val syntax =
    3.21            (base_syntax /: nodes.entries) {
    3.22 @@ -193,7 +194,7 @@
    3.23          nodes.descendants(doc_edits.iterator.map(_._1).toList)
    3.24        else Nil
    3.25  
    3.26 -    (syntax, reparse, nodes, doc_edits.toList)
    3.27 +    (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList)
    3.28    }
    3.29  
    3.30  
    3.31 @@ -431,62 +432,59 @@
    3.32      }
    3.33    }
    3.34  
    3.35 -  def parse_edits(
    3.36 +  def parse_change(
    3.37        resources: Resources,
    3.38        reparse_limit: Int,
    3.39        previous: Document.Version,
    3.40        doc_blobs: Document.Blobs,
    3.41        edits: List[Document.Edit_Text]): Session.Change =
    3.42    {
    3.43 -    val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
    3.44 +    val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
    3.45        header_edits(resources.base_syntax, previous, edits)
    3.46  
    3.47 -    if (edits.isEmpty)
    3.48 -      Session.Change(previous, doc_blobs, false, Nil, Document.Version.make(syntax, previous.nodes))
    3.49 -    else {
    3.50 -      val reparse =
    3.51 -        (reparse0 /: nodes0.entries)({
    3.52 -          case (reparse, (name, node)) =>
    3.53 -            if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
    3.54 -              name :: reparse
    3.55 -            else reparse
    3.56 -          })
    3.57 -      val reparse_set = reparse.toSet
    3.58 +    val (doc_edits, version) =
    3.59 +      if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
    3.60 +      else {
    3.61 +        val reparse =
    3.62 +          (reparse0 /: nodes0.entries)({
    3.63 +            case (reparse, (name, node)) =>
    3.64 +              if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
    3.65 +                name :: reparse
    3.66 +              else reparse
    3.67 +            })
    3.68 +        val reparse_set = reparse.toSet
    3.69  
    3.70 -      var nodes = nodes0
    3.71 -      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
    3.72 +        var nodes = nodes0
    3.73 +        val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
    3.74  
    3.75 -      val node_edits =
    3.76 -        (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
    3.77 -          .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
    3.78 +        val node_edits =
    3.79 +          (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
    3.80 +            .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
    3.81  
    3.82 -      node_edits foreach {
    3.83 -        case (name, edits) =>
    3.84 -          val node = nodes(name)
    3.85 -          val commands = node.commands
    3.86 +        node_edits foreach {
    3.87 +          case (name, edits) =>
    3.88 +            val node = nodes(name)
    3.89 +            val commands = node.commands
    3.90  
    3.91 -          val node1 =
    3.92 -            if (reparse_set(name) && !commands.isEmpty)
    3.93 -              node.update_commands(
    3.94 -                reparse_spans(resources, syntax, doc_blobs,
    3.95 -                  name, commands, commands.head, commands.last))
    3.96 -            else node
    3.97 -          val node2 = (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
    3.98 +            val node1 =
    3.99 +              if (reparse_set(name) && !commands.isEmpty)
   3.100 +                node.update_commands(
   3.101 +                  reparse_spans(resources, syntax, doc_blobs,
   3.102 +                    name, commands, commands.head, commands.last))
   3.103 +              else node
   3.104 +            val node2 =
   3.105 +              (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
   3.106  
   3.107 -          if (!(node.same_perspective(node2.perspective)))
   3.108 -            doc_edits += (name -> node2.perspective)
   3.109 +            if (!(node.same_perspective(node2.perspective)))
   3.110 +              doc_edits += (name -> node2.perspective)
   3.111  
   3.112 -          doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
   3.113 +            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
   3.114  
   3.115 -          nodes += (name -> node2)
   3.116 +            nodes += (name -> node2)
   3.117 +        }
   3.118 +        (doc_edits.toList, Document.Version.make(syntax, nodes))
   3.119        }
   3.120  
   3.121 -      Session.Change(
   3.122 -        previous,
   3.123 -        doc_blobs,
   3.124 -        syntax_changed,
   3.125 -        doc_edits.toList,
   3.126 -        Document.Version.make(syntax, nodes))
   3.127 -    }
   3.128 +    Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
   3.129    }
   3.130  }
     4.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Mar 29 10:17:09 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Mar 29 10:49:32 2014 +0100
     4.3 @@ -117,7 +117,10 @@
     4.4  
     4.5    /* theory text edits */
     4.6  
     4.7 -  override def syntax_changed(): Unit =
     4.8 -    Swing_Thread.later { jEdit.propertiesChanged() }
     4.9 +  override def commit(change: Session.Change)
    4.10 +  {
    4.11 +    if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
    4.12 +    if (change.deps_changed) PIDE.deps_changed()
    4.13 +  }
    4.14  }
    4.15  
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 29 10:17:09 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 29 10:49:32 2014 +0100
     5.3 @@ -39,6 +39,7 @@
     5.4    @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty))
     5.5  
     5.6    def options_changed() { plugin.options_changed() }
     5.7 +  def deps_changed() { plugin.deps_changed() }
     5.8  
     5.9    def resources(): JEdit_Resources =
    5.10      session.resources.asInstanceOf[JEdit_Resources]
    5.11 @@ -168,13 +169,19 @@
    5.12  
    5.13  class Plugin extends EBPlugin
    5.14  {
    5.15 -  /* options */
    5.16 +  /* global changes */
    5.17  
    5.18 -  def options_changed() {
    5.19 +  def options_changed()
    5.20 +  {
    5.21      PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
    5.22      Swing_Thread.later { delay_load.invoke() }
    5.23    }
    5.24  
    5.25 +  def deps_changed()
    5.26 +  {
    5.27 +    Swing_Thread.later { delay_load.invoke() }
    5.28 +  }
    5.29 +
    5.30  
    5.31    /* theory files */
    5.32