# HG changeset patch # User wenzelm # Date 1417526216 -3600 # Node ID 7e0d3da6e6d8440c8a11af5fc16f342890740709 # Parent 65babcd8b0e62683889e45d45a2790e17030ca20 node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker; diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Tue Dec 02 14:16:56 2014 +0100 @@ -114,12 +114,13 @@ /* merge */ - def ++ (other: Outer_Syntax): Outer_Syntax = + def ++ (other: Prover.Syntax): Prover.Syntax = if (this eq other) this else { - val keywords1 = keywords ++ other.keywords - val completion1 = completion ++ other.completion - new Outer_Syntax(keywords1, completion1, language_context, has_tokens) + val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords + val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion + if ((keywords eq keywords1) && (completion eq completion1)) this + else new Outer_Syntax(keywords1, completion1, language_context, has_tokens) } diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Pure/PIDE/document.scala Tue Dec 02 14:16:56 2014 +0100 @@ -244,6 +244,7 @@ final class Node private( val get_blob: Option[Document.Blob] = None, val header: Node.Header = Node.no_header, + val syntax: Option[Prover.Syntax] = None, val perspective: Node.Perspective_Command = Node.no_perspective_command, _commands: Node.Commands = Node.Commands.empty) { @@ -256,15 +257,18 @@ def commands: Linear_Set[Command] = _commands.commands def load_commands: List[Command] = _commands.load_commands - def clear: Node = new Node(header = header) + def clear: Node = new Node(header = header, syntax = syntax) - def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged)) + def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged)) def update_header(new_header: Node.Header): Node = - new Node(get_blob, new_header, perspective, _commands) + new Node(get_blob, new_header, syntax, perspective, _commands) + + def update_syntax(new_syntax: Option[Prover.Syntax]): Node = + new Node(get_blob, header, new_syntax, perspective, _commands) def update_perspective(new_perspective: Node.Perspective_Command): Node = - new Node(get_blob, header, new_perspective, _commands) + new Node(get_blob, header, syntax, new_perspective, _commands) def same_perspective(other_perspective: Node.Perspective_Command): Boolean = perspective.required == other_perspective.required && @@ -273,7 +277,7 @@ def update_commands(new_commands: Linear_Set[Command]): Node = if (new_commands eq _commands.commands) this - else new Node(get_blob, header, perspective, Node.Commands(new_commands)) + else new Node(get_blob, header, syntax, perspective, Node.Commands(new_commands)) def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = _commands.iterator(i) @@ -344,14 +348,11 @@ object Version { val init: Version = new Version() - - def make(syntax: Option[Prover.Syntax], nodes: Nodes): Version = - new Version(Document_ID.make(), syntax, nodes) + def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes) } final class Version private( val id: Document_ID.Version = Document_ID.none, - val syntax: Option[Prover.Syntax] = None, val nodes: Nodes = Nodes.empty) { override def toString: String = "Version(" + id + ")" diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Pure/PIDE/prover.scala Tue Dec 02 14:16:56 2014 +0100 @@ -17,6 +17,7 @@ trait Syntax { + def ++ (other: Syntax): Syntax def add_keywords(keywords: Thy_Header.Keywords): Syntax def parse_spans(input: CharSequence): List[Command_Span.Span] def load_command(name: String): Option[List[String]] diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Pure/PIDE/session.scala Tue Dec 02 14:16:56 2014 +0100 @@ -47,7 +47,7 @@ sealed case class Change( previous: Document.Version, - syntax_changed: Boolean, + syntax_changed: List[Document.Node.Name], deps_changed: Boolean, doc_edits: List[Document.Edit_Command], version: Document.Version) @@ -231,11 +231,9 @@ private val global_state = Synchronized(Document.State.init) def current_state(): Document.State = global_state.value - def recent_syntax(): Prover.Syntax = - { - val version = current_state().recent_finished.version.get_finished - version.syntax getOrElse resources.base_syntax - } + def recent_syntax(name: Document.Node.Name): Prover.Syntax = + current_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse + resources.base_syntax /* protocol handlers */ diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Tue Dec 02 14:16:56 2014 +0100 @@ -69,11 +69,9 @@ resources: Resources, previous: Document.Version, edits: List[Document.Edit_Text]): - (Prover.Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes, - List[Document.Edit_Command]) = + (List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) = { - var updated_imports = false - var updated_keywords = false + val syntax_changed0 = new mutable.ListBuffer[Document.Node.Name] var nodes = previous.nodes val doc_edits = new mutable.ListBuffer[Document.Edit_Command] @@ -84,32 +82,28 @@ !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header if (update_header) { val node1 = node.update_header(header) - updated_imports = updated_imports || (node.header.imports != node1.header.imports) - updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords) + if (node.header.imports != node1.header.imports || + node.header.keywords != node1.header.keywords) syntax_changed0 += name nodes += (name -> node1) doc_edits += (name -> Document.Node.Deps(header)) } case _ => } - val (syntax, syntax_changed) = - previous.syntax match { - case Some(syntax) if !updated_keywords => - (syntax, false) - case _ => - val syntax = - (resources.base_syntax /: nodes.iterator) { - case (syn, (_, node)) => syn.add_keywords(node.header.keywords) - } - (syntax, true) - } + val syntax_changed = nodes.descendants(syntax_changed0.toList) - val reparse = - if (updated_imports || updated_keywords) - nodes.descendants(doc_edits.iterator.map(_._1).toList) - else Nil + for (name <- syntax_changed) { + val node = nodes(name) + val syntax = + if (node.is_empty) None + else { + val imports_syntax = node.header.imports.flatMap(a => nodes(a).syntax) + Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(node.header.keywords)) + } + nodes += (name -> node.update_syntax(syntax)) + } - (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList) + (syntax_changed, nodes, doc_edits.toList) } @@ -311,14 +305,13 @@ def get_blob(name: Document.Node.Name) = doc_blobs.get(name) orElse previous.nodes(name).get_blob - val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) = - header_edits(resources, previous, edits) + val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits) val (doc_edits, version) = - if (edits.isEmpty) (Nil, Document.Version.make(Some(syntax), previous.nodes)) + if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes)) else { val reparse = - (reparse0 /: nodes0.iterator)({ + (syntax_changed /: nodes0.iterator)({ case (reparse, (name, node)) => if (node.load_commands.exists(_.blobs_changed(doc_blobs))) name :: reparse @@ -336,6 +329,7 @@ node_edits foreach { case (name, edits) => val node = nodes(name) + val syntax = node.syntax getOrElse resources.base_syntax val commands = node.commands val node1 = @@ -354,9 +348,9 @@ nodes += (name -> node2) } - (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes)) + (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes)) } - Session.Change(previous, syntax_changed, deps_changed, doc_edits, version) + Session.Change(previous, syntax_changed, !syntax_changed.isEmpty, doc_edits, version) } } diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Dec 02 14:16:56 2014 +0100 @@ -13,6 +13,7 @@ import scala.collection.mutable +import org.gjt.sp.jedit.jEdit import org.gjt.sp.jedit.Buffer import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} @@ -44,15 +45,23 @@ } } - def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model = + def init(session: Session, buffer: Buffer, node_name: Document.Node.Name, + old_model: Option[Document_Model]): Document_Model = { GUI_Thread.require {} - apply(buffer).map(_.deactivate) - val model = new Document_Model(session, buffer, node_name) - buffer.setProperty(key, model) - model.activate() - buffer.propertiesChanged - model + + old_model match { + case Some(old) + if old.node_name == node_name && Isabelle.buffer_token_marker(buffer).isEmpty => old + + case _ => + apply(buffer).map(_.deactivate) + val model = new Document_Model(session, buffer, node_name) + buffer.setProperty(key, model) + model.activate() + buffer.propertiesChanged + model + } } } @@ -277,18 +286,26 @@ /* activation */ + private def refresh_token_marker() + { + Isabelle.buffer_token_marker(buffer) match { + case Some(marker) if marker != buffer.getTokenMarker => + buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker) + buffer.setTokenMarker(marker) + case _ => + } + } + private def activate() { pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))) buffer.addBufferListener(buffer_listener) - Isabelle.buffer_token_marker(buffer).foreach(marker => - JEdit_Lib.update_token_marker(buffer, marker)) + refresh_token_marker() } private def deactivate() { buffer.removeBufferListener(buffer_listener) - Isabelle.mode_token_marker(JEdit_Lib.buffer_mode(buffer)).foreach(marker => - JEdit_Lib.update_token_marker(buffer, marker)) + refresh_token_marker() } } diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Dec 02 14:16:56 2014 +0100 @@ -47,18 +47,9 @@ private lazy val news_syntax: Outer_Syntax = Outer_Syntax.init().no_tokens - private lazy val bootstrap_syntax: Outer_Syntax = - Thy_Header.bootstrap_syntax() - - def session_syntax(): Option[Outer_Syntax] = - PIDE.session.recent_syntax match { - case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax) - case _ => None - } - def mode_syntax(mode: String): Option[Outer_Syntax] = mode match { - case "isabelle" => Some(bootstrap_syntax) + case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax]) case "isabelle-options" => Some(Options.options_syntax) case "isabelle-root" => Some(Build.root_syntax) case "isabelle-ml" => Some(ml_syntax) @@ -69,9 +60,10 @@ } def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] = - JEdit_Lib.buffer_mode(buffer) match { - case "isabelle" => session_syntax() - case mode => mode_syntax(mode) + (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match { + case ("isabelle", Some(model)) => + Some(PIDE.session.recent_syntax(model.node_name).asInstanceOf[Outer_Syntax]) + case (mode, _) => mode_syntax(mode) } @@ -86,8 +78,10 @@ def buffer_token_marker(buffer: Buffer): Option[TokenMarker] = { val mode = JEdit_Lib.buffer_mode(buffer) - if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer))) - else mode_token_marker(mode) + val new_token_marker = + if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer))) + else mode_token_marker(mode) + if (new_token_marker == Some(buffer.getTokenMarker)) None else new_token_marker } diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Dec 02 14:16:56 2014 +0100 @@ -153,7 +153,7 @@ { val opt_snapshot = GUI_Thread.now { - Document_Model(buffer) match { + PIDE.document_model(buffer) match { case Some(model) if model.is_theory => Some(model.snapshot) case _ => None } diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Dec 02 14:16:56 2014 +0100 @@ -114,12 +114,6 @@ def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath - def update_token_marker(buffer: JEditBuffer, marker: TokenMarker) - { - buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker) - buffer.setTokenMarker(marker) - } - /* main jEdit components */ diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Dec 02 14:16:56 2014 +0100 @@ -114,7 +114,7 @@ override def commit(change: Session.Change) { - if (change.syntax_changed) GUI_Thread.later { jEdit.propertiesChanged() } + if (!change.syntax_changed.isEmpty) GUI_Thread.later { jEdit.propertiesChanged() } if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed() } } diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Tue Dec 02 14:16:56 2014 +0100 @@ -17,6 +17,7 @@ import org.jedit.options.CombinedOptions import org.gjt.sp.jedit.gui.AboutDialog import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} +import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.syntax.ModeProvider import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} @@ -64,7 +65,11 @@ /* document model and view */ - def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer) + def document_model(buffer: JEditBuffer): Option[Document_Model] = + buffer match { + case b: Buffer => Document_Model(b) + case _ => None + } def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area) @@ -111,11 +116,7 @@ } { JEdit_Lib.buffer_lock(buffer) { val node_name = resources.node_name(buffer) - val model = - document_model(buffer) match { - case Some(model) if model.node_name == node_name => model - case _ => Document_Model.init(session, buffer, node_name) - } + val model = Document_Model.init(session, buffer, node_name, document_model(buffer)) for { text_area <- JEdit_Lib.jedit_text_areas(buffer) if document_view(text_area).map(_.model) != Some(model) @@ -315,7 +316,6 @@ "It is for testing only, not for production use.") } - case msg: BufferUpdate if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Dec 02 14:16:56 2014 +0100 @@ -43,7 +43,7 @@ val nodes0 = version0.nodes val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) - val version1 = Document.Version.make(version0.syntax, nodes1) + val version1 = Document.Version.make(nodes1) val state1 = state0.continue_history(Future.value(version0), edits, Future.value(version1)) .define_version(version1, state0.the_assignment(version0)) diff -r 65babcd8b0e6 -r 7e0d3da6e6d8 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Mon Dec 01 19:25:20 2014 +0100 +++ b/src/Tools/jEdit/src/token_markup.scala Tue Dec 02 14:16:56 2014 +0100 @@ -308,8 +308,17 @@ /* token marker */ - class Marker(mode: String, opt_buffer: Option[Buffer]) extends TokenMarker + class Marker( + protected val mode: String, + protected val opt_buffer: Option[Buffer]) extends TokenMarker { + override def hashCode: Int = (mode, opt_buffer).hashCode + override def equals(that: Any): Boolean = + that match { + case other: Marker => mode == other.mode && opt_buffer == other.opt_buffer + case _ => false + } + override def toString: String = opt_buffer match { case None => "Marker(" + mode + ")"