propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;

--- a/src/Pure/System/session.scala	Sat Jan 25 13:55:09 2014 +0100
+++ b/src/Pure/System/session.scala	Sat Jan 25 15:29:40 2014 +0100
@@ -180,12 +180,12 @@
 
         case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
           val prev = previous.get_finished
-          val (doc_edits, version) =
+          val (syntax_changed, doc_edits, version) =
             Timing.timeit("Thy_Load.text_edits", timing) {
               thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
             }
           version_result.fulfill(version)
-          sender ! Change(doc_blobs, doc_edits, prev, version)
+          sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
 
         case bad => System.err.println("change_parser: ignoring bad message " + bad)
       }
@@ -252,6 +252,7 @@
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Change(
     doc_blobs: Document.Blobs,
+    syntax_changed: Boolean,
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
     version: Document.Version)
@@ -370,9 +371,7 @@
     def handle_change(change: Change)
     //{{{
     {
-      val previous = change.previous
-      val version = change.version
-      val doc_edits = change.doc_edits
+      val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
 
       def id_command(command: Command)
       {
@@ -380,7 +379,7 @@
           digest <- command.blobs_digests
           if !global_state().defined_blob(digest)
         } {
-          change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
+          doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
             case Some(blob) =>
               global_state >> (_.define_blob(digest))
               prover.get.define_blob(blob)
@@ -401,6 +400,8 @@
       val assignment = global_state().the_assignment(previous).check_finished
       global_state >> (_.define_version(version, assignment))
       prover.get.update(previous.id, version.id, doc_edits)
+
+      if (syntax_changed) thy_load.syntax_changed()
     }
     //}}}
 

--- a/src/Pure/Thy/thy_load.scala	Sat Jan 25 13:55:09 2014 +0100
+++ b/src/Pure/Thy/thy_load.scala	Sat Jan 25 15:29:40 2014 +0100
@@ -103,7 +103,9 @@
     reparse_limit: Int,
     previous: Document.Version,
     doc_blobs: Document.Blobs,
-    edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
+    edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
     Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
+
+  def syntax_changed() { }
 }
 

--- a/src/Pure/Thy/thy_syntax.scala	Sat Jan 25 13:55:09 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Jan 25 15:29:40 2014 +0100
@@ -155,8 +155,8 @@
   private def header_edits(
     base_syntax: Outer_Syntax,
     previous: Document.Version,
-    edits: List[Document.Edit_Text])
-    : (Outer_Syntax, List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
+    edits: List[Document.Edit_Text]):
+    ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
   {
     var updated_imports = false
     var updated_keywords = false
@@ -179,11 +179,14 @@
     }
 
     val syntax =
-      if (previous.is_init || updated_keywords)
-        (base_syntax /: nodes.entries) {
-          case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
-        }
-      else previous.syntax
+      if (previous.is_init || updated_keywords) {
+        val syntax =
+          (base_syntax /: nodes.entries) {
+            case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
+          }
+        (syntax, true)
+      }
+      else (previous.syntax, false)
 
     val reparse =
       if (updated_imports || updated_keywords)
@@ -428,13 +431,13 @@
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text])
-    : (List[Document.Edit_Command], Document.Version) =
+    : (Boolean, List[Document.Edit_Command], Document.Version) =
   {
-    val (syntax, reparse0, nodes0, doc_edits0) =
+    val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
       header_edits(thy_load.base_syntax, previous, edits)
 
     if (edits.isEmpty)
-      (Nil, Document.Version.make(syntax, previous.nodes))
+      (false, Nil, Document.Version.make(syntax, previous.nodes))
     else {
       val reparse =
         (reparse0 /: nodes0.entries)({
@@ -472,7 +475,7 @@
           nodes += (name -> node2)
       }
 
-      (doc_edits.toList, Document.Version.make(syntax, nodes))
+      (syntax_changed, doc_edits.toList, Document.Version.make(syntax, nodes))
     }
   }
 }

--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Sat Jan 25 13:55:09 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Sat Jan 25 15:29:40 2014 +0100
@@ -14,7 +14,7 @@
 
 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
 import org.gjt.sp.jedit.MiscUtilities
-import org.gjt.sp.jedit.{View, Buffer}
+import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
@@ -111,5 +111,11 @@
       }
     content()
   }
+
+
+  /* theory text edits */
+
+  override def syntax_changed(): Unit =
+    Swing_Thread.later { jEdit.propertiesChanged() }
 }