--- a/src/Tools/jEdit/src/bibtex_jedit.scala Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Fri Jan 06 13:27:18 2017 +0100
@@ -58,7 +58,7 @@
def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
for {
buffer <- JEdit_Lib.jedit_buffers()
- model <- PIDE.document_model(buffer).iterator
+ model <- Document_Model.get(buffer).iterator
(name, offset) <- model.bibtex_entries.iterator
} yield (name, buffer, offset)
--- a/src/Tools/jEdit/src/document_model.scala Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Jan 06 13:27:18 2017 +0100
@@ -21,53 +21,55 @@
object Document_Model
{
+ /* global state */
+
+ sealed case class State(buffer_models: Map[JEditBuffer, Document_Model] = Map.empty)
+
+ private val state = Synchronized(State())
+
+
/* document model of buffer */
- private val key = "PIDE.document_model"
-
- def apply(buffer: Buffer): Option[Document_Model] =
- {
- buffer.getProperty(key) match {
- case model: Document_Model => Some(model)
- case _ => None
- }
- }
+ def get(buffer: JEditBuffer): Option[Document_Model] =
+ state.value.buffer_models.get(buffer)
def exit(buffer: Buffer)
{
GUI_Thread.require {}
- apply(buffer) match {
- case None =>
- case Some(model) =>
- model.deactivate()
- buffer.unsetProperty(key)
- buffer.propertiesChanged
- }
+ state.change(st =>
+ st.buffer_models.get(buffer) match {
+ case None => st
+ case Some(model) =>
+ model.deactivate()
+ buffer.propertiesChanged
+ st.copy(buffer_models = st.buffer_models - buffer)
+ })
}
- def init(session: Session, buffer: Buffer, node_name: Document.Node.Name,
- old_model: Option[Document_Model]): Document_Model =
+ def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
{
GUI_Thread.require {}
-
val model =
- old_model match {
- case Some(old) if old.node_name == node_name => old
- case _ =>
- apply(buffer).map(_.deactivate)
- val model = new Document_Model(session, buffer, node_name)
- buffer.setProperty(key, model)
- model.activate()
- buffer.propertiesChanged
- model
- }
+ state.change_result(st =>
+ {
+ val old_model = st.buffer_models.get(buffer)
+ old_model match {
+ case Some(model) if model.node_name == node_name => (model, st)
+ case _ =>
+ old_model.foreach(_.deactivate)
+ val model = new Document_Model(session, buffer, node_name)
+ model.activate()
+ buffer.propertiesChanged
+ (model, st.copy(st.buffer_models + (buffer -> model)))
+ }
+ })
model.init_token_marker
model
}
}
-
-class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
+class Document_Model private(
+ val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
{
override def toString: String = node_name.toString
--- a/src/Tools/jEdit/src/isabelle.scala Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Jan 06 13:27:18 2017 +0100
@@ -63,7 +63,7 @@
def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
if (buffer == null) None
else
- (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
+ (JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match {
case ("isabelle", Some(model)) =>
Some(PIDE.session.recent_syntax(model.node_name))
case (mode, _) => mode_syntax(mode)
@@ -231,7 +231,7 @@
private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
{
GUI_Thread.require {}
- PIDE.document_model(view.getBuffer) match {
+ Document_Model.get(view.getBuffer) match {
case Some(model) =>
model.node_required = (if (toggle) !model.node_required else set)
case None =>
@@ -329,7 +329,7 @@
{
val buffer = text_area.getBuffer
if (!snapshot.is_outdated && text != "") {
- (snapshot.find_command(id), PIDE.document_model(buffer)) match {
+ (snapshot.find_command(id), Document_Model.get(buffer)) match {
case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
node.command_start(command) match {
case Some(start) =>
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Jan 06 13:27:18 2017 +0100
@@ -178,7 +178,7 @@
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
val opt_snapshot =
- PIDE.document_model(buffer) match {
+ Document_Model.get(buffer) match {
case Some(model) if model.is_theory => Some(model.snapshot)
case _ => None
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Jan 06 13:27:18 2017 +0100
@@ -73,10 +73,10 @@
GUI_Thread.require { jEdit.getActiveView() }
override def current_node(view: View): Option[Document.Node.Name] =
- GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
+ GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
override def current_node_snapshot(view: View): Option[Document.Snapshot] =
- GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
+ GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) }
override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
{
@@ -84,7 +84,7 @@
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
- PIDE.document_model(buffer) match {
+ Document_Model.get(buffer) match {
case Some(model) => model.snapshot
case None => session.snapshot(name)
}
@@ -113,7 +113,7 @@
}
else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
case _ =>
- PIDE.document_model(buffer) match {
+ Document_Model.get(buffer) match {
case Some(model) if !model.is_theory =>
snapshot.version.nodes.commands_loading(model.node_name) match {
case cmd :: _ => Some(cmd)
--- a/src/Tools/jEdit/src/jedit_resources.scala Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Fri Jan 06 13:27:18 2017 +0100
@@ -118,7 +118,7 @@
val changed = change.syntax_changed.toSet
for {
buffer <- JEdit_Lib.jedit_buffers()
- model <- PIDE.document_model(buffer)
+ model <- Document_Model.get(buffer)
if changed(model.node_name)
} model.syntax_changed()
}
--- a/src/Tools/jEdit/src/plugin.scala Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Jan 06 13:27:18 2017 +0100
@@ -63,12 +63,6 @@
/* document model and view */
- def document_model(buffer: JEditBuffer): Option[Document_Model] =
- buffer match {
- case b: Buffer => Document_Model(b)
- case _ => None
- }
-
def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
def document_views(buffer: Buffer): List[Document_View] =
@@ -80,15 +74,15 @@
def document_models(): List[Document_Model] =
for {
buffer <- JEdit_Lib.jedit_buffers().toList
- model <- document_model(buffer)
+ model <- Document_Model.get(buffer)
} yield model
def document_blobs(): Document.Blobs =
Document.Blobs(
(for {
buffer <- JEdit_Lib.jedit_buffers()
- model <- document_model(buffer)
- blob <- model.get_blob()
+ model <- Document_Model.get(buffer)
+ blob <- model.get_blob
} yield (model.node_name -> blob)).toMap)
def exit_models(buffers: List[Buffer])
@@ -115,7 +109,7 @@
if (buffer.isLoaded) {
JEdit_Lib.buffer_lock(buffer) {
val node_name = resources.node_name(buffer)
- val model = Document_Model.init(session, buffer, node_name, document_model(buffer))
+ val model = Document_Model.init(session, buffer, node_name)
for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
if document_view(text_area).map(_.model) != Some(model)
@@ -132,7 +126,7 @@
def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
GUI_Thread.now {
JEdit_Lib.buffer_lock(buffer) {
- document_model(buffer) match {
+ Document_Model.get(buffer) match {
case Some(model) => Document_View.init(model, text_area)
case None =>
}
@@ -151,8 +145,7 @@
def snapshot(view: View): Document.Snapshot = GUI_Thread.now
{
- val buffer = view.getBuffer
- document_model(buffer) match {
+ Document_Model.get(view.getBuffer) match {
case Some(model) => model.snapshot
case None => error("No document model for current buffer")
}
@@ -212,7 +205,7 @@
val thys =
for {
buffer <- buffers
- model <- PIDE.document_model(buffer)
+ model <- Document_Model.get(buffer)
if model.is_theory
} yield (model.node_name, Position.none)
--- a/src/Tools/jEdit/src/state_dockable.scala Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Fri Jan 06 13:27:18 2017 +0100
@@ -64,7 +64,7 @@
{
GUI_Thread.require {}
- PIDE.document_model(view.getBuffer).map(_.snapshot()) match {
+ Document_Model.get(view.getBuffer).map(_.snapshot()) match {
case Some(snapshot) =>
(PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
case (Some(command1), Some(command2)) if command1.id == command2.id =>
--- a/src/Tools/jEdit/src/theories_dockable.scala Fri Jan 06 11:58:29 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Fri Jan 06 13:27:18 2017 +0100
@@ -41,7 +41,7 @@
if (clicks == 1) {
for {
buffer <- JEdit_Lib.jedit_buffer(listData(index))
- model <- PIDE.document_model(buffer)
+ model <- Document_Model.get(buffer)
} model.node_required = !model.node_required
}
}
@@ -97,7 +97,7 @@
nodes_required = Set.empty
for {
buffer <- JEdit_Lib.jedit_buffers
- model <- PIDE.document_model(buffer)
+ model <- Document_Model.get(buffer)
if model.node_required
} nodes_required += model.node_name
}