# HG changeset patch
# User wenzelm
# Date 1483705638 -3600
# Node ID 7283f41d05abf5d010dbdd3c030fb89b723c38a9
# Parent  ddbb89e7621d7c522563289513e36dd7d5c3be04
manage buffer models as explicit global state;
tuned signature;

diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/bibtex_jedit.scala
--- 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)
 
diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/document_model.scala
--- 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
 
diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/isabelle.scala
--- 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) =>
diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/isabelle_sidekick.scala
--- 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
       }
diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/jedit_editor.scala
--- 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)
diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/jedit_resources.scala
--- 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()
       }
diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/plugin.scala
--- 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)
 
diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/state_dockable.scala
--- 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 =>
diff -r ddbb89e7621d -r 7283f41d05ab src/Tools/jEdit/src/theories_dockable.scala
--- 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
   }