maintain Version.syntax within document state;
clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;

--- a/src/Pure/Isar/outer_syntax.scala	Thu Mar 15 10:16:21 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Mar 15 11:37:56 2012 +0100
@@ -35,13 +35,15 @@
   }
 
   type Decl = (String, Option[(String, List[String])])
-  def init(): Outer_Syntax = new Outer_Syntax()
+
+  val empty: Outer_Syntax = new Outer_Syntax()
+  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
 }
 
 final class Outer_Syntax private(
   keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
   lexicon: Scan.Lexicon = Scan.Lexicon.empty,
-  val completion: Completion = Completion.init())
+  val completion: Completion = Completion.empty)
 {
   def keyword_kind(name: String): Option[String] = keywords.get(name)
 

--- a/src/Pure/PIDE/document.scala	Thu Mar 15 10:16:21 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Mar 15 11:37:56 2012 +0100
@@ -212,12 +212,17 @@
   {
     val init: Version = new Version()
 
-    def make(nodes: Nodes): Version = new Version(new_id(), nodes)
+    def make(syntax: Outer_Syntax, nodes: Nodes): Version =
+      new Version(new_id(), syntax, nodes)
   }
 
   final class Version private(
     val id: Version_ID = no_id,
+    val syntax: Outer_Syntax = Outer_Syntax.empty,
     val nodes: Nodes = Nodes.empty)
+  {
+    def is_init: Boolean = id == no_id
+  }
 
 
   /* changes of plain text, eventually resulting in document edits */

--- a/src/Pure/System/session.scala	Thu Mar 15 10:16:21 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Mar 15 11:37:56 2012 +0100
@@ -86,7 +86,6 @@
 
   //{{{
   private case class Text_Edits(
-    syntax: Outer_Syntax,
     name: Document.Node.Name,
     previous: Future[Document.Version],
     text_edits: List[Document.Edit_Text],
@@ -99,8 +98,9 @@
       receive {
         case Stop => finished = true; reply(())
 
-        case Text_Edits(syntax, name, previous, text_edits, version_result) =>
+        case Text_Edits(name, previous, text_edits, version_result) =>
           val prev = previous.get_finished
+          val syntax = if (prev.is_init) prover_syntax else prev.syntax
           val (doc_edits, version) = Thy_Syntax.text_edits(syntax, prev, text_edits)
           version_result.fulfill(version)
           sender ! Change_Node(name, doc_edits, prev, version)
@@ -118,8 +118,11 @@
 
   @volatile var verbose: Boolean = false
 
-  @volatile private var syntax = Outer_Syntax.init()
-  def current_syntax(): Outer_Syntax = syntax
+  @volatile private var prover_syntax =
+    Outer_Syntax.init() +
+      // FIXME avoid hardwired stuff!?
+      ("hence", Keyword.PRF_ASM_GOAL, "then have") +
+      ("thus", Keyword.PRF_ASM_GOAL, "then show")
 
   private val syslog = Volatile(Queue.empty[XML.Elem])
   def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
@@ -135,6 +138,7 @@
 
   private val global_state = Volatile(Document.State.init)
   def current_state(): Document.State = global_state()
+  def recent_syntax(): Outer_Syntax = current_state().recent_stable.version.get_finished.syntax
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
@@ -279,7 +283,6 @@
         header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
     //{{{
     {
-      val syntax = current_syntax()
       val previous = global_state().history.tip.version
 
       prover.get.cancel_execution()
@@ -288,7 +291,7 @@
       val version = Future.promise[Document.Version]
       val change = global_state >>> (_.continue_history(previous, text_edits, version))
 
-      change_parser ! Text_Edits(syntax, name, previous, text_edits, version)
+      change_parser ! Text_Edits(name, previous, text_edits, version)
     }
     //}}}
 
@@ -398,19 +401,16 @@
           System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
 
         case Isabelle_Markup.Ready if output.is_protocol =>
-            // FIXME move to ML side (!?)
-            syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
-            syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
             phase = Session.Ready
 
         case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
           thy_load.register_thy(name)
 
         case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol =>
-          syntax += (name, kind)
+          prover_syntax += (name, kind)
 
         case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
-          syntax += name
+          prover_syntax += name
 
         case _ =>
           if (output.is_exit && phase == Session.Startup) phase = Session.Failed

--- a/src/Pure/Thy/thy_syntax.scala	Thu Mar 15 10:16:21 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 15 11:37:56 2012 +0100
@@ -136,7 +136,7 @@
   {
     val nodes = previous.nodes
     val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
-    val version = Document.Version.make(new_nodes getOrElse nodes)
+    val version = Document.Version.make(previous.syntax, new_nodes getOrElse nodes)
     (perspective, version)
   }
 
@@ -265,7 +265,7 @@
               nodes = nodes1
           }
       }
-      (doc_edits.toList, Document.Version.make(nodes))
+      (doc_edits.toList, Document.Version.make(syntax, nodes))
     }
   }
 }

--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 15 10:16:21 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 15 11:37:56 2012 +0100
@@ -92,7 +92,7 @@
           val start = buffer.getLineStartOffset(line)
           val text = buffer.getSegment(start, caret - start)
 
-          val completion = model.session.current_syntax().completion
+          val completion = model.session.recent_syntax().completion
           completion.complete(text) match {
             case None => null
             case Some((word, cs)) =>
@@ -116,7 +116,7 @@
 
   def parser(data: SideKickParsedData, model: Document_Model)
   {
-    val syntax = model.session.current_syntax()
+    val syntax = model.session.recent_syntax()
 
     def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
       entry match {

--- a/src/Tools/jEdit/src/token_markup.scala	Thu Mar 15 10:16:21 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Mar 15 11:37:56 2012 +0100
@@ -178,7 +178,7 @@
       {
         val (styled_tokens, context1) =
           if (line_ctxt.isDefined && Isabelle.session.is_ready) {
-            val syntax = Isabelle.session.current_syntax()
+            val syntax = Isabelle.session.recent_syntax()
             val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
             val styled_tokens =
               tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))