src/Tools/jEdit/src/document_model.scala
author wenzelm
Mon Jun 05 23:55:58 2017 +0200 (2017-06-05)
changeset 66019 69b5ef78fb07
parent 65469 78ace4a14975
child 66036 b6396880b644
permissions -rw-r--r--
HTML preview via builtin HTTP server;
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@64858
    14
import java.io.{File => JFile}
wenzelm@64858
    15
wenzelm@34693
    16
import scala.collection.mutable
wenzelm@66019
    17
import scala.annotation.tailrec
wenzelm@34446
    18
wenzelm@64817
    19
import org.gjt.sp.jedit.{jEdit, View}
wenzelm@34784
    20
import org.gjt.sp.jedit.Buffer
wenzelm@61192
    21
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
wenzelm@34318
    22
wenzelm@34760
    23
wenzelm@34784
    24
object Document_Model
wenzelm@34588
    25
{
wenzelm@64817
    26
  /* document models */
wenzelm@64817
    27
wenzelm@64817
    28
  sealed case class State(
wenzelm@64817
    29
    models: Map[Document.Node.Name, Document_Model] = Map.empty,
wenzelm@64817
    30
    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty)
wenzelm@64817
    31
  {
wenzelm@64868
    32
    def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
wenzelm@64817
    33
      for {
wenzelm@64868
    34
        (node_name, model) <- models.iterator
wenzelm@64817
    35
        if model.isInstanceOf[File_Model]
wenzelm@64868
    36
      } yield (node_name, model.asInstanceOf[File_Model])
wenzelm@64813
    37
wenzelm@64817
    38
    def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
wenzelm@64817
    39
      : (Buffer_Model, State) =
wenzelm@64817
    40
    {
wenzelm@64817
    41
      val old_model =
wenzelm@64817
    42
        models.get(node_name) match {
wenzelm@64817
    43
          case Some(file_model: File_Model) => Some(file_model)
wenzelm@64817
    44
          case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
wenzelm@64817
    45
          case _ => None
wenzelm@64817
    46
        }
wenzelm@64817
    47
      val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
wenzelm@64817
    48
      (buffer_model,
wenzelm@64817
    49
        copy(models = models + (node_name -> buffer_model),
wenzelm@64817
    50
          buffer_models = buffer_models + (buffer -> buffer_model)))
wenzelm@64817
    51
    }
wenzelm@64817
    52
wenzelm@64817
    53
    def close_buffer(buffer: JEditBuffer): State =
wenzelm@64817
    54
    {
wenzelm@64817
    55
      buffer_models.get(buffer) match {
wenzelm@64817
    56
        case None => this
wenzelm@64817
    57
        case Some(buffer_model) =>
wenzelm@64817
    58
          val file_model = buffer_model.exit()
wenzelm@64817
    59
          copy(models = models + (file_model.node_name -> file_model),
wenzelm@64817
    60
            buffer_models = buffer_models - buffer)
wenzelm@64817
    61
      }
wenzelm@64817
    62
    }
wenzelm@64835
    63
wenzelm@64835
    64
    def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
wenzelm@64835
    65
      if (models.isDefinedAt(node_name)) this
wenzelm@64835
    66
      else {
wenzelm@64835
    67
        val edit = Text.Edit.insert(0, text)
wenzelm@64863
    68
        val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
wenzelm@64835
    69
        copy(models = models + (node_name -> model))
wenzelm@64835
    70
      }
wenzelm@64817
    71
  }
wenzelm@34784
    72
wenzelm@64817
    73
  private val state = Synchronized(State())  // owned by GUI thread
wenzelm@64817
    74
wenzelm@64835
    75
  def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
wenzelm@64835
    76
  def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name)
wenzelm@64835
    77
  def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
wenzelm@64817
    78
wenzelm@64831
    79
  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
wenzelm@64829
    80
    for {
wenzelm@64868
    81
      (_, model) <- state.value.models.iterator
wenzelm@65132
    82
      info <- model.bibtex_entries.iterator
wenzelm@65132
    83
    } yield info.map((_, model))
wenzelm@64829
    84
wenzelm@64817
    85
wenzelm@64858
    86
  /* sync external files */
wenzelm@64858
    87
wenzelm@64858
    88
  def sync_files(changed_files: Set[JFile]): Boolean =
