manage buffer models as explicit global state;
authorwenzelm
Fri Jan 06 13:27:18 2017 +0100 (2017-01-06 ago)
changeset 648137283f41d05ab
parent 64812 ddbb89e7621d
child 64814 c7693244672e
manage buffer models as explicit global state;
tuned signature;
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/state_dockable.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Fri Jan 06 11:58:29 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Fri Jan 06 13:27:18 2017 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4    def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
     1.5      for {
     1.6        buffer <- JEdit_Lib.jedit_buffers()
     1.7 -      model <- PIDE.document_model(buffer).iterator
     1.8 +      model <- Document_Model.get(buffer).iterator
     1.9        (name, offset) <- model.bibtex_entries.iterator
    1.10      } yield (name, buffer, offset)
    1.11  
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Jan 06 11:58:29 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Jan 06 13:27:18 2017 +0100
     2.3 @@ -21,53 +21,55 @@
     2.4  
     2.5  object Document_Model
     2.6  {
     2.7 +  /* global state */
     2.8 +
     2.9 +  sealed case class State(buffer_models: Map[JEditBuffer, Document_Model] = Map.empty)
    2.10 +
    2.11 +  private val state = Synchronized(State())
    2.12 +
    2.13 +
    2.14    /* document model of buffer */
    2.15  
    2.16 -  private val key = "PIDE.document_model"
    2.17 -
    2.18 -  def apply(buffer: Buffer): Option[Document_Model] =
    2.19 -  {
    2.20 -    buffer.getProperty(key) match {
    2.21 -      case model: Document_Model => Some(model)
    2.22 -      case _ => None
    2.23 -    }
    2.24 -  }
    2.25 +  def get(buffer: JEditBuffer): Option[Document_Model] =
    2.26 +    state.value.buffer_models.get(buffer)
    2.27  
    2.28    def exit(buffer: Buffer)
    2.29    {
    2.30      GUI_Thread.require {}
    2.31 -    apply(buffer) match {
    2.32 -      case None =>
    2.33 -      case Some(model) =>
    2.34 -        model.deactivate()
    2.35 -        buffer.unsetProperty(key)
    2.36 -        buffer.propertiesChanged
    2.37 -    }
    2.38 +    state.change(st =>
    2.39 +      st.buffer_models.get(buffer) match {
    2.40 +        case None => st
    2.41 +        case Some(model) =>
    2.42 +          model.deactivate()
    2.43 +          buffer.propertiesChanged
    2.44 +          st.copy(buffer_models = st.buffer_models - buffer)
    2.45 +      })
    2.46    }
    2.47  
    2.48 -  def init(session: Session, buffer: Buffer, node_name: Document.Node.Name,
    2.49 -    old_model: Option[Document_Model]): Document_Model =
    2.50 +  def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
    2.51    {
    2.52      GUI_Thread.require {}
    2.53 -
    2.54      val model =
    2.55 -      old_model match {
    2.56 -        case Some(old) if old.node_name == node_name => old
    2.57 -        case _ =>
    2.58 -          apply(buffer).map(_.deactivate)
    2.59 -          val model = new Document_Model(session, buffer, node_name)
    2.60 -          buffer.setProperty(key, model)
    2.61 -          model.activate()
    2.62 -          buffer.propertiesChanged
    2.63 -          model
    2.64 -      }
    2.65 +      state.change_result(st =>
    2.66 +        {
    2.67 +          val old_model = st.buffer_models.get(buffer)
    2.68 +          old_model match {
    2.69 +            case Some(model) if model.node_name == node_name => (model, st)
    2.70 +            case _ =>
    2.71 +              old_model.foreach(_.deactivate)
    2.72 +              val model = new Document_Model(session, buffer, node_name)
    2.73 +              model.activate()
    2.74 +              buffer.propertiesChanged
    2.75 +              (model, st.copy(st.buffer_models + (buffer -> model)))
    2.76 +          }
    2.77 +        })
    2.78      model.init_token_marker
    2.79      model
    2.80    }
    2.81  }
    2.82  
    2.83 -
    2.84 -class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
    2.85 +class Document_Model private(
    2.86 +  val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
    2.87  {
    2.88    override def toString: String = node_name.toString
    2.89  
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Jan 06 11:58:29 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Fri Jan 06 13:27:18 2017 +0100
     3.3 @@ -63,7 +63,7 @@
     3.4    def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
     3.5      if (buffer == null) None
     3.6      else
     3.7 -      (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
     3.8 +      (JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match {
     3.9          case ("isabelle", Some(model)) =>
    3.10            Some(PIDE.session.recent_syntax(model.node_name))
    3.11          case (mode, _) => mode_syntax(mode)
    3.12 @@ -231,7 +231,7 @@
    3.13    private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
    3.14    {
    3.15      GUI_Thread.require {}
    3.16 -    PIDE.document_model(view.getBuffer) match {
    3.17 +    Document_Model.get(view.getBuffer) match {
    3.18        case Some(model) =>
    3.19          model.node_required = (if (toggle) !model.node_required else set)
    3.20        case None =>
    3.21 @@ -329,7 +329,7 @@
    3.22    {
    3.23      val buffer = text_area.getBuffer
    3.24      if (!snapshot.is_outdated && text != "") {
    3.25 -      (snapshot.find_command(id), PIDE.document_model(buffer)) match {
    3.26 +      (snapshot.find_command(id), Document_Model.get(buffer)) match {
    3.27          case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
    3.28            node.command_start(command) match {
    3.29              case Some(start) =>
     4.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Jan 06 11:58:29 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Jan 06 13:27:18 2017 +0100
     4.3 @@ -178,7 +178,7 @@
     4.4    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
     4.5    {
     4.6      val opt_snapshot =
     4.7 -      PIDE.document_model(buffer) match {
     4.8 +      Document_Model.get(buffer) match {
     4.9          case Some(model) if model.is_theory => Some(model.snapshot)
    4.10          case _ => None
    4.11        }
     5.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Jan 06 11:58:29 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Jan 06 13:27:18 2017 +0100
     5.3 @@ -73,10 +73,10 @@
     5.4      GUI_Thread.require { jEdit.getActiveView() }
     5.5  
     5.6    override def current_node(view: View): Option[Document.Node.Name] =
     5.7 -    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
     5.8 +    GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
     5.9  
    5.10    override def current_node_snapshot(view: View): Option[Document.Snapshot] =
    5.11 -    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    5.12 +    GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) }
    5.13  
    5.14    override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    5.15    {
    5.16 @@ -84,7 +84,7 @@
    5.17  
    5.18      JEdit_Lib.jedit_buffer(name) match {
    5.19        case Some(buffer) =>
    5.20 -        PIDE.document_model(buffer) match {
    5.21 +        Document_Model.get(buffer) match {
    5.22            case Some(model) => model.snapshot
    5.23            case None => session.snapshot(name)
    5.24          }
    5.25 @@ -113,7 +113,7 @@
    5.26          }
    5.27          else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    5.28        case _ =>
    5.29 -        PIDE.document_model(buffer) match {
    5.30 +        Document_Model.get(buffer) match {
    5.31            case Some(model) if !model.is_theory =>
    5.32              snapshot.version.nodes.commands_loading(model.node_name) match {
    5.33                case cmd :: _ => Some(cmd)
     6.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Fri Jan 06 11:58:29 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Jan 06 13:27:18 2017 +0100
     6.3 @@ -118,7 +118,7 @@
     6.4          val changed = change.syntax_changed.toSet
     6.5          for {
     6.6            buffer <- JEdit_Lib.jedit_buffers()
     6.7 -          model <- PIDE.document_model(buffer)
     6.8 +          model <- Document_Model.get(buffer)
     6.9            if changed(model.node_name)
    6.10          } model.syntax_changed()
    6.11        }
     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Jan 06 11:58:29 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Jan 06 13:27:18 2017 +0100
     7.3 @@ -63,12 +63,6 @@
     7.4  
     7.5    /* document model and view */
     7.6  
     7.7 -  def document_model(buffer: JEditBuffer): Option[Document_Model] =
     7.8 -    buffer match {
     7.9 -      case b: Buffer => Document_Model(b)
    7.10 -      case _ => None
    7.11 -    }
    7.12 -
    7.13    def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
    7.14  
    7.15    def document_views(buffer: Buffer): List[Document_View] =
    7.16 @@ -80,15 +74,15 @@
    7.17    def document_models(): List[Document_Model] =
    7.18      for {
    7.19        buffer <- JEdit_Lib.jedit_buffers().toList
    7.20 -      model <- document_model(buffer)
    7.21 +      model <- Document_Model.get(buffer)
    7.22      } yield model
    7.23  
    7.24    def document_blobs(): Document.Blobs =
    7.25      Document.Blobs(
    7.26        (for {
    7.27          buffer <- JEdit_Lib.jedit_buffers()
    7.28 -        model <- document_model(buffer)
    7.29 -        blob <- model.get_blob()
    7.30 +        model <- Document_Model.get(buffer)
    7.31 +        blob <- model.get_blob
    7.32        } yield (model.node_name -> blob)).toMap)
    7.33  
    7.34    def exit_models(buffers: List[Buffer])
    7.35 @@ -115,7 +109,7 @@
    7.36          if (buffer.isLoaded) {
    7.37            JEdit_Lib.buffer_lock(buffer) {
    7.38              val node_name = resources.node_name(buffer)
    7.39 -            val model = Document_Model.init(session, buffer, node_name, document_model(buffer))
    7.40 +            val model = Document_Model.init(session, buffer, node_name)
    7.41              for {
    7.42                text_area <- JEdit_Lib.jedit_text_areas(buffer)
    7.43                if document_view(text_area).map(_.model) != Some(model)
    7.44 @@ -132,7 +126,7 @@
    7.45    def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
    7.46      GUI_Thread.now {
    7.47        JEdit_Lib.buffer_lock(buffer) {
    7.48 -        document_model(buffer) match {
    7.49 +        Document_Model.get(buffer) match {
    7.50            case Some(model) => Document_View.init(model, text_area)
    7.51            case None =>
    7.52          }
    7.53 @@ -151,8 +145,7 @@
    7.54  
    7.55    def snapshot(view: View): Document.Snapshot = GUI_Thread.now
    7.56    {
    7.57 -    val buffer = view.getBuffer
    7.58 -    document_model(buffer) match {
    7.59 +    Document_Model.get(view.getBuffer) match {
    7.60        case Some(model) => model.snapshot
    7.61        case None => error("No document model for current buffer")
    7.62      }
    7.63 @@ -212,7 +205,7 @@
    7.64            val thys =
    7.65              for {
    7.66                buffer <- buffers
    7.67 -              model <- PIDE.document_model(buffer)
    7.68 +              model <- Document_Model.get(buffer)
    7.69                if model.is_theory
    7.70              } yield (model.node_name, Position.none)
    7.71  
     8.1 --- a/src/Tools/jEdit/src/state_dockable.scala	Fri Jan 06 11:58:29 2017 +0100
     8.2 +++ b/src/Tools/jEdit/src/state_dockable.scala	Fri Jan 06 13:27:18 2017 +0100
     8.3 @@ -64,7 +64,7 @@
     8.4    {
     8.5      GUI_Thread.require {}
     8.6  
     8.7 -    PIDE.document_model(view.getBuffer).map(_.snapshot()) match {
     8.8 +    Document_Model.get(view.getBuffer).map(_.snapshot()) match {
     8.9        case Some(snapshot) =>
    8.10          (PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
    8.11            case (Some(command1), Some(command2)) if command1.id == command2.id =>
     9.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Fri Jan 06 11:58:29 2017 +0100
     9.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Jan 06 13:27:18 2017 +0100
     9.3 @@ -41,7 +41,7 @@
     9.4              if (clicks == 1) {
     9.5                for {
     9.6                  buffer <- JEdit_Lib.jedit_buffer(listData(index))
     9.7 -                model <- PIDE.document_model(buffer)
     9.8 +                model <- Document_Model.get(buffer)
     9.9                } model.node_required = !model.node_required
    9.10              }
    9.11            }
    9.12 @@ -97,7 +97,7 @@
    9.13      nodes_required = Set.empty
    9.14      for {
    9.15        buffer <- JEdit_Lib.jedit_buffers
    9.16 -      model <- PIDE.document_model(buffer)
    9.17 +      model <- Document_Model.get(buffer)
    9.18        if model.node_required
    9.19      } nodes_required += model.node_name
    9.20    }