clarified Version.syntax -- avoid guessing initial situation;

--- a/src/Pure/PIDE/document.scala	Thu Apr 03 20:53:35 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Apr 03 21:08:00 2014 +0200
@@ -317,17 +317,15 @@
   {
     val init: Version = new Version()
 
-    def make(syntax: Prover.Syntax, nodes: Nodes): Version =
+    def make(syntax: Option[Prover.Syntax], nodes: Nodes): Version =
       new Version(Document_ID.make(), syntax, nodes)
   }
 
   final class Version private(
     val id: Document_ID.Version = Document_ID.none,
-    val syntax: Prover.Syntax = Prover.Syntax.empty,
+    val syntax: Option[Prover.Syntax] = None,
     val nodes: Nodes = Nodes.empty)
   {
-    def is_init: Boolean = id == Document_ID.none
-
     override def toString: String = "Version(" + id + ")"
   }
 

--- a/src/Pure/PIDE/prover.scala	Thu Apr 03 20:53:35 2014 +0200
+++ b/src/Pure/PIDE/prover.scala	Thu Apr 03 21:08:00 2014 +0200
@@ -11,11 +11,6 @@
 {
   /* syntax */
 
-  object Syntax
-  {
-    val empty: Syntax = Outer_Syntax.empty
-  }
-
   trait Syntax
   {
     def add_keywords(keywords: Thy_Header.Keywords): Syntax

--- a/src/Pure/PIDE/session.scala	Thu Apr 03 20:53:35 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Apr 03 21:08:00 2014 +0200
@@ -225,8 +225,7 @@
   def recent_syntax(): Prover.Syntax =
   {
     val version = current_state().recent_finished.version.get_finished
-    if (version.is_init) resources.base_syntax  // FIXME
-    else version.syntax
+    version.syntax getOrElse resources.base_syntax
   }
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,

--- a/src/Pure/Thy/thy_syntax.scala	Thu Apr 03 20:53:35 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Apr 03 21:08:00 2014 +0200
@@ -153,7 +153,7 @@
   /** header edits: structure and outer syntax **/
 
   private def header_edits(
-    base_syntax: Prover.Syntax,
+    resources: Resources,
     previous: Document.Version,
     edits: List[Document.Edit_Text]):
     (Prover.Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
@@ -180,14 +180,16 @@
     }
 
     val (syntax, syntax_changed) =
-      if (previous.is_init || updated_keywords) {
-        val syntax =
-          (base_syntax /: nodes.iterator) {
-            case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
-          }
-        (syntax, true)
+      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)
       }
-      else (previous.syntax, false)
 
     val reparse =
       if (updated_imports || updated_keywords)
@@ -443,10 +445,10 @@
       doc_blobs.get(name) orElse previous.nodes(name).get_blob
 
     val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
-      header_edits(resources.base_syntax, previous, edits)
+      header_edits(resources, previous, edits)
 
     val (doc_edits, version) =
-      if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
+      if (edits.isEmpty) (Nil, Document.Version.make(Some(syntax), previous.nodes))
       else {
         val reparse =
           (reparse0 /: nodes0.iterator)({
@@ -485,7 +487,7 @@
 
             nodes += (name -> node2)
         }
-        (doc_edits.toList, Document.Version.make(syntax, nodes))
+        (doc_edits.toList, Document.Version.make(Some(syntax), nodes))
       }
 
     Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)

--- a/src/Tools/jEdit/src/isabelle.scala	Thu Apr 03 20:53:35 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Apr 03 21:08:00 2014 +0200
@@ -47,7 +47,7 @@
     name match {
       case "isabelle" | "isabelle-markup" =>
         PIDE.session.recent_syntax match {
-          case syntax : Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
+          case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
           case _ => None
         }
       case "isabelle-options" => Some(Options.options_syntax)