wenzelm@64858
    89
  {
wenzelm@64858
    90
    state.change_result(st =>
wenzelm@64858
    91
      {
wenzelm@64858
    92
        val changed_models =
wenzelm@64858
    93
          (for {
wenzelm@64868
    94
            (node_name, model) <- st.file_models_iterator
wenzelm@64864
    95
            file <- model.file if changed_files(file)
wenzelm@64868
    96
            text <- PIDE.resources.read_file_content(node_name)
wenzelm@64858
    97
            if model.content.text != text
wenzelm@64858
    98
          } yield {
wenzelm@64858
    99
            val content = Document_Model.File_Content(text)
wenzelm@64858
   100
            val edits = Text.Edit.replace(0, model.content.text, text)
wenzelm@64868
   101
            (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
wenzelm@64858
   102
          }).toList
wenzelm@64858
   103
        if (changed_models.isEmpty) (false, st)
wenzelm@64858
   104
        else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
wenzelm@64858
   105
      })
wenzelm@64858
   106
  }
wenzelm@64858
   107
wenzelm@64858
   108
wenzelm@64836
   109
  /* syntax */
wenzelm@64836
   110
wenzelm@64836
   111
  def syntax_changed(names: List[Document.Node.Name])
wenzelm@64836
   112
  {
wenzelm@64836
   113
    GUI_Thread.require {}
wenzelm@64836
   114
wenzelm@64836
   115
    val models = state.value.models
wenzelm@64836
   116
    for (name <- names.iterator; model <- models.get(name)) {
wenzelm@64836
   117
      model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
wenzelm@64836
   118
    }
wenzelm@64836
   119
  }
wenzelm@64836
   120
wenzelm@64836
   121
wenzelm@64817
   122
  /* init and exit */
wenzelm@64817
   123
wenzelm@64817
   124
  def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
wenzelm@64817
   125
  {
wenzelm@64817
   126
    GUI_Thread.require {}
wenzelm@64817
   127
    state.change_result(st =>
wenzelm@64817
   128
      st.buffer_models.get(buffer) match {
wenzelm@64817
   129
        case Some(buffer_model) if buffer_model.node_name == node_name =>
wenzelm@64817
   130
          buffer_model.init_token_marker
wenzelm@64817
   131
          (buffer_model, st)
wenzelm@64817
   132
        case _ =>
wenzelm@64817
   133
          val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
wenzelm@64817
   134
          buffer.propertiesChanged
wenzelm@64817
   135
          res
wenzelm@64817
   136
      })
wenzelm@64817
   137
  }
wenzelm@64817
   138
wenzelm@34784
   139
  def exit(buffer: Buffer)
wenzelm@34784
   140
  {
wenzelm@57612
   141
    GUI_Thread.require {}
wenzelm@64813
   142
    state.change(st =>
wenzelm@64817
   143
      if (st.buffer_models.isDefinedAt(buffer)) {
wenzelm@64817
   144
        val res = st.close_buffer(buffer)
wenzelm@64817
   145
        buffer.propertiesChanged
wenzelm@64817
   146
        res
wenzelm@64817
   147
      }
wenzelm@64817
   148
      else st)
wenzelm@64817
   149
  }
wenzelm@64817
   150
wenzelm@64835
   151
  def provide_files(session: Session, files: List[(Document.Node.Name, String)])
wenzelm@64835
   152
  {
wenzelm@64835
   153
    GUI_Thread.require {}
wenzelm@64835
   154
    state.change(st =>
wenzelm@64835
   155
      (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) })
wenzelm@64835
   156
  }
wenzelm@64835
   157
wenzelm@64817
   158
wenzelm@64817
   159
  /* required nodes */
wenzelm@64817
   160
wenzelm@64817
   161
  def required_nodes(): Set[Document.Node.Name] =
wenzelm@64817
   162
    (for {
wenzelm@64868
   163
      (node_name, model) <- state.value.models.iterator
wenzelm@64817
   164
      if model.node_required
wenzelm@64868
   165
    } yield node_name).toSet
wenzelm@64817
   166
wenzelm@64817
   167
  def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false)
