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