separate Buffer_Model vs. File_Model;
authorwenzelm
Sat Jan 07 14:34:53 2017 +0100 (2017-01-07)
changeset 648170bb6b582bb4f
parent 64816 e306cab8edf9
child 64818 67a0a563d2b3
separate Buffer_Model vs. File_Model;
misc tuning and clarification;
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sat Jan 07 11:22:13 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sat Jan 07 14:34:53 2017 +0100
     1.3 @@ -34,13 +34,16 @@
     1.4    def check(buffer: Buffer): Boolean =
     1.5      JEdit_Lib.buffer_name(buffer).endsWith(".bib")
     1.6  
     1.7 +  def check(name: Document.Node.Name): Boolean =
     1.8 +    name.node.endsWith(".bib")
     1.9 +
    1.10  
    1.11    /* parse entries */
    1.12  
    1.13 -  def parse_buffer_entries(buffer: Buffer): List[(String, Text.Offset)] =
    1.14 +  def parse_entries(text: String): List[(String, Text.Offset)] =
    1.15    {
    1.16      val chunks =
    1.17 -      try { Bibtex.parse(JEdit_Lib.buffer_text(buffer)) }
    1.18 +      try { Bibtex.parse(text) }
    1.19        catch { case ERROR(msg) => Output.warning(msg); Nil }
    1.20  
    1.21      val result = new mutable.ListBuffer[(String, Text.Offset)]
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 11:22:13 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 14:34:53 2017 +0100
     2.3 @@ -2,8 +2,8 @@
     2.4      Author:     Fabian Immler, TU Munich
     2.5      Author:     Makarius
     2.6  
     2.7 -Document model connected to jEdit buffer (node in theory graph or
     2.8 -auxiliary file).
     2.9 +Document model connected to jEdit buffer or external file: content of theory
    2.10 +node or auxiliary file (blob).
    2.11  */
    2.12  
    2.13  package isabelle.jedit
    2.14 @@ -14,74 +14,299 @@
    2.15  import scala.collection.mutable
    2.16  import scala.util.parsing.input.CharSequenceReader
    2.17  
    2.18 -import org.gjt.sp.jedit.jEdit
    2.19 +import org.gjt.sp.jedit.{jEdit, View}
    2.20  import org.gjt.sp.jedit.Buffer
    2.21  import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
    2.22  
    2.23  
    2.24  object Document_Model
    2.25  {
    2.26 -  /* global state */
    2.27 +  /* document models */
    2.28 +
    2.29 +  sealed case class State(
    2.30 +    models: Map[Document.Node.Name, Document_Model] = Map.empty,
    2.31 +    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty)
    2.32 +  {
    2.33 +    def models_iterator: Iterator[Document_Model] =
    2.34 +      for ((_, model) <- models.iterator) yield model
    2.35  
    2.36 -  sealed case class State(buffer_models: Map[JEditBuffer, Document_Model] = Map.empty)
    2.37 +    def file_models_iterator: Iterator[File_Model] =
    2.38 +      for {
    2.39 +        (_, model) <- models.iterator
    2.40 +        if model.isInstanceOf[File_Model]
    2.41 +      } yield model.asInstanceOf[File_Model]
    2.42  
    2.43 -  private val state = Synchronized(State())
    2.44 +    def buffer_models_iterator: Iterator[Buffer_Model] =
    2.45 +      for ((_, model) <- buffer_models.iterator) yield model
    2.46  
    2.47  
    2.48 -  /* document model of buffer */
    2.49 +    def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
    2.50 +      : (Buffer_Model, State) =
    2.51 +    {
    2.52 +      val old_model =
    2.53 +        models.get(node_name) match {
    2.54 +          case Some(file_model: File_Model) => Some(file_model)
    2.55 +          case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
    2.56 +          case _ => None
    2.57 +        }
    2.58 +      val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
    2.59 +      (buffer_model,
    2.60 +        copy(models = models + (node_name -> buffer_model),
    2.61 +          buffer_models = buffer_models + (buffer -> buffer_model)))
    2.62 +    }
    2.63 +
    2.64 +    def close_buffer(buffer: JEditBuffer): State =
    2.65 +    {
    2.66 +      buffer_models.get(buffer) match {
    2.67 +        case None => this
    2.68 +        case Some(buffer_model) =>
    2.69 +          val file_model = buffer_model.exit()
    2.70 +          copy(models = models + (file_model.node_name -> file_model),
    2.71 +            buffer_models = buffer_models - buffer)
    2.72 +      }
    2.73 +    }
    2.74 +  }
    2.75  
    2.76 -  def get(buffer: JEditBuffer): Option[Document_Model] =
    2.77 +  private val state = Synchronized(State())  // owned by GUI thread
    2.78 +
    2.79 +  def get(name: Document.Node.Name): Option[Document_Model] =
    2.80 +    state.value.models.get(name)
    2.81 +
    2.82 +  def get(buffer: JEditBuffer): Option[Buffer_Model] =
    2.83      state.value.buffer_models.get(buffer)
    2.84  
    2.85 +  def is_stable(): Boolean =
    2.86 +    state.value.models_iterator.forall(_.is_stable)
    2.87 +
    2.88 +
    2.89 +  /* init and exit */
    2.90 +
    2.91 +  def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
    2.92 +  {
    2.93 +    GUI_Thread.require {}
    2.94 +    state.change_result(st =>
    2.95 +      st.buffer_models.get(buffer) match {
    2.96 +        case Some(buffer_model) if buffer_model.node_name == node_name =>
    2.97 +          buffer_model.init_token_marker
    2.98 +          (buffer_model, st)
    2.99 +        case _ =>
   2.100 +          val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
   2.101 +          buffer.propertiesChanged
   2.102 +          res
   2.103 +      })
   2.104 +  }
   2.105 +
   2.106    def exit(buffer: Buffer)
   2.107    {
   2.108      GUI_Thread.require {}
   2.109      state.change(st =>
   2.110 -      st.buffer_models.get(buffer) match {
   2.111 -        case None => st
   2.112 -        case Some(model) =>
   2.113 -          model.deactivate()
   2.114 -          buffer.propertiesChanged
   2.115 -          st.copy(buffer_models = st.buffer_models - buffer)
   2.116 +      if (st.buffer_models.isDefinedAt(buffer)) {
   2.117 +        val res = st.close_buffer(buffer)
   2.118 +        buffer.propertiesChanged
   2.119 +        res
   2.120 +      }
   2.121 +      else st)
   2.122 +  }
   2.123 +
   2.124 +
   2.125 +  /* required nodes */
   2.126 +
   2.127 +  def required_nodes(): Set[Document.Node.Name] =
   2.128 +    (for {
   2.129 +      model <- state.value.models_iterator
   2.130 +      if model.node_required
   2.131 +    } yield model.node_name).toSet
   2.132 +
   2.133 +  def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false)
   2.134 +  {
   2.135 +    GUI_Thread.require {}
   2.136 +
   2.137 +    val changed =
   2.138 +      state.change_result(st =>
   2.139 +        st.models.get(name) match {
   2.140 +          case None => (false, st)
   2.141 +          case Some(model) =>
   2.142 +            val required = if (toggle) !model.node_required else set
   2.143 +            model match {
   2.144 +              case model1: File_Model if required != model1.node_required =>
   2.145 +                (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
   2.146 +              case model1: Buffer_Model if required != model1.node_required =>
   2.147 +                model1.set_node_required(required); (true, st)
   2.148 +              case _ => (false, st)
   2.149 +            }
   2.150 +        })
   2.151 +    if (changed) {
   2.152 +      PIDE.options_changed()
   2.153 +      PIDE.editor.flush()
   2.154 +    }
   2.155 +  }
   2.156 +
   2.157 +  def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
   2.158 +    Document_Model.get(view.getBuffer).foreach(model =>
   2.159 +      node_required(model.node_name, toggle = toggle, set = set))
   2.160 +
   2.161 +
   2.162 +  /* flushed edits */
   2.163 +
   2.164 +  def flush_edits(hidden: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
   2.165 +  {
   2.166 +    GUI_Thread.require {}
   2.167 +
   2.168 +    state.change_result(st =>
   2.169 +      {
   2.170 +        val doc_blobs =
   2.171 +          Document.Blobs(
   2.172 +            (for {
   2.173 +              model <- st.models_iterator
   2.174 +              blob <- model.get_blob
   2.175 +            } yield (model.node_name -> blob)).toMap)
   2.176 +
   2.177 +        val buffer_edits =
   2.178 +          (for {
   2.179 +            model <- st.buffer_models_iterator
   2.180 +            edit <- model.flush_edits(doc_blobs, hidden).iterator
   2.181 +          } yield edit).toList
   2.182 +
   2.183 +        val file_edits =
   2.184 +          (for {
   2.185 +            model <- st.file_models_iterator
   2.186 +            change <- model.flush_edits(doc_blobs, hidden)
   2.187 +          } yield change).toList
   2.188 +
   2.189 +        val edits = buffer_edits ::: file_edits.flatMap(_._1)
   2.190 +
   2.191 +        ((doc_blobs, edits),
   2.192 +          st.copy(
   2.193 +            models = (st.models /: file_edits) { case (ms, (_, m)) => ms + (m.node_name -> m) }))
   2.194        })
   2.195    }
   2.196  
   2.197 -  def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
   2.198 +
   2.199 +  /* file content */
   2.200 +
   2.201 +  sealed case class File_Content(text: String)
   2.202 +  {
   2.203 +    lazy val bytes: Bytes = Bytes(text)
   2.204 +    lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
   2.205 +    lazy val bibtex_entries: List[(String, Text.Offset)] = Bibtex_JEdit.parse_entries(text)
   2.206 +  }
   2.207 +}
   2.208 +
   2.209 +trait Document_Model extends Document.Model
   2.210 +{
   2.211 +  /* content */
   2.212 +
   2.213 +  def bibtex_entries: List[(String, Text.Offset)]
   2.214 +
   2.215 +
   2.216 +  /* perspective */
   2.217 +
   2.218 +  def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
   2.219 +
   2.220 +  def node_perspective(
   2.221 +    doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
   2.222    {
   2.223      GUI_Thread.require {}
   2.224 -    val model =
   2.225 -      state.change_result(st =>
   2.226 -        {
   2.227 -          val old_model = st.buffer_models.get(buffer)
   2.228 -          old_model match {
   2.229 -            case Some(model) if model.node_name == node_name => (model, st)
   2.230 -            case _ =>
   2.231 -              old_model.foreach(_.deactivate)
   2.232 -              val model = new Document_Model(session, buffer, node_name)
   2.233 -              model.activate()
   2.234 -              buffer.propertiesChanged
   2.235 -              (model, st.copy(st.buffer_models + (buffer -> model)))
   2.236 -          }
   2.237 -        })
   2.238 -    model.init_token_marker
   2.239 -    model
   2.240 +
   2.241 +    if (Isabelle.continuous_checking && is_theory) {
   2.242 +      val snapshot = this.snapshot()
   2.243 +
   2.244 +      val reparse = snapshot.node.load_commands_changed(doc_blobs)
   2.245 +      val perspective =
   2.246 +        if (hidden) Text.Perspective.empty
   2.247 +        else {
   2.248 +          val view_ranges = document_view_ranges(snapshot)
   2.249 +          val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
   2.250 +          Text.Perspective(view_ranges ::: load_ranges)
   2.251 +        }
   2.252 +      val overlays = PIDE.editor.node_overlays(node_name)
   2.253 +
   2.254 +      (reparse, Document.Node.Perspective(node_required, perspective, overlays))
   2.255 +    }
   2.256 +    else (false, Document.Node.no_perspective_text)
   2.257    }
   2.258  }
   2.259  
   2.260 -class Document_Model private(
   2.261 -  val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
   2.262 +case class File_Model(
   2.263 +  session: Session,
   2.264 +  node_name: Document.Node.Name,
   2.265 +  content: Document_Model.File_Content,
   2.266 +  node_required: Boolean = false,
   2.267 +  last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
   2.268 +  pending_edits: List[Text.Edit] = Nil) extends Document_Model
   2.269  {
   2.270 -  override def toString: String = node_name.toString
   2.271 +  /* header */
   2.272 +
   2.273 +  // FIXME eliminate clone
   2.274 +  def node_header: Document.Node.Header =
   2.275 +    PIDE.resources.special_header(node_name) getOrElse
   2.276 +    {
   2.277 +      if (is_theory)
   2.278 +        PIDE.resources.check_thy_reader(
   2.279 +          "", node_name, new CharSequenceReader(content.text), Token.Pos.command)
   2.280 +      else Document.Node.no_header
   2.281 +    }
   2.282 +
   2.283 +
   2.284 +  /* content */
   2.285 +
   2.286 +  def get_blob: Option[Document.Blob] =
   2.287 +    if (is_theory) None
   2.288 +    else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
   2.289 +
   2.290 +  def bibtex_entries: List[(String, Text.Offset)] =
   2.291 +    if (Bibtex_JEdit.check(node_name)) content.bibtex_entries else Nil
   2.292  
   2.293  
   2.294 -  /* header */
   2.295 +  /* edits */
   2.296 +
   2.297 +  def update_text(text: String): Option[File_Model] =
   2.298 +    Text.Edit.replace(0, content.text, text) match {
   2.299 +      case Nil => None
   2.300 +      case edits =>
   2.301 +        val content1 = Document_Model.File_Content(text)
   2.302 +        val pending_edits1 = pending_edits ::: edits
   2.303 +        Some(copy(content = content1, pending_edits = pending_edits1))
   2.304 +    }
   2.305  
   2.306 -  def is_theory: Boolean = node_name.is_theory
   2.307 +  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
   2.308 +    : Option[(List[Document.Edit_Text], File_Model)] =
   2.309 +  {
   2.310 +    val (reparse, perspective) = node_perspective(doc_blobs, hidden)
   2.311 +    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
   2.312 +      // FIXME eliminate clone
   2.313 +      val edits: List[Document.Edit_Text] =
   2.314 +        get_blob match {
   2.315 +          case None =>
   2.316 +            List(session.header_edit(node_name, node_header),
   2.317 +              node_name -> Document.Node.Edits(pending_edits.toList),
   2.318 +              node_name -> perspective)
   2.319 +          case Some(blob) =>
   2.320 +            List(node_name -> Document.Node.Blob(blob),
   2.321 +              node_name -> Document.Node.Edits(pending_edits.toList))
   2.322 +        }
   2.323 +      Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
   2.324 +    }
   2.325 +    else None
   2.326 +  }
   2.327 +
   2.328 +
   2.329 +  /* snapshot */
   2.330 +
   2.331 +  def is_stable: Boolean = pending_edits.isEmpty
   2.332 +  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.toList)
   2.333 +}
   2.334 +
   2.335 +case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
   2.336 +  extends Document_Model
   2.337 +{
   2.338 +  /* header */
   2.339  
   2.340    def node_header(): Document.Node.Header =
   2.341    {
   2.342      GUI_Thread.require {}
   2.343  
   2.344 +    // FIXME eliminate clone
   2.345      PIDE.resources.special_header(node_name) getOrElse
   2.346      {
   2.347        if (is_theory) {
   2.348 @@ -111,39 +336,16 @@
   2.349    // owned by GUI thread
   2.350    private var _node_required = false
   2.351    def node_required: Boolean = _node_required
   2.352 -  def node_required_=(b: Boolean)
   2.353 -  {
   2.354 -    GUI_Thread.require {}
   2.355 -    if (_node_required != b && is_theory) {
   2.356 -      _node_required = b
   2.357 -      PIDE.options_changed()
   2.358 -      PIDE.editor.flush()
   2.359 -    }
   2.360 -  }
   2.361 +  def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }
   2.362  
   2.363 -  def node_perspective(hidden: Boolean, doc_blobs: Document.Blobs)
   2.364 -    : (Boolean, Document.Node.Perspective_Text) =
   2.365 +  override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
   2.366    {
   2.367      GUI_Thread.require {}
   2.368  
   2.369 -    if (Isabelle.continuous_checking && is_theory) {
   2.370 -      val snapshot = this.snapshot()
   2.371 -
   2.372 -      val document_view_ranges =
   2.373 -        for {
   2.374 -          doc_view <- PIDE.document_views(buffer)
   2.375 -          range <- doc_view.perspective(snapshot).ranges
   2.376 -        } yield range
   2.377 -
   2.378 -      val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
   2.379 -      val reparse = snapshot.node.load_commands_changed(doc_blobs)
   2.380 -
   2.381 -      (reparse,
   2.382 -        Document.Node.Perspective(node_required,
   2.383 -          Text.Perspective(if (hidden) Nil else document_view_ranges ::: load_ranges),
   2.384 -          PIDE.editor.node_overlays(node_name)))
   2.385 -    }
   2.386 -    else (false, Document.Node.no_perspective_text)
   2.387 +    (for {
   2.388 +      doc_view <- PIDE.document_views(buffer).iterator
   2.389 +      range <- doc_view.perspective(snapshot).ranges.iterator
   2.390 +    } yield range).toList
   2.391    }
   2.392  
   2.393  
   2.394 @@ -153,7 +355,7 @@
   2.395  
   2.396    private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
   2.397  
   2.398 -  def get_blob(): Option[Document.Blob] =
   2.399 +  def get_blob: Option[Document.Blob] =
   2.400      GUI_Thread.require {
   2.401        if (is_theory) None
   2.402        else {
   2.403 @@ -174,18 +376,19 @@
   2.404  
   2.405    /* bibtex entries */
   2.406  
   2.407 -  private var _bibtex: Option[List[(String, Text.Offset)]] = None  // owned by GUI thread
   2.408 +  private var _bibtex_entries: Option[List[(String, Text.Offset)]] = None  // owned by GUI thread
   2.409  
   2.410 -  private def reset_bibtex(): Unit = GUI_Thread.require { _bibtex = None }
   2.411 +  private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
   2.412  
   2.413 -  def bibtex_entries(): List[(String, Text.Offset)] =
   2.414 +  def bibtex_entries: List[(String, Text.Offset)] =
   2.415      GUI_Thread.require {
   2.416        if (Bibtex_JEdit.check(buffer)) {
   2.417 -        _bibtex match {
   2.418 +        _bibtex_entries match {
   2.419            case Some(entries) => entries
   2.420            case None =>
   2.421 -            val entries = Bibtex_JEdit.parse_buffer_entries(buffer)
   2.422 -            _bibtex = Some(entries)
   2.423 +            val text = JEdit_Lib.buffer_text(buffer)
   2.424 +            val entries = Bibtex_JEdit.parse_entries(text)
   2.425 +            _bibtex_entries = Some(entries)
   2.426              entries
   2.427          }
   2.428        }
   2.429 @@ -201,7 +404,7 @@
   2.430        perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
   2.431    {
   2.432      val edits: List[Document.Edit_Text] =
   2.433 -      get_blob() match {
   2.434 +      get_blob match {
   2.435          case None =>
   2.436            val header_edit = session.header_edit(node_name, node_header())
   2.437            if (clear)
   2.438 @@ -230,15 +433,18 @@
   2.439      private var last_perspective = Document.Node.no_perspective_text
   2.440  
   2.441      def is_pending(): Boolean = synchronized { pending_clear || pending.nonEmpty }
   2.442 -    def snapshot(): List[Text.Edit] = synchronized { pending.toList }
   2.443 +    def get_edits(): List[Text.Edit] = synchronized { pending.toList }
   2.444 +    def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
   2.445 +    def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
   2.446 +      synchronized { last_perspective = perspective }
   2.447  
   2.448 -    def flushed_edits(hidden: Boolean, doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   2.449 +    def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
   2.450        synchronized {
   2.451          GUI_Thread.require {}
   2.452  
   2.453          val clear = pending_clear
   2.454 -        val edits = snapshot()
   2.455 -        val (reparse, perspective) = node_perspective(hidden, doc_blobs)
   2.456 +        val edits = get_edits()
   2.457 +        val (reparse, perspective) = node_perspective(doc_blobs, hidden)
   2.458          if (clear || reparse || edits.nonEmpty || last_perspective != perspective) {
   2.459            pending_clear = false
   2.460            pending.clear
   2.461 @@ -253,7 +459,7 @@
   2.462        GUI_Thread.require {}
   2.463  
   2.464        reset_blob()
   2.465 -      reset_bibtex()
   2.466 +      reset_bibtex_entries()
   2.467  
   2.468        for (doc_view <- PIDE.document_views(buffer))
   2.469          doc_view.rich_text_area.active_reset()
   2.470 @@ -268,12 +474,10 @@
   2.471    }
   2.472  
   2.473    def is_stable(): Boolean = !pending_edits.is_pending();
   2.474 +  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits())
   2.475  
   2.476 -  def snapshot(): Document.Snapshot =
   2.477 -    session.snapshot(node_name, pending_edits.snapshot())
   2.478 -
   2.479 -  def flushed_edits(hidden: Boolean, doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   2.480 -    pending_edits.flushed_edits(hidden, doc_blobs)
   2.481 +  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
   2.482 +    pending_edits.flush_edits(doc_blobs, hidden)
   2.483  
   2.484  
   2.485    /* buffer listener */
   2.486 @@ -312,7 +516,7 @@
   2.487      buffer.invalidateCachedFoldLevels
   2.488    }
   2.489  
   2.490 -  private def init_token_marker()
   2.491 +  def init_token_marker()
   2.492    {
   2.493      Isabelle.buffer_token_marker(buffer) match {
   2.494        case Some(marker) if marker != buffer.getTokenMarker =>
   2.495 @@ -323,18 +527,43 @@
   2.496    }
   2.497  
   2.498  
   2.499 -  /* activation */
   2.500 +  /* init */
   2.501 +
   2.502 +  def init(old_model: Option[File_Model]): Buffer_Model =
   2.503 +  {
   2.504 +    GUI_Thread.require {}
   2.505  
   2.506 -  private def activate()
   2.507 -  {
   2.508 -    pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   2.509 +    old_model match {
   2.510 +      case None =>
   2.511 +        pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   2.512 +      case Some(file_model) =>
   2.513 +        set_node_required(file_model.node_required)
   2.514 +        pending_edits.set_last_perspective(file_model.last_perspective)
   2.515 +        for {
   2.516 +          edit <-
   2.517 +            file_model.pending_edits :::
   2.518 +              Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))
   2.519 +        } pending_edits.edit(false, edit)
   2.520 +    }
   2.521 +
   2.522      buffer.addBufferListener(buffer_listener)
   2.523      init_token_marker()
   2.524 +
   2.525 +    this
   2.526    }
   2.527  
   2.528 -  private def deactivate()
   2.529 +
   2.530 +  /* exit */
   2.531 +
   2.532 +  def exit(): File_Model =
   2.533    {
   2.534 +    GUI_Thread.require {}
   2.535 +
   2.536      buffer.removeBufferListener(buffer_listener)
   2.537      init_token_marker()
   2.538 +
   2.539 +    val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer))
   2.540 +    File_Model(session, node_name, content, node_required,
   2.541 +      pending_edits.get_last_perspective, pending_edits.get_edits())
   2.542    }
   2.543  }
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Jan 07 11:22:13 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Jan 07 14:34:53 2017 +0100
     3.3 @@ -45,7 +45,7 @@
     3.4      }
     3.5    }
     3.6  
     3.7 -  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
     3.8 +  def init(model: Buffer_Model, text_area: JEditTextArea): Document_View =
     3.9    {
    3.10      exit(text_area)
    3.11      val doc_view = new Document_View(model, text_area)
    3.12 @@ -56,7 +56,7 @@
    3.13  }
    3.14  
    3.15  
    3.16 -class Document_View(val model: Document_Model, val text_area: JEditTextArea)
    3.17 +class Document_View(val model: Buffer_Model, val text_area: JEditTextArea)
    3.18  {
    3.19    private val session = model.session
    3.20  
     4.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sat Jan 07 11:22:13 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Jan 07 14:34:53 2017 +0100
     4.3 @@ -228,19 +228,9 @@
     4.4  
     4.5    /* required document nodes */
     4.6  
     4.7 -  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
     4.8 -  {
     4.9 -    GUI_Thread.require {}
    4.10 -    Document_Model.get(view.getBuffer) match {
    4.11 -      case Some(model) =>
    4.12 -        model.node_required = (if (toggle) !model.node_required else set)
    4.13 -      case None =>
    4.14 -    }
    4.15 -  }
    4.16 -
    4.17 -  def set_node_required(view: View) { node_required_update(view, set = true) }
    4.18 -  def reset_node_required(view: View) { node_required_update(view, set = false) }
    4.19 -  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
    4.20 +  def set_node_required(view: View) { Document_Model.view_node_required(view, set = true) }
    4.21 +  def reset_node_required(view: View) { Document_Model.view_node_required(view, set = false) }
    4.22 +  def toggle_node_required(view: View) { Document_Model.view_node_required(view, toggle = true) }
    4.23  
    4.24  
    4.25    /* font size */
     5.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Jan 07 11:22:13 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Jan 07 14:34:53 2017 +0100
     5.3 @@ -22,27 +22,11 @@
     5.4  
     5.5    override def session: Session = PIDE.session
     5.6  
     5.7 -  // owned by GUI thread
     5.8 -  private var removed_nodes = Set.empty[Document.Node.Name]
     5.9 -
    5.10 -  def remove_node(name: Document.Node.Name): Unit =
    5.11 -    GUI_Thread.require { removed_nodes += name }
    5.12 -
    5.13 -  override def flush(hidden: Boolean = false)
    5.14 -  {
    5.15 -    GUI_Thread.require {}
    5.16 -
    5.17 -    val doc_blobs = PIDE.document_blobs()
    5.18 -    val models = PIDE.document_models()
    5.19 -
    5.20 -    val removed = removed_nodes; removed_nodes = Set.empty
    5.21 -    val removed_perspective =
    5.22 -      (removed -- models.iterator.map(_.node_name)).toList.map(
    5.23 -        name => (name, Document.Node.no_perspective_text))
    5.24 -
    5.25 -    val edits = models.flatMap(_.flushed_edits(hidden, doc_blobs)) ::: removed_perspective
    5.26 -    session.update(doc_blobs, edits)
    5.27 -  }
    5.28 +  override def flush(hidden: Boolean = false): Unit =
    5.29 +    GUI_Thread.require {
    5.30 +      val (doc_blobs, edits) = Document_Model.flush_edits(hidden)
    5.31 +      session.update(doc_blobs, edits)
    5.32 +    }
    5.33  
    5.34    private val delay1_flush =
    5.35      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    5.36 @@ -55,7 +39,7 @@
    5.37  
    5.38    def stable_tip_version(): Option[Document.Version] =
    5.39      GUI_Thread.require {
    5.40 -      if (removed_nodes.isEmpty && PIDE.document_models().forall(_.is_stable))
    5.41 +      if (Document_Model.is_stable())
    5.42          session.current_state().stable_tip_version
    5.43        else None
    5.44      }
    5.45 @@ -81,13 +65,8 @@
    5.46    override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    5.47    {
    5.48      GUI_Thread.require {}
    5.49 -
    5.50 -    JEdit_Lib.jedit_buffer(name) match {
    5.51 -      case Some(buffer) =>
    5.52 -        Document_Model.get(buffer) match {
    5.53 -          case Some(model) => model.snapshot
    5.54 -          case None => session.snapshot(name)
    5.55 -        }
    5.56 +    Document_Model.get(name) match {
    5.57 +      case Some(model) => model.snapshot
    5.58        case None => session.snapshot(name)
    5.59      }
    5.60    }
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Jan 07 11:22:13 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Jan 07 14:34:53 2017 +0100
     6.3 @@ -71,20 +71,6 @@
     6.4        doc_view <- document_view(text_area)
     6.5      } yield doc_view
     6.6  
     6.7 -  def document_models(): List[Document_Model] =
     6.8 -    for {
     6.9 -      buffer <- JEdit_Lib.jedit_buffers().toList
    6.10 -      model <- Document_Model.get(buffer)
    6.11 -    } yield model
    6.12 -
    6.13 -  def document_blobs(): Document.Blobs =
    6.14 -    Document.Blobs(
    6.15 -      (for {
    6.16 -        buffer <- JEdit_Lib.jedit_buffers()
    6.17 -        model <- Document_Model.get(buffer)
    6.18 -        blob <- model.get_blob
    6.19 -      } yield (model.node_name -> blob)).toMap)
    6.20 -
    6.21    def exit_models(buffers: List[Buffer])
    6.22    {
    6.23      GUI_Thread.now {
    6.24 @@ -109,7 +95,7 @@
    6.25          if (buffer.isLoaded) {
    6.26            JEdit_Lib.buffer_lock(buffer) {
    6.27              val node_name = resources.node_name(buffer)
    6.28 -            val model = Document_Model.init(session, buffer, node_name)
    6.29 +            val model = Document_Model.init(session, node_name, buffer)
    6.30              for {
    6.31                text_area <- JEdit_Lib.jedit_text_areas(buffer)
    6.32                if document_view(text_area).map(_.model) != Some(model)
    6.33 @@ -340,10 +326,9 @@
    6.34            msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
    6.35            msg.getWhat == BufferUpdate.CLOSING =>
    6.36  
    6.37 -          if (msg.getWhat == BufferUpdate.CLOSING) {
    6.38 -            val buffer = msg.getBuffer
    6.39 -            if (buffer != null) PIDE.editor.remove_node(PIDE.resources.node_name(msg.getBuffer))
    6.40 -          }
    6.41 +          if (msg.getWhat == BufferUpdate.CLOSING && msg.getBuffer != null)
    6.42 +            PIDE.exit_models(List(msg.getBuffer))
    6.43 +
    6.44            if (PIDE.session.is_ready) {
    6.45              delay_init.invoke()
    6.46              delay_load.invoke()
     7.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Jan 07 11:22:13 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Jan 07 14:34:53 2017 +0100
     7.3 @@ -38,12 +38,7 @@
     7.4          val index = peer.locationToIndex(point)
     7.5          if (index >= 0) {
     7.6            if (in_checkbox(peer.indexToLocation(index), point)) {
     7.7 -            if (clicks == 1) {
     7.8 -              for {
     7.9 -                buffer <- JEdit_Lib.jedit_buffer(listData(index))
    7.10 -                model <- Document_Model.get(buffer)
    7.11 -              } model.node_required = !model.node_required
    7.12 -            }
    7.13 +            if (clicks == 1) Document_Model.node_required(listData(index), toggle = true)
    7.14            }
    7.15            else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
    7.16          }
    7.17 @@ -90,18 +85,7 @@
    7.18    /* component state -- owned by GUI thread */
    7.19  
    7.20    private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
    7.21 -  private var nodes_required: Set[Document.Node.Name] = Set.empty
    7.22 -
    7.23 -  private def update_nodes_required()
    7.24 -  {
    7.25 -    nodes_required = Set.empty
    7.26 -    for {
    7.27 -      buffer <- JEdit_Lib.jedit_buffers
    7.28 -      model <- Document_Model.get(buffer)
    7.29 -      if model.node_required
    7.30 -    } nodes_required += model.node_name
    7.31 -  }
    7.32 -  update_nodes_required()
    7.33 +  private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
    7.34  
    7.35    private def in_checkbox(loc0: Point, p: Point): Boolean =
    7.36      Node_Renderer_Component != null &&
    7.37 @@ -229,7 +213,7 @@
    7.38          GUI_Thread.later {
    7.39            continuous_checking.load()
    7.40            logic.load ()
    7.41 -          update_nodes_required()
    7.42 +          nodes_required = Document_Model.required_nodes()
    7.43            status.repaint()
    7.44          }
    7.45