wenzelm@64817
   168
  {
wenzelm@64817
   169
    GUI_Thread.require {}
wenzelm@64817
   170
wenzelm@64817
   171
    val changed =
wenzelm@64817
   172
      state.change_result(st =>
wenzelm@64817
   173
        st.models.get(name) match {
wenzelm@64817
   174
          case None => (false, st)
wenzelm@64817
   175
          case Some(model) =>
wenzelm@64817
   176
            val required = if (toggle) !model.node_required else set
wenzelm@64817
   177
            model match {
wenzelm@64817
   178
              case model1: File_Model if required != model1.node_required =>
wenzelm@64817
   179
                (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
wenzelm@64817
   180
              case model1: Buffer_Model if required != model1.node_required =>
wenzelm@64817
   181
                model1.set_node_required(required); (true, st)
wenzelm@64817
   182
              case _ => (false, st)
wenzelm@64817
   183
            }
wenzelm@64817
   184
        })
wenzelm@64817
   185
    if (changed) {
wenzelm@65243
   186
      PIDE.plugin.options_changed()
wenzelm@65246
   187
      JEdit_Editor.flush()
wenzelm@64817
   188
    }
wenzelm@64817
   189
  }
wenzelm@64817
   190
wenzelm@64817
   191
  def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
wenzelm@64817
   192
    Document_Model.get(view.getBuffer).foreach(model =>
wenzelm@64817
   193
      node_required(model.node_name, toggle = toggle, set = set))
wenzelm@64817
   194
wenzelm@64817
   195
wenzelm@64817
   196
  /* flushed edits */
wenzelm@64817
   197
wenzelm@64867
   198
  def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
wenzelm@64817
   199
  {
wenzelm@64817
   200
    GUI_Thread.require {}
wenzelm@64817
   201
wenzelm@64817
   202
    state.change_result(st =>
wenzelm@64817
   203
      {
wenzelm@64817
   204
        val doc_blobs =
wenzelm@64817
   205
          Document.Blobs(
wenzelm@64817
   206
            (for {
wenzelm@64868
   207
              (node_name, model) <- st.models.iterator
wenzelm@64817
   208
              blob <- model.get_blob
wenzelm@64868
   209
            } yield (node_name -> blob)).toMap)
wenzelm@64817
   210
wenzelm@64817
   211
        val buffer_edits =
wenzelm@64817
   212
          (for {
wenzelm@64868
   213
            (_, model) <- st.buffer_models.iterator
wenzelm@64817
   214
            edit <- model.flush_edits(doc_blobs, hidden).iterator
wenzelm@64817
   215
          } yield edit).toList
wenzelm@64817
   216
wenzelm@64817
   217
        val file_edits =
wenzelm@64817
   218
          (for {
wenzelm@64868
   219
            (node_name, model) <- st.file_models_iterator
wenzelm@64867
   220
            (edits, model1) <- model.flush_edits(doc_blobs, hidden)
wenzelm@64868
   221
          } yield (edits, node_name -> model1)).toList
wenzelm@64867
   222
wenzelm@64867
   223
        val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
wenzelm@64867
   224
wenzelm@64867
   225
        val purge_edits =
wenzelm@64867
   226
          if (purge) {
wenzelm@64867
   227
            val purged =
wenzelm@64868
   228
              (for ((node_name, model) <- st.file_models_iterator)
wenzelm@64868
   229
               yield (node_name -> model.purge_edits(doc_blobs))).toList
wenzelm@64817
   230
wenzelm@64867
   231
            val imports =
wenzelm@64867
   232
            {
wenzelm@64868
   233
              val open_nodes =
wenzelm@64868
   234
                (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
wenzelm@64867
   235
              val touched_nodes = model_edits.map(_._1)
wenzelm@64867
   236
              val pending_nodes = for ((node_name, None) <- purged) yield node_name
wenzelm@64867
   237
              (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
wenzelm@64867
   238
            }
wenzelm@65359
   239
            val retain = PIDE.resources.thy_info.dependencies(imports).deps.map(_.name).toSet
wenzelm@64817
   240
wenzelm@64867
   241
            for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
wenzelm@64867
   242
              yield edit
wenzelm@64867
   243
          }
wenzelm@64867
   244
          else Nil
wenzelm@64867
   245
wenzelm@64867
   246
        val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
wenzelm@65245
   247
        PIDE.plugin.file_watcher.purge(
wenzelm@64867
   248
          (for {
wenzelm@64868
   249
            (_, model) <- st1.file_models_iterator
wenzelm@64867
   250
            file <- model.file
wenzelm@64867
   251
          } yield file.getParentFile).toSet)
wenzelm@64867
   252
wenzelm@64867
   253
        ((doc_blobs, model_edits ::: purge_edits), st1)
wenzelm@64813
   254
      })
wenzelm@34318
   255
  }
wenzelm@43397
   256
wenzelm@64817
   257
wenzelm@64817
   258
  /* file content */
wenzelm@64817
   259
wenzelm@64817
   260
  sealed case class File_Content(text: String)
wenzelm@64817
   261
  {
wenzelm@64835
   262
    lazy val bytes: Bytes = Bytes(Symbol.encode(text))
wenzelm@64817
   263
    lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
wenzelm@64831
   264
    lazy val bibtex_entries: List[Text.Info[String]] =
wenzelm@64831
   265
      try { Bibtex.document_entries(text) }
wenzelm@64828
   266
      catch { case ERROR(msg) => Output.warning(msg); Nil }
wenzelm@64817
   267
  }
wenzelm@66019
   268
wenzelm@66019
   269
wenzelm@66019
   270
  /* HTTP preview */
wenzelm@66019
   271
wenzelm@66019
   272
  def open_preview(view: View)
wenzelm@66019
   273
  {
wenzelm@66019
   274
    Document_Model.get(view.getBuffer) match {
wenzelm@66019
   275
      case Some(model) =>
wenzelm@66019
   276
        JEdit_Editor.hyperlink_url(
wenzelm@66019
   277
          PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview/" +
wenzelm@66019
   278
            model.node_name.theory).follow(view)
wenzelm@66019
   279
      case None =>
wenzelm@66019
   280
    }
wenzelm@66019
   281
  }
wenzelm@66019
   282
wenzelm@66019
   283
  def http_handlers(http_root: String): List[HTTP.Handler] =
wenzelm@66019
   284
  {
wenzelm@66019
   285
    val preview_root = http_root + "/preview"
wenzelm@66019
   286
    val preview =
wenzelm@66019
   287
      HTTP.get(preview_root, uri =>
wenzelm@66019
   288
        for {
wenzelm@66019
   289
          theory <- Library.try_unprefix(preview_root + "/", uri.toString)
wenzelm@66019
   290
          model <-
wenzelm@66019
   291
            get_models().iterator.collectFirst(
wenzelm@66019
   292
              { case (node_name, model) if node_name.theory == theory => model })
wenzelm@66019
   293
        }
wenzelm@66019
   294
        yield HTTP.Response.html(model.preview("../fonts")))
wenzelm@66019
   295
wenzelm@66019
   296
    List(HTTP.fonts(http_root + "/fonts"), preview)
wenzelm@66019
   297
  }
wenzelm@64817
   298
}
wenzelm@64817
   299
wenzelm@64829
   300
sealed abstract class Document_Model extends Document.Model
wenzelm@64817
   301
{
wenzelm@64817
   302
  /* content */
wenzelm@64817
   303
wenzelm@64831
   304
  def bibtex_entries: List[Text.Info[String]]
wenzelm@64817
   305
wenzelm@66019
   306
  def preview(fonts_dir: String): String =
wenzelm@66019
   307
  {
wenzelm@66019
   308
    val snapshot = await_stable_snapshot()
wenzelm@66019
   309
wenzelm@66019
   310
    HTML.output_document(
wenzelm@66019
   311
      List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))),
wenzelm@66019
   312
      List(
wenzelm@66019
   313
        HTML.chapter("Theory " + quote(node_name.theory_base_name)),
wenzelm@66019
   314
        HTML.source(snapshot.node.commands.iterator.map(_.source).mkString)),
wenzelm@66019
   315
      css = "")
wenzelm@66019
   316
  }
wenzelm@66019
   317
wenzelm@64817
   318
wenzelm@64817
   319
  /* perspective */
wenzelm@64817
   320
wenzelm@64817
   321
  def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
wenzelm@64817
   322
wenzelm@64817
   323
  def node_perspective(
wenzelm@64817
   324
    doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
wenzelm@43397
   325
  {
wenzelm@57612
   326
    GUI_Thread.require {}
wenzelm@64817
   327
wenzelm@64817
   328
    if (Isabelle.continuous_checking && is_theory) {
wenzelm@64817
   329
      val snapshot = this.snapshot()
wenzelm@64817
   330
wenzelm@64817
   331
      val reparse = snapshot.node.load_commands_changed(doc_blobs)
wenzelm@64817
   332
      val perspective =
wenzelm@64817
   333
        if (hidden) Text.Perspective.empty
wenzelm@64817
   334
        else {
wenzelm@64817
   335
          val view_ranges = document_view_ranges(snapshot)
wenzelm@65246
   336
          val load_ranges = snapshot.commands_loading_ranges(JEdit_Editor.visible_node(_))
wenzelm@64817
   337
          Text.Perspective(view_ranges ::: load_ranges)
wenzelm@64817
   338
        }
wenzelm@65246
   339
      val overlays = JEdit_Editor.node_overlays(node_name)
wenzelm@64817
   340
wenzelm@64817
   341
      (reparse, Document.Node.Perspective(node_required, perspective, overlays))
wenzelm@64817
   342
    }
wenzelm@64817
   343
    else (false, Document.Node.no_perspective_text)
wenzelm@43397
   344
  }
wenzelm@66019
   345
wenzelm@66019
   346
wenzelm@66019
   347
  /* snapshot */
wenzelm@66019
   348
wenzelm@66019
   349
  @tailrec final def await_stable_snapshot(): Document.Snapshot =
wenzelm@66019
   350
  {
wenzelm@66019
   351
    val snapshot = this.snapshot()
wenzelm@66019
   352
    if (snapshot.is_outdated) {
wenzelm@66019
   353
      Thread.sleep(PIDE.options.seconds("editor_output_delay").ms)
wenzelm@66019
   354
      await_stable_snapshot()
wenzelm@66019
   355
    }
wenzelm@66019
   356
    else snapshot
wenzelm@66019
   357
  }
wenzelm@34318
   358
}
wenzelm@34318
   359
