node-specific syntax, with base_syntax as default;
clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;

--- 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)
     }
 
 

--- 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 + ")"

--- 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]]

--- 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 */

--- 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)
   }
 }

--- 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()
   }
 }

--- 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
   }
 
 

--- 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
         }

--- 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 */
 

--- 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()
   }
 }

--- 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 ||

--- 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))

--- 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 + ")"