# HG changeset patch # User wenzelm # Date 1396086572 -3600 # Node ID b1cf8ddc2e040e17262d3d6164141664f7d5e49b # Parent c20053f670936474386c389ea0672e93ad79ae55 propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save); tuned signature; diff -r c20053f67093 -r b1cf8ddc2e04 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sat Mar 29 10:17:09 2014 +0100 +++ b/src/Pure/PIDE/resources.scala Sat Mar 29 10:49:32 2014 +0100 @@ -91,15 +91,15 @@ with_thy_text(name, check_thy_text(name, _)) - /* theory text edits */ + /* document changes */ - def parse_edits( + def parse_change( reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Session.Change = - Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits) + Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits) - def syntax_changed() { } + def commit(change: Session.Change) { } } diff -r c20053f67093 -r b1cf8ddc2e04 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Mar 29 10:17:09 2014 +0100 +++ b/src/Pure/PIDE/session.scala Sat Mar 29 10:49:32 2014 +0100 @@ -24,6 +24,7 @@ previous: Document.Version, doc_blobs: Document.Blobs, syntax_changed: Boolean, + deps_changed: Boolean, doc_edits: List[Document.Edit_Command], version: Document.Version) @@ -190,8 +191,8 @@ case Text_Edits(previous, doc_blobs, text_edits, version_result) => val prev = previous.get_finished val change = - Timing.timeit("parse_edits", timing) { - resources.parse_edits(reparse_limit, prev, doc_blobs, text_edits) + Timing.timeit("parse_change", timing) { + resources.parse_change(reparse_limit, prev, doc_blobs, text_edits) } version_result.fulfill(change.version) sender ! change @@ -402,8 +403,7 @@ val assignment = global_state().the_assignment(change.previous).check_finished global_state >> (_.define_version(change.version, assignment)) prover.get.update(change.previous.id, change.version.id, change.doc_edits) - - if (change.syntax_changed) resources.syntax_changed() + resources.commit(change) } //}}} diff -r c20053f67093 -r b1cf8ddc2e04 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sat Mar 29 10:17:09 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Sat Mar 29 10:49:32 2014 +0100 @@ -156,7 +156,8 @@ base_syntax: Outer_Syntax, previous: Document.Version, edits: List[Document.Edit_Text]): - ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) = + (Outer_Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes, + List[Document.Edit_Command]) = { var updated_imports = false var updated_keywords = false @@ -178,7 +179,7 @@ case _ => } - val syntax = + val (syntax, syntax_changed) = if (previous.is_init || updated_keywords) { val syntax = (base_syntax /: nodes.entries) { @@ -193,7 +194,7 @@ nodes.descendants(doc_edits.iterator.map(_._1).toList) else Nil - (syntax, reparse, nodes, doc_edits.toList) + (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList) } @@ -431,62 +432,59 @@ } } - def parse_edits( + def parse_change( resources: Resources, reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Session.Change = { - val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) = + val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) = header_edits(resources.base_syntax, previous, edits) - if (edits.isEmpty) - Session.Change(previous, doc_blobs, false, Nil, Document.Version.make(syntax, previous.nodes)) - else { - val reparse = - (reparse0 /: nodes0.entries)({ - case (reparse, (name, node)) => - if (node.load_commands.exists(_.blobs_changed(doc_blobs))) - name :: reparse - else reparse - }) - val reparse_set = reparse.toSet + val (doc_edits, version) = + if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes)) + else { + val reparse = + (reparse0 /: nodes0.entries)({ + case (reparse, (name, node)) => + if (node.load_commands.exists(_.blobs_changed(doc_blobs))) + name :: reparse + else reparse + }) + val reparse_set = reparse.toSet - var nodes = nodes0 - val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 + var nodes = nodes0 + val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 - val node_edits = - (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1) - .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ??? + val node_edits = + (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1) + .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ??? - node_edits foreach { - case (name, edits) => - val node = nodes(name) - val commands = node.commands + node_edits foreach { + case (name, edits) => + val node = nodes(name) + val commands = node.commands - val node1 = - if (reparse_set(name) && !commands.isEmpty) - node.update_commands( - reparse_spans(resources, syntax, doc_blobs, - name, commands, commands.head, commands.last)) - else node - val node2 = (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _)) + val node1 = + if (reparse_set(name) && !commands.isEmpty) + node.update_commands( + reparse_spans(resources, syntax, doc_blobs, + name, commands, commands.head, commands.last)) + else node + val node2 = + (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _)) - if (!(node.same_perspective(node2.perspective))) - doc_edits += (name -> node2.perspective) + if (!(node.same_perspective(node2.perspective))) + doc_edits += (name -> node2.perspective) - doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) + doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) - nodes += (name -> node2) + nodes += (name -> node2) + } + (doc_edits.toList, Document.Version.make(syntax, nodes)) } - Session.Change( - previous, - doc_blobs, - syntax_changed, - doc_edits.toList, - Document.Version.make(syntax, nodes)) - } + Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version) } } diff -r c20053f67093 -r b1cf8ddc2e04 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Sat Mar 29 10:17:09 2014 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Sat Mar 29 10:49:32 2014 +0100 @@ -117,7 +117,10 @@ /* theory text edits */ - override def syntax_changed(): Unit = - Swing_Thread.later { jEdit.propertiesChanged() } + override def commit(change: Session.Change) + { + if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() } + if (change.deps_changed) PIDE.deps_changed() + } } diff -r c20053f67093 -r b1cf8ddc2e04 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sat Mar 29 10:17:09 2014 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Sat Mar 29 10:49:32 2014 +0100 @@ -39,6 +39,7 @@ @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty)) def options_changed() { plugin.options_changed() } + def deps_changed() { plugin.deps_changed() } def resources(): JEdit_Resources = session.resources.asInstanceOf[JEdit_Resources] @@ -168,13 +169,19 @@ class Plugin extends EBPlugin { - /* options */ + /* global changes */ - def options_changed() { + def options_changed() + { PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value)) Swing_Thread.later { delay_load.invoke() } } + def deps_changed() + { + Swing_Thread.later { delay_load.invoke() } + } + /* theory files */