wenzelm@64863
   360
object File_Model
wenzelm@64863
   361
{
wenzelm@64863
   362
  def init(session: Session,
wenzelm@64863
   363
    node_name: Document.Node.Name,
wenzelm@64863
   364
    text: String,
wenzelm@64863
   365
    node_required: Boolean = false,
wenzelm@64863
   366
    last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
wenzelm@64863
   367
    pending_edits: List[Text.Edit] = Nil): File_Model =
wenzelm@64863
   368
  {
wenzelm@65469
   369
    val file = JEdit_Lib.check_file(node_name.node)
wenzelm@65245
   370
    file.foreach(PIDE.plugin.file_watcher.register_parent(_))
wenzelm@64863
   371
wenzelm@64864
   372
    val content = Document_Model.File_Content(text)
wenzelm@64864
   373
    File_Model(session, node_name, file, content, node_required, last_perspective, pending_edits)
wenzelm@64863
   374
  }
wenzelm@64863
   375
}
wenzelm@64863
   376
wenzelm@64817
   377
case class File_Model(
wenzelm@64817
   378
  session: Session,
wenzelm@64817
   379
  node_name: Document.Node.Name,
wenzelm@64864
   380
  file: Option[JFile],
wenzelm@64817
   381
  content: Document_Model.File_Content,
wenzelm@64863
   382
  node_required: Boolean,
wenzelm@64863
   383
  last_perspective: Document.Node.Perspective_Text,
wenzelm@64863
   384
  pending_edits: List[Text.Edit]) extends Document_Model
