# HG changeset patch
# User wenzelm
# Date 1331818782 -3600
# Node ID 9fc22eb6408c455a102c6cfe2260bb8aaa5bcc0e
# Parent  ac1c41ea856d4a8458e2ade5ec67651dc6ff6100
more recent recent_syntax, e.g. relevant for document rendering during startup;

diff -r ac1c41ea856d -r 9fc22eb6408c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Mar 15 14:22:54 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Mar 15 14:39:42 2012 +0100
@@ -419,6 +419,7 @@
     def is_stable(change: Change): Boolean =
       change.is_finished && is_assigned(change.version.get_finished)
 
+    def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail
     def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
     def tip_stable: Boolean = is_stable(history.tip)
     def tip_version: Version = history.tip.version.get_finished
diff -r ac1c41ea856d -r 9fc22eb6408c src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Mar 15 14:22:54 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Mar 15 14:39:42 2012 +0100
@@ -137,7 +137,13 @@
 
   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 recent_syntax(): Outer_Syntax =
+  {
+    val version = current_state().recent_finished.version.get_finished
+    if (version.is_init) prover_syntax
+    else version.syntax
+  }
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =