src/Tools/jEdit/src/document_model.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64836 3611f759f896
child 64858 e31cf6eaecb8
permissions -rw-r--r--
tuned signature;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/document_model.scala
wenzelm@36760
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36760
     3
    Author:     Makarius
wenzelm@36760
     4
wenzelm@64817
     5
Document model connected to jEdit buffer or external file: content of theory
wenzelm@64817
     6
node or auxiliary file (blob).
wenzelm@36760
     7
*/
wenzelm@34407
     8
wenzelm@34784
     9
package isabelle.jedit
wenzelm@34760
    10
wenzelm@34318
    11
wenzelm@36015
    12
import isabelle._
wenzelm@36015
    13
wenzelm@34693
    14
import scala.collection.mutable
wenzelm@34446
    15
wenzelm@64817
    16
import org.gjt.sp.jedit.{jEdit, View}
wenzelm@34784
    17
import org.gjt.sp.jedit.Buffer
wenzelm@61192
    18
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
wenzelm@34318
    19
wenzelm@34760
    20
wenzelm@34784
    21
object Document_Model
wenzelm@34588
    22
{
wenzelm@64817
    23
  /* document models */
wenzelm@64817
    24
wenzelm@64817
    25
  sealed case class State(
wenzelm@64817
    26
    models: Map[Document.Node.Name, Document_Model] = Map.empty,
wenzelm@64817
    27
    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty)
wenzelm@64817
    28
  {
wenzelm@64817
    29
    def models_iterator: Iterator[Document_Model] =
wenzelm@64817
    30
      for ((_, model) <- models.iterator) yield model
wenzelm@64813
    31
wenzelm@64817
    32
    def file_models_iterator: Iterator[File_Model] =
wenzelm@64817
    33
      for {
wenzelm@64817
    34
        (_, model) <- models.iterator
wenzelm@64817
    35
        if model.isInstanceOf[File_Model]
wenzelm@64817
    36
      } yield model.asInstanceOf[File_Model]
wenzelm@64813
    37
wenzelm@64817
    38
    def buffer_models_iterator: Iterator[Buffer_Model] =
wenzelm@64817
    39
      for ((_, model) <- buffer_models.iterator) yield model
wenzelm@64813
    40
wenzelm@64813
    41
wenzelm@64817
    42
    def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
wenzelm@64817
    43
      : (Buffer_Model, State) =
wenzelm@64817
    44
    {
wenzelm@64817
    45
      val old_model =
wenzelm@64817
    46
        models.get(node_name) match {
wenzelm@64817
    47
          case Some(file_model: File_Model) => Some(file_model)
wenzelm@64817
    48
          case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
wenzelm@64817
    49
          case _ => None
wenzelm@64817
    50
        }
wenzelm@64817
    51
      val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
wenzelm@64817
    52
      (buffer_model,
wenzelm@64817
    53
        copy(models = models + (node_name -> buffer_model),
wenzelm@64817
    54
          buffer_models = buffer_models + (buffer -> buffer_model)))
wenzelm@64817
    55
    }
wenzelm@64817
    56
wenzelm@64817
    57
    def close_buffer(buffer: JEditBuffer): State =
wenzelm@64817
    58
    {
wenzelm@64817
    59
      buffer_models.get(buffer) match {
wenzelm@64817
    60
        case None => this
wenzelm@64817
    61
        case Some(buffer_model) =>
wenzelm@64817
    62
          val file_model = buffer_model.exit()
wenzelm@64817
    63
          copy(models = models + (file_model.node_name -> file_model),
wenzelm@64817
    64
            buffer_models = buffer_models - buffer)
wenzelm@64817
    65
      }
wenzelm@64817
    66
    }
wenzelm@64835
    67
wenzelm@64835
    68
    def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
wenzelm@64835
    69
      if (models.isDefinedAt(node_name)) this
wenzelm@64835
    70
      else {
wenzelm@64835
    71
        val edit = Text.Edit.insert(0, text)
wenzelm@64835
    72
        val model = File_Model(session, node_name, File_Content(text), pending_edits = List(edit))
wenzelm@64835
    73
        copy(models = models + (node_name -> model))
wenzelm@64835
    74
      }
wenzelm@64817
    75
  }
wenzelm@34784
    76
wenzelm@64817
    77
  private val state = Synchronized(State())  // owned by GUI thread
wenzelm@64817
    78
wenzelm@64835
    79
  def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
wenzelm@64835
    80
  def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name)
wenzelm@64835
    81
  def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
wenzelm@64817
    82
wenzelm@64831
    83
  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
wenzelm@64829
    84
    for {
wenzelm@64829
    85
      model <- state.value.models_iterator
wenzelm@64832
    86
      Text.Info(range, entry) <- model.bibtex_entries.iterator
wenzelm@64831
    87
    } yield Text.Info(range, (entry, model))
wenzelm@64829
    88
wenzelm@64817
    89
wenzelm@64836
    90
  /* syntax */
wenzelm@64836
    91
wenzelm@64836
    92
  def syntax_changed(names: List[Document.Node.Name])
wenzelm@64836
    93
  {
wenzelm@64836
    94
    GUI_Thread.require {}
wenzelm@64836
    95
wenzelm@64836
    96
    val models = state.value.models
wenzelm@64836
    97
    for (name <- names.iterator; model <- models.get(name)) {
wenzelm@64836
    98
      model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
wenzelm@64836
    99
    }
wenzelm@64836
   100
  }
wenzelm@64836
   101
wenzelm@64836
   102
wenzelm@64817
   103
  /* init and exit */
wenzelm@64817
   104
wenzelm@64817
   105
  def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
wenzelm@64817
   106
  {
wenzelm@64817
   107
    GUI_Thread.require {}
wenzelm@64817
   108
    state.change_result(st =>
wenzelm@64817
   109
      st.buffer_models.get(buffer) match {
wenzelm@64817
   110
        case Some(buffer_model) if buffer_model.node_name == node_name =>
wenzelm@64817
   111
          buffer_model.init_token_marker
wenzelm@64817
   112
          (buffer_model, st)
wenzelm@64817
   113
        case _ =>
wenzelm@64817
   114
          val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
wenzelm@64817
   115
          buffer.propertiesChanged
wenzelm@64817
   116
          res
wenzelm@64817
   117
      })
wenzelm@64817
   118
  }
wenzelm@64817
   119
wenzelm@34784
   120
  def exit(buffer: Buffer)
wenzelm@34784
   121
  {
wenzelm@57612
   122
    GUI_Thread.require {}
wenzelm@64813
   123
    state.change(st =>
wenzelm@64817
   124
      if (st.buffer_models.isDefinedAt(buffer)) {
wenzelm@64817
   125
        val res = st.close_buffer(buffer)
wenzelm@64817
   126
        buffer.propertiesChanged
wenzelm@64817
   127
        res
wenzelm@64817
   128
      }
wenzelm@64817
   129
      else st)
wenzelm@64817
   130
  }
wenzelm@64817
   131
wenzelm@64835
   132
  def provide_files(session: Session, files: List[(Document.Node.Name, String)])
wenzelm@64835
   133
  {
wenzelm@64835
   134
    GUI_Thread.require {}
wenzelm@64835
   135
    state.change(st =>
wenzelm@64835
   136
      (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) })
wenzelm@64835
   137
  }
wenzelm@64835
   138
wenzelm@64817
   139
wenzelm@64817
   140
  /* required nodes */
wenzelm@64817
   141
wenzelm@64817
   142
  def required_nodes(): Set[Document.Node.Name] =
wenzelm@64817
   143
    (for {
wenzelm@64817
   144
      model <- state.value.models_iterator
wenzelm@64817
   145
      if model.node_required
wenzelm@64817
   146
    } yield model.node_name).toSet
wenzelm@64817
   147