wenzelm@34588
   385
{
wenzelm@64817
   386
  /* header */
wenzelm@64817
   387
wenzelm@64817
   388
  def node_header: Document.Node.Header =
wenzelm@64817
   389
    PIDE.resources.special_header(node_name) getOrElse
wenzelm@65359
   390
      PIDE.resources.check_thy_reader(node_name, Scan.char_reader(content.text), strict = false)
wenzelm@64817
   391
wenzelm@64817
   392
wenzelm@64817
   393
  /* content */
wenzelm@64817
   394
wenzelm@64829
   395
  def node_position(offset: Text.Offset): Line.Node_Position =
wenzelm@64829
   396
    Line.Node_Position(node_name.node,
wenzelm@65196
   397
      Line.Position.zero.advance(content.text.substring(0, offset)))
wenzelm@64829
   398
wenzelm@64817
   399
  def get_blob: Option[Document.Blob] =
wenzelm@64817
   400
    if (is_theory) None
wenzelm@64817
   401
    else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
wenzelm@64817
   402
wenzelm@64831
   403
  def bibtex_entries: List[Text.Info[String]] =
wenzelm@64828
   404
    if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil
wenzelm@64680
   405
wenzelm@64680
   406
wenzelm@64817
   407
  /* edits */
wenzelm@64817
   408
wenzelm@64817
   409
  def update_text(text: String): Option[File_Model] =
wenzelm@64817
   410
    Text.Edit.replace(0, content.text, text) match {
wenzelm@64817
   411
      case Nil => None
wenzelm@64817
   412
      case edits =>
wenzelm@64817
   413
        val content1 = Document_Model.File_Content(text)
wenzelm@64817
   414
        val pending_edits1 = pending_edits ::: edits
wenzelm@64817
   415
        Some(copy(content = content1, pending_edits = pending_edits1))
wenzelm@64817
   416
    }
wenzelm@38222
   417
wenzelm@64817
   418
  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
wenzelm@64817
   419
    : Option[(List[Document.Edit_Text], File_Model)] =
wenzelm@64817
   420
  {
wenzelm@64817
   421
    val (reparse, perspective) = node_perspective(doc_blobs, hidden)
wenzelm@64817
   422
    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
wenzelm@64867
   423
      val edits = node_edits(node_header, pending_edits, perspective)
wenzelm@64817
   424
      Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
wenzelm@64817
   425
    }
wenzelm@64817
   426
    else None
wenzelm@64817
   427
  }
wenzelm@64817
   428
wenzelm@64867
   429
  def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
wenzelm@64867
   430
    if (node_required || !Document.Node.is_no_perspective_text(last_perspective) ||
wenzelm@64867
   431
        pending_edits.nonEmpty) None
wenzelm@64867
   432
    else {
wenzelm@64867
   433
      val text_edits = List(Text.Edit.remove(0, content.text))
wenzelm@64867
   434
      Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
wenzelm@64867
   435
    }
wenzelm@64867
   436
wenzelm@64817
   437
wenzelm@64817
   438
  /* snapshot */
wenzelm@64817
   439
wenzelm@64817
   440
  def is_stable: Boolean = pending_edits.isEmpty
wenzelm@64818
   441
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
wenzelm@64817
   442
}
wenzelm@64817
   443
wenzelm@64817
   444
case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
wenzelm@64817
   445
  extends Document_Model
