equal
deleted
inserted
replaced
45 |
45 |
46 /* change */ |
46 /* change */ |
47 |
47 |
48 sealed case class Change( |
48 sealed case class Change( |
49 previous: Document.Version, |
49 previous: Document.Version, |
50 syntax_changed: Boolean, |
50 syntax_changed: List[Document.Node.Name], |
51 deps_changed: Boolean, |
51 deps_changed: Boolean, |
52 doc_edits: List[Document.Edit_Command], |
52 doc_edits: List[Document.Edit_Command], |
53 version: Document.Version) |
53 version: Document.Version) |
54 |
54 |
55 case object Change_Flush |
55 case object Change_Flush |
229 def is_ready: Boolean = phase == Session.Ready |
229 def is_ready: Boolean = phase == Session.Ready |
230 |
230 |
231 private val global_state = Synchronized(Document.State.init) |
231 private val global_state = Synchronized(Document.State.init) |
232 def current_state(): Document.State = global_state.value |
232 def current_state(): Document.State = global_state.value |
233 |
233 |
234 def recent_syntax(): Prover.Syntax = |
234 def recent_syntax(name: Document.Node.Name): Prover.Syntax = |
235 { |
235 current_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse |
236 val version = current_state().recent_finished.version.get_finished |
236 resources.base_syntax |
237 version.syntax getOrElse resources.base_syntax |
|
238 } |
|
239 |
237 |
240 |
238 |
241 /* protocol handlers */ |
239 /* protocol handlers */ |
242 |
240 |
243 @volatile private var _protocol_handlers = new Session.Protocol_Handlers() |
241 @volatile private var _protocol_handlers = new Session.Protocol_Handlers() |