wenzelm@64817
   148
  def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false)
wenzelm@64817
   149
  {
wenzelm@64817
   150
    GUI_Thread.require {}
wenzelm@64817
   151
wenzelm@64817
   152
    val changed =
wenzelm@64817
   153
      state.change_result(st =>
wenzelm@64817
   154
        st.models.get(name) match {
wenzelm@64817
   155
          case None => (false, st)
wenzelm@64817
   156
          case Some(model) =>
wenzelm@64817
   157
            val required = if (toggle) !model.node_required else set
wenzelm@64817
   158
            model match {
wenzelm@64817
   159
              case model1: File_Model if required != model1.node_required =>
wenzelm@64817
   160
                (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
wenzelm@64817
   161
              case model1: Buffer_Model if required != model1.node_required =>
wenzelm@64817
   162
                model1.set_node_required(required); (true, st)
wenzelm@64817
   163
              case _ => (false, st)
wenzelm@64817
   164
            }
wenzelm@64817
   165
        })
wenzelm@64817
   166
    if (changed) {
wenzelm@64817
   167
      PIDE.options_changed()
wenzelm@64817
   168
      PIDE.editor.flush()
wenzelm@64817
   169
    }
wenzelm@64817
   170
  }
wenzelm@64817
   171
wenzelm@64817
   172
  def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
wenzelm@64817
   173
    Document_Model.get(view.getBuffer).foreach(model =>
wenzelm@64817
   174
      node_required(model.node_name, toggle = toggle, set = set))
wenzelm@64817
   175
wenzelm@64817
   176
wenzelm@64817
   177
  /* flushed edits */
wenzelm@64817
   178
wenzelm@64817
   179
  def flush_edits(hidden: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
wenzelm@64817
   180
  {
wenzelm@64817
   181
    GUI_Thread.require {}
wenzelm@64817
   182
wenzelm@64817
   183
    state.change_result(st =>
wenzelm@64817
   184
      {
wenzelm@64817
   185
        val doc_blobs =
wenzelm@64817
   186
          Document.Blobs(
wenzelm@64817
   187
            (for {
wenzelm@64817
   188
              model <- st.models_iterator
wenzelm@64817
   189
              blob <- model.get_blob
wenzelm@64817
   190
            } yield (model.node_name -> blob)).toMap)
wenzelm@64817
   191
wenzelm@64817
   192
        val buffer_edits =
wenzelm@64817
   193
          (for {
wenzelm@64817
   194
            model <- st.buffer_models_iterator
wenzelm@64817
   195
            edit <- model.flush_edits(doc_blobs, hidden).iterator
wenzelm@64817
   196
          } yield edit).toList
wenzelm@64817
   197
wenzelm@64817
   198
        val file_edits =
wenzelm@64817
   199
          (for {
wenzelm@64817
   200
            model <- st.file_models_iterator
wenzelm@64817
   201
            change <- model.flush_edits(doc_blobs, hidden)
wenzelm@64817
   202
          } yield change).toList
wenzelm@64817
   203
wenzelm@64817
   204
        val edits = buffer_edits ::: file_edits.flatMap(_._1)
wenzelm@64817
   205
wenzelm@64817
   206
        ((doc_blobs, edits),
wenzelm@64817
   207
          st.copy(
wenzelm@64817
   208
            models = (st.models /: file_edits) { case (ms, (_, m)) => ms + (m.node_name -> m) }))
wenzelm@64813
   209
      })
wenzelm@34318
   210
  }
wenzelm@43397
   211
wenzelm@64817
   212
wenzelm@64817
   213
  /* file content */
wenzelm@64817
   214
wenzelm@64817
   215
  sealed case class File_Content(text: String)
wenzelm@64817
   216
  {
wenzelm@64835
   217
    lazy val bytes: Bytes = Bytes(Symbol.encode(text))
wenzelm@64817
   218
    lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
wenzelm@64831
   219
    lazy val bibtex_entries: List[Text.Info[String]] =
wenzelm@64831
   220
      try { Bibtex.document_entries(text) }
wenzelm@64828
   221
      catch { case ERROR(msg) => Output.warning(msg); Nil }
wenzelm@64817
   222
  }
wenzelm@64817
   223
}
wenzelm@64817
   224
wenzelm@64829
   225
sealed abstract class Document_Model extends Document.Model
wenzelm@64817
   226
{
wenzelm@64817
   227
  /* content */
wenzelm@64817
   228
wenzelm@64831
   229
  def bibtex_entries: List[Text.Info[String]]
wenzelm@64817
   230
wenzelm@64817
   231
wenzelm@64817
   232
  /* perspective */
wenzelm@64817
   233
wenzelm@64817
   234
  def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
wenzelm@64817
   235
wenzelm@64817
   236
  def node_perspective(
wenzelm@64817
   237
    doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
wenzelm@43397
   238
  {
wenzelm@57612
   239
    GUI_Thread.require {}
wenzelm@64817
   240
wenzelm@64817
   241
    if (Isabelle.continuous_checking && is_theory) {
wenzelm@64817
   242
      val snapshot = this.snapshot()
wenzelm@64817
   243
wenzelm@64817
   244
      val reparse = snapshot.node.load_commands_changed(doc_blobs)
wenzelm@64817
   245
      val perspective =
wenzelm@64817
   246
        if (hidden) Text.Perspective.empty
wenzelm@64817
   247
        else {
wenzelm@64817
   248
          val view_ranges = document_view_ranges(snapshot)
wenzelm@64817
   249
          val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
wenzelm@64817
   250
          Text.Perspective(view_ranges ::: load_ranges)
wenzelm@64817
   251
        }
wenzelm@64817
   252
      val overlays = PIDE.editor.node_overlays(node_name)
wenzelm@64817
   253
wenzelm@64817
   254
      (reparse, Document.Node.Perspective(node_required, perspective, overlays))
wenzelm@64817
   255
    }
wenzelm@64817
   256
    else (false, Document.Node.no_perspective_text)
wenzelm@43397
   257
  }
wenzelm@34318
   258
}
wenzelm@34318
   259
wenzelm@64817
   260
case class File_Model(
wenzelm@64817
   261
  session: Session,
wenzelm@64817
   262
  node_name: Document.Node.Name,
wenzelm@64817
   263
  content: Document_Model.File_Content,
wenzelm@64817
   264
  node_required: Boolean = false,
wenzelm@64817
   265
  last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
wenzelm@64817
   266
  pending_edits: List[Text.Edit] = Nil) extends Document_Model
wenzelm@34588
   267
{
wenzelm@64817
   268
  /* header */
wenzelm@64817
   269
wenzelm@64817
   270
  def node_header: Document.Node.Header =
wenzelm@64817
   271
    PIDE.resources.special_header(node_name) getOrElse
wenzelm@64826
   272
      PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false)
wenzelm@64817
   273
wenzelm@64817
   274
wenzelm@64817
   275
  /* content */
wenzelm@64817
   276
wenzelm@64829
   277
  def node_position(offset: Text.Offset): Line.Node_Position =
wenzelm@64829
   278
    Line.Node_Position(node_name.node,
wenzelm@64829
   279
      Line.Position.zero.advance(content.text.substring(0, offset), Text.Length))
wenzelm@64829
   280
wenzelm@64817
   281
  def get_blob: Option[Document.Blob] =
wenzelm@64817
   282
    if (is_theory) None
wenzelm@64817
   283
    else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
wenzelm@64817
   284
wenzelm@64831
   285
  def bibtex_entries: List[Text.Info[String]] =
wenzelm@64828
   286
    if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil
wenzelm@64680
   287
wenzelm@64680
   288
wenzelm@64817
   289
  /* edits */
wenzelm@64817
   290
wenzelm@64817
   291
  def update_text(text: String): Option[File_Model] =
wenzelm@64817
   292
    Text.Edit.replace(0, content.text, text) match {
wenzelm@64817
   293
      case Nil => None
wenzelm@64817
   294
      case edits =>
wenzelm@64817
   295
        val content1 = Document_Model.File_Content(text)
wenzelm@64817
   296
        val pending_edits1 = pending_edits ::: edits
wenzelm@64817
   297
        Some(copy(content = content1, pending_edits = pending_edits1))
wenzelm@64817
   298
    }
wenzelm@38222
   299
wenzelm@64817
   300
  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
wenzelm@64817
   301
    : Option[(List[Document.Edit_Text], File_Model)] =
wenzelm@64817
   302
  {
wenzelm@64817
   303
    val (reparse, perspective) = node_perspective(doc_blobs, hidden)
wenzelm@64817
   304
    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
wenzelm@64827
   305
      val edits = node_edits(pending_edits, perspective)
wenzelm@64817
   306
      Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
wenzelm@64817
   307
    }
wenzelm@64817
   308
    else None
wenzelm@64817
   309
  }
wenzelm@64817
   310
wenzelm@64817
   311
wenzelm@64817
   312
  /* snapshot */
wenzelm@64817
   313
wenzelm@64817
   314
  def is_stable: Boolean = pending_edits.isEmpty
wenzelm@64818
   315
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
wenzelm@64817
   316
}
wenzelm@64817
   317