wenzelm@64817
   446
{
wenzelm@64817
   447
  /* header */
wenzelm@54509
   448
wenzelm@48707
   449
  def node_header(): Document.Node.Header =
wenzelm@46920
   450
  {
wenzelm@57612
   451
    GUI_Thread.require {}
wenzelm@54509
   452
wenzelm@64673
   453
    PIDE.resources.special_header(node_name) getOrElse
wenzelm@64826
   454
      JEdit_Lib.buffer_lock(buffer) {
wenzelm@65359
   455
        PIDE.resources.check_thy_reader(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
wenzelm@46748
   456
      }
wenzelm@46920
   457
  }
wenzelm@44385
   458
wenzelm@44385
   459
wenzelm@44385
   460
  /* perspective */
wenzelm@44385
   461
wenzelm@57612
   462
  // owned by GUI thread
wenzelm@52816
   463
  private var _node_required = false
wenzelm@52816
   464
  def node_required: Boolean = _node_required
wenzelm@64817
   465
  def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }
wenzelm@52808
   466
wenzelm@64883
   467
  def document_view_iterator: Iterator[Document_View] =
wenzelm@64883
   468
    for {
wenzelm@64883
   469
      text_area <- JEdit_Lib.jedit_text_areas(buffer)
wenzelm@64883
   470
      doc_view <- Document_View.get(text_area)
wenzelm@64883
   471
    } yield doc_view
wenzelm@64883
   472
wenzelm@64817
   473
  override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
wenzelm@44385
   474
  {
wenzelm@57612
   475
    GUI_Thread.require {}
wenzelm@52759
   476
wenzelm@64817
   477
    (for {
wenzelm@64883
   478
      doc_view <- document_view_iterator
wenzelm@64817
   479
      range <- doc_view.perspective(snapshot).ranges.iterator
wenzelm@64817
   480
    } yield range).toList
wenzelm@44385
   481
  }
wenzelm@44385
   482
wenzelm@44385
   483
wenzelm@54509
   484
  /* blob */
wenzelm@54509
   485
wenzelm@64885
   486
  // owned by GUI thread
wenzelm@64885
   487
  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None
wenzelm@54511
   488
wenzelm@57612
   489
  private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
wenzelm@54511
   490
wenzelm@64817
   491
  def get_blob: Option[Document.Blob] =
wenzelm@57612
   492
    GUI_Thread.require {
wenzelm@55783
   493
      if (is_theory) None
wenzelm@55783
   494
      else {
wenzelm@56473
   495
        val (bytes, chunk) =
wenzelm@55783
   496
          _blob match {
wenzelm@55783
   497
            case Some(x) => x
wenzelm@55783
   498
            case None =>
wenzelm@64835
   499
              val bytes = PIDE.resources.make_file_content(buffer)
wenzelm@56746
   500
              val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
wenzelm@56473
   501
              _blob = Some((bytes, chunk))
wenzelm@56473
   502
              (bytes, chunk)
wenzelm@55783
   503
          }
wenzelm@64818
   504
        val changed = pending_edits.nonEmpty
wenzelm@56473
   505
        Some(Document.Blob(bytes, chunk, changed))
wenzelm@54511
   506
      }
wenzelm@54511
   507
    }
wenzelm@54509
   508
wenzelm@54509
   509
wenzelm@58543
   510
  /* bibtex entries */
wenzelm@58543
   511
wenzelm@64885
   512
  // owned by GUI thread
wenzelm@64885
   513
  private var _bibtex_entries: Option[List[Text.Info[String]]] = None
wenzelm@58543
   514
wenzelm@64817
   515
  private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
wenzelm@58543
   516
wenzelm@64831
   517
  def bibtex_entries: List[Text.Info[String]] =
wenzelm@58543
   518
    GUI_Thread.require {
wenzelm@64828
   519
      if (Bibtex.check_name(node_name)) {
wenzelm@64817
   520
        _bibtex_entries match {
wenzelm@58543
   521
          case Some(entries) => entries
wenzelm@58543
   522
          case None =>
wenzelm@64817
   523
            val text = JEdit_Lib.buffer_text(buffer)
wenzelm@64828
   524
            val entries =
wenzelm@64831
   525
              try { Bibtex.document_entries(text) }
wenzelm@64828
   526
              catch { case ERROR(msg) => Output.warning(msg); Nil }
wenzelm@64817
   527
            _bibtex_entries = Some(entries)
wenzelm@58543
   528
            entries
wenzelm@58543
   529
        }
wenzelm@58543
   530
      }
wenzelm@58543
   531
      else Nil
wenzelm@58543
   532
    }
wenzelm@58543
   533
wenzelm@58543
   534
wenzelm@50344
   535
  /* pending edits */
wenzelm@43648
   536
wenzelm@60272
   537
  private object pending_edits
wenzelm@38224
   538
  {
wenzelm@38425
   539
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@57615
   540
    private var last_perspective = Document.Node.no_perspective_text
wenzelm@44438
   541
wenzelm@64818
   542
    def nonEmpty: Boolean = synchronized { pending.nonEmpty }
wenzelm@64818
   543
    def get_edits: List[Text.Edit] = synchronized { pending.toList }
wenzelm@64817
   544
    def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
wenzelm@64817
   545
    def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
wenzelm@64817
   546
      synchronized { last_perspective = perspective }
wenzelm@38224
   547
wenzelm@64817
   548
    def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
wenzelm@61728
   549
      synchronized {
wenzelm@61728
   550
        GUI_Thread.require {}
wenzelm@60272
   551
wenzelm@64818
   552
        val edits = get_edits
wenzelm@64817
   553
        val (reparse, perspective) = node_perspective(doc_blobs, hidden)
wenzelm@64818
   554
        if (reparse || edits.nonEmpty || last_perspective != perspective) {
wenzelm@61728
   555
          pending.clear
wenzelm@61728
   556
          last_perspective = perspective
wenzelm@64867
   557
          node_edits(node_header, edits, perspective)
wenzelm@61728
   558
        }
wenzelm@61728
   559
        else Nil
wenzelm@43648
   560
      }
wenzelm@38224
   561
wenzelm@64818
   562
    def edit(edits: List[Text.Edit]): Unit = synchronized
wenzelm@38224
   563
    {
wenzelm@60272
   564
      GUI_Thread.require {}
wenzelm@60272
   565
wenzelm@54511
   566
      reset_blob()
wenzelm@64817
   567
      reset_bibtex_entries()
wenzelm@54511
   568
wenzelm@64883
   569
      for (doc_view <- document_view_iterator)
wenzelm@61538
   570
        doc_view.rich_text_area.active_reset()
wenzelm@61538
   571
wenzelm@64818
   572
      pending ++= edits
wenzelm@65246
   573
      JEdit_Editor.invoke()
wenzelm@44436
   574
    }
wenzelm@44436
   575
  }
wenzelm@44436
   576
wenzelm@64835
   577
  def is_stable: Boolean = !pending_edits.nonEmpty
wenzelm@64818
   578
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
wenzelm@60933
   579
wenzelm@64817
   580
  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
wenzelm@64817
   581
    pending_edits.flush_edits(doc_blobs, hidden)
wenzelm@34828
   582
wenzelm@34828
   583
wenzelm@34828
   584
  /* buffer listener */
wenzelm@34828
   585
wenzelm@34828
   586
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   587
  {
wenzelm@34828
   588
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   589
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   590
    {
wenzelm@64818
   591
      pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
wenzelm@34828
   592
    }
wenzelm@34828
   593
wenzelm@34828
   594
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   595
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   596
    {
wenzelm@64818
   597
      pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
wenzelm@34828
   598
    }
wenzelm@34828
   599
  }
wenzelm@34828
   600
wenzelm@34828
   601
wenzelm@59078
   602
  /* syntax */
wenzelm@37557
   603
wenzelm@59078
   604
  def syntax_changed()
wenzelm@59078
   605
  {
wenzelm@61192
   606
    JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
wenzelm@59080
   607
    for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
wenzelm@59080
   608
      Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
wenzelm@59080
   609
        invoke(text_area)
wenzelm@62246
   610
    buffer.invalidateCachedFoldLevels
wenzelm@59078
   611
  }
wenzelm@59078
   612
wenzelm@64817
   613
  def init_token_marker()
wenzelm@59077
   614
  {
wenzelm@59077
   615
    Isabelle.buffer_token_marker(buffer) match {
wenzelm@59077
   616
      case Some(marker) if marker != buffer.getTokenMarker =>
wenzelm@59077
   617
        buffer.setTokenMarker(marker)
wenzelm@59078
   618
        syntax_changed()
wenzelm@59077
   619
      case _ =>
wenzelm@59077
   620
    }
wenzelm@59077
   621
  }
wenzelm@59077
   622
wenzelm@59078
   623
wenzelm@64817
   624
  /* init */
wenzelm@64817
   625
wenzelm@64817
   626
  def init(old_model: Option[File_Model]): Buffer_Model =
wenzelm@64817
   627
  {
wenzelm@64817
   628
    GUI_Thread.require {}
wenzelm@59078
   629
wenzelm@64817
   630
    old_model match {
wenzelm@64817
   631
      case None =>
wenzelm@64818
   632
        pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
wenzelm@64817
   633
      case Some(file_model) =>
wenzelm@64817
   634
        set_node_required(file_model.node_required)
wenzelm@64817
   635
        pending_edits.set_last_perspective(file_model.last_perspective)
wenzelm@64818
   636
        pending_edits.edit(
wenzelm@64818
   637
          file_model.pending_edits :::
wenzelm@64818
   638
            Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
wenzelm@64817
   639
    }
wenzelm@64817
   640
wenzelm@34784
   641
    buffer.addBufferListener(buffer_listener)
wenzelm@59078
   642
    init_token_marker()
wenzelm@64817
   643
wenzelm@64817
   644
    this
immler@34680
   645
  }
immler@34680
   646
wenzelm@64817
   647
wenzelm@64817
   648
  /* exit */
wenzelm@64817
   649
wenzelm@64817
   650
  def exit(): File_Model =
immler@34680
   651
  {
wenzelm@64817
   652
    GUI_Thread.require {}
wenzelm@64817
   653
wenzelm@34784
   654
    buffer.removeBufferListener(buffer_listener)
wenzelm@59078
   655
    init_token_marker()
wenzelm@64817
   656
wenzelm@64863
   657
    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
wenzelm@64863
   658
      pending_edits.get_last_perspective, pending_edits.get_edits)
immler@34680
   659
  }
wenzelm@34447
   660
}