wenzelm@64817
   318
case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
wenzelm@64817
   319
  extends Document_Model
wenzelm@64817
   320
{
wenzelm@64817
   321
  /* header */
wenzelm@54509
   322
wenzelm@48707
   323
  def node_header(): Document.Node.Header =
wenzelm@46920
   324
  {
wenzelm@57612
   325
    GUI_Thread.require {}
wenzelm@54509
   326
wenzelm@64673
   327
    PIDE.resources.special_header(node_name) getOrElse
wenzelm@64826
   328
      JEdit_Lib.buffer_lock(buffer) {
wenzelm@64826
   329
        PIDE.resources.check_thy_reader(
wenzelm@64826
   330
          "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
wenzelm@46748
   331
      }
wenzelm@46920
   332
  }
wenzelm@44385
   333
wenzelm@44385
   334
wenzelm@44385
   335
  /* perspective */
wenzelm@44385
   336
wenzelm@57612
   337
  // owned by GUI thread
wenzelm@52816
   338
  private var _node_required = false
wenzelm@52816
   339
  def node_required: Boolean = _node_required
wenzelm@64817
   340
  def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }
wenzelm@52808
   341
wenzelm@64817
   342
  override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
wenzelm@44385
   343
  {
wenzelm@57612
   344
    GUI_Thread.require {}
wenzelm@52759
   345
wenzelm@64817
   346
    (for {
wenzelm@64817
   347
      doc_view <- PIDE.document_views(buffer).iterator
wenzelm@64817
   348
      range <- doc_view.perspective(snapshot).ranges.iterator
wenzelm@64817
   349
    } yield range).toList
wenzelm@44385
   350
  }
wenzelm@44385
   351
wenzelm@44385
   352
wenzelm@54509
   353
  /* blob */
wenzelm@54509
   354
wenzelm@57612
   355
  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by GUI thread
wenzelm@54511
   356
wenzelm@57612
   357
  private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
wenzelm@54511
   358
wenzelm@64817
   359
  def get_blob: Option[Document.Blob] =
wenzelm@57612
   360
    GUI_Thread.require {
wenzelm@55783
   361
      if (is_theory) None
wenzelm@55783
   362
      else {
wenzelm@56473
   363
        val (bytes, chunk) =
wenzelm@55783
   364
          _blob match {
wenzelm@55783
   365
            case Some(x) => x
wenzelm@55783
   366
            case None =>
wenzelm@64835
   367
              val bytes = PIDE.resources.make_file_content(buffer)
wenzelm@56746
   368
              val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
wenzelm@56473
   369
              _blob = Some((bytes, chunk))
wenzelm@56473
   370
              (bytes, chunk)
wenzelm@55783
   371
          }
wenzelm@64818
   372
        val changed = pending_edits.nonEmpty
wenzelm@56473
   373
        Some(Document.Blob(bytes, chunk, changed))
wenzelm@54511
   374
      }
wenzelm@54511
   375
    }
wenzelm@54509
   376
wenzelm@54509
   377
wenzelm@58543
   378
  /* bibtex entries */
wenzelm@58543
   379
wenzelm@64831
   380
  private var _bibtex_entries: Option[List[Text.Info[String]]] = None  // owned by GUI thread
wenzelm@58543
   381
wenzelm@64817
   382
  private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
wenzelm@58543
   383
wenzelm@64831
   384
  def bibtex_entries: List[Text.Info[String]] =
wenzelm@58543
   385
    GUI_Thread.require {
wenzelm@64828
   386
      if (Bibtex.check_name(node_name)) {
wenzelm@64817
   387
        _bibtex_entries match {
wenzelm@58543
   388
          case Some(entries) => entries
wenzelm@58543
   389
          case None =>
wenzelm@64817
   390
            val text = JEdit_Lib.buffer_text(buffer)
wenzelm@64828
   391
            val entries =
wenzelm@64831
   392
              try { Bibtex.document_entries(text) }
wenzelm@64828
   393
              catch { case ERROR(msg) => Output.warning(msg); Nil }
wenzelm@64817
   394
            _bibtex_entries = Some(entries)
wenzelm@58543
   395
            entries
wenzelm@58543
   396
        }
wenzelm@58543
   397
      }
wenzelm@58543
   398
      else Nil
wenzelm@58543
   399
    }
wenzelm@58543
   400
wenzelm@58543
   401
wenzelm@50344
   402
  /* pending edits */
wenzelm@43648
   403
wenzelm@60272
   404
  private object pending_edits
wenzelm@38224
   405
  {
wenzelm@38425
   406
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@57615
   407
    private var last_perspective = Document.Node.no_perspective_text
wenzelm@44438
   408
wenzelm@64818
   409
    def nonEmpty: Boolean = synchronized { pending.nonEmpty }
wenzelm@64818
   410
    def get_edits: List[Text.Edit] = synchronized { pending.toList }
wenzelm@64817
   411
    def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
wenzelm@64817
   412
    def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
wenzelm@64817
   413
      synchronized { last_perspective = perspective }
wenzelm@38224
   414
wenzelm@64817
   415
    def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
wenzelm@61728
   416
      synchronized {
wenzelm@61728
   417
        GUI_Thread.require {}
wenzelm@60272
   418
wenzelm@64818
   419
        val edits = get_edits
wenzelm@64817
   420
        val (reparse, perspective) = node_perspective(doc_blobs, hidden)
wenzelm@64818
   421
        if (reparse || edits.nonEmpty || last_perspective != perspective) {
wenzelm@61728
   422
          pending.clear
wenzelm@61728
   423
          last_perspective = perspective
wenzelm@64818
   424
          node_edits(edits, perspective)
wenzelm@61728
   425
        }
wenzelm@61728
   426
        else Nil
wenzelm@43648
   427
      }
wenzelm@38224
   428
wenzelm@64818
   429
    def edit(edits: List[Text.Edit]): Unit = synchronized
wenzelm@38224
   430
    {
wenzelm@60272
   431
      GUI_Thread.require {}
wenzelm@60272
   432
wenzelm@54511
   433
      reset_blob()
wenzelm@64817
   434
      reset_bibtex_entries()
wenzelm@54511
   435
wenzelm@61538
   436
      for (doc_view <- PIDE.document_views(buffer))
wenzelm@61538
   437
        doc_view.rich_text_area.active_reset()
wenzelm@61538
   438
wenzelm@64818
   439
      pending ++= edits
wenzelm@54461
   440
      PIDE.editor.invoke()
wenzelm@44436
   441
    }
wenzelm@44436
   442
  }
wenzelm@44436
   443
wenzelm@64835
   444
  def is_stable: Boolean = !pending_edits.nonEmpty
wenzelm@64818
   445
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
wenzelm@60933
   446
wenzelm@64817
   447
  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
wenzelm@64817
   448
    pending_edits.flush_edits(doc_blobs, hidden)
wenzelm@34828
   449
wenzelm@34828
   450
wenzelm@34828
   451
  /* buffer listener */
wenzelm@34828
   452
wenzelm@34828
   453
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   454
  {
wenzelm@34828
   455
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   456
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   457
    {
wenzelm@64818
   458
      pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
wenzelm@34828
   459
    }
wenzelm@34828
   460
wenzelm@34828
   461
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   462
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   463
    {
wenzelm@64818
   464
      pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
wenzelm@34828
   465
    }
wenzelm@34828
   466
  }
wenzelm@34828
   467
wenzelm@34828
   468
wenzelm@59078
   469
  /* syntax */
wenzelm@37557
   470
wenzelm@59078
   471
  def syntax_changed()
wenzelm@59078
   472
  {
wenzelm@61192
   473
    JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
wenzelm@59080
   474
    for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
wenzelm@59080
   475
      Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
wenzelm@59080
   476
        invoke(text_area)
wenzelm@62246
   477
    buffer.invalidateCachedFoldLevels
wenzelm@59078
   478
  }
wenzelm@59078
   479
wenzelm@64817
   480
  def init_token_marker()
wenzelm@59077
   481
  {
wenzelm@59077
   482
    Isabelle.buffer_token_marker(buffer) match {
wenzelm@59077
   483
      case Some(marker) if marker != buffer.getTokenMarker =>
wenzelm@59077
   484
        buffer.setTokenMarker(marker)
wenzelm@59078
   485
        syntax_changed()
wenzelm@59077
   486
      case _ =>
wenzelm@59077
   487
    }
wenzelm@59077
   488
  }
wenzelm@59077
   489
wenzelm@59078
   490
wenzelm@64817
   491
  /* init */
wenzelm@64817
   492
wenzelm@64817
   493
  def init(old_model: Option[File_Model]): Buffer_Model =
wenzelm@64817
   494
  {
wenzelm@64817
   495
    GUI_Thread.require {}
wenzelm@59078
   496
wenzelm@64817
   497
    old_model match {
wenzelm@64817
   498
      case None =>
wenzelm@64818
   499
        pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
wenzelm@64817
   500
      case Some(file_model) =>
wenzelm@64817
   501
        set_node_required(file_model.node_required)
wenzelm@64817
   502
        pending_edits.set_last_perspective(file_model.last_perspective)
wenzelm@64818
   503
        pending_edits.edit(
wenzelm@64818
   504
          file_model.pending_edits :::
wenzelm@64818
   505
            Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
wenzelm@64817
   506
    }
wenzelm@64817
   507
wenzelm@34784
   508
    buffer.addBufferListener(buffer_listener)
wenzelm@59078
   509
    init_token_marker()
wenzelm@64817
   510
wenzelm@64817
   511
    this
immler@34680
   512
  }
immler@34680
   513
wenzelm@64817
   514
wenzelm@64817
   515
  /* exit */
wenzelm@64817
   516
wenzelm@64817
   517
  def exit(): File_Model =
immler@34680
   518
  {
wenzelm@64817
   519
    GUI_Thread.require {}
wenzelm@64817
   520
wenzelm@34784
   521
    buffer.removeBufferListener(buffer_listener)
wenzelm@59078
   522
    init_token_marker()
wenzelm@64817
   523
wenzelm@64817
   524
    val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer))
wenzelm@64817
   525
    File_Model(session, node_name, content, node_required,
wenzelm@64818
   526
      pending_edits.get_last_perspective, pending_edits.get_edits)
immler@34680
   527
  }
wenzelm@34447
   528
}