src/Tools/jEdit/src/document_model.scala
author wenzelm
Wed, 31 Mar 2021 12:02:52 +0200
changeset 73774 c42144d9dde6
parent 73665 56c0a793cd8b
child 73959 7202e12cb324
permissions -rw-r--r--
more uniform HTTP resources;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 40851
diff changeset
     1
/*  Title:      Tools/jEdit/src/document_model.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     2
    Author:     Fabian Immler, TU Munich
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     3
    Author:     Makarius
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     4
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
     5
Document model connected to jEdit buffer or external file: content of theory
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
     6
node or auxiliary file (blob).
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     7
*/
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     8
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
     9
package isabelle.jedit
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    10
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    11
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    12
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    13
64858
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
    14
import java.io.{File => JFile}
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
    15
34693
3e995f100ad2 sealed Edit;
wenzelm
parents: 34685
diff changeset
    16
import scala.collection.mutable
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
    17
import scala.annotation.tailrec
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    18
73200
wenzelm
parents: 73199
diff changeset
    19
import org.gjt.sp.jedit.View
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    20
import org.gjt.sp.jedit.Buffer
61192
98eba31c51f8 tuned signature;
wenzelm
parents: 60933
diff changeset
    21
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    22
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    23
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    24
object Document_Model
34588
e8ac8794971f superficial tuning;
wenzelm
parents: 34583
diff changeset
    25
{
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    26
  /* document models */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    27
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    28
  sealed case class State(
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    29
    models: Map[Document.Node.Name, Document_Model] = Map.empty,
66101
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
    30
    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
    31
    overlays: Document.Overlays = Document.Overlays.empty)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    32
  {
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
    33
    def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    34
      for {
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
    35
        (node_name, model) <- models.iterator
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    36
        if model.isInstanceOf[File_Model]
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
    37
      } yield (node_name, model.asInstanceOf[File_Model])
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
    38
68477
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
    39
    def document_blobs: Document.Blobs =
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
    40
      Document.Blobs(
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
    41
        (for {
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
    42
          (node_name, model) <- models.iterator
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
    43
          blob <- model.get_blob
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
    44
        } yield (node_name -> blob)).toMap)
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
    45
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    46
    def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    47
      : (Buffer_Model, State) =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    48
    {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    49
      val old_model =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    50
        models.get(node_name) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    51
          case Some(file_model: File_Model) => Some(file_model)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    52
          case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    53
          case _ => None
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    54
        }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    55
      val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    56
      (buffer_model,
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    57
        copy(models = models + (node_name -> buffer_model),
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    58
          buffer_models = buffer_models + (buffer -> buffer_model)))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    59
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    60
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    61
    def close_buffer(buffer: JEditBuffer): State =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    62
    {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    63
      buffer_models.get(buffer) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    64
        case None => this
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    65
        case Some(buffer_model) =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    66
          val file_model = buffer_model.exit()
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    67
          copy(models = models + (file_model.node_name -> file_model),
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    68
            buffer_models = buffer_models - buffer)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    69
      }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    70
    }
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
    71
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
    72
    def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
    73
      if (models.isDefinedAt(node_name)) this
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
    74
      else {
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
    75
        val edit = Text.Edit.insert(0, text)
64863
wenzelm
parents: 64858
diff changeset
    76
        val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
    77
        copy(models = models + (node_name -> model))
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
    78
      }
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    79
  }
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    80
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    81
  private val state = Synchronized(State())  // owned by GUI thread
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    82
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
    83
  def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69260
diff changeset
    84
  def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
    85
  def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    86
68477
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
    87
  def document_blobs(): Document.Blobs = state.value.document_blobs
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
    88
66152
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
    89
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
    90
  /* bibtex */
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
    91
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
    92
  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66114
diff changeset
    93
    Bibtex.entries_iterator(state.value.models)
64829
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
    94
66152
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
    95
  def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
    96
      : Option[Completion.Result] =
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
    97
    Bibtex.completion(history, rendering, caret, state.value.models)
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
    98
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    99
66101
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   100
  /* overlays */
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   101
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   102
  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   103
    state.value.overlays(name)
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   104
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   105
  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   106
    state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args)))
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   107
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   108
  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   109
    state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   110
0f0f294e314f maintain overlays within main state of document models;
wenzelm
parents: 66082
diff changeset
   111
64858
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   112
  /* sync external files */
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   113
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   114
  def sync_files(changed_files: Set[JFile]): Boolean =
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   115
  {
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   116
    state.change_result(st =>
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   117
      {
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   118
        val changed_models =
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   119
          (for {
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   120
            (node_name, model) <- st.file_models_iterator
64864
eec7ffef0be6 accomodate very big file_models and changed_files;
wenzelm
parents: 64863
diff changeset
   121
            file <- model.file if changed_files(file)
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   122
            text <- PIDE.resources.read_file_content(node_name)
64858
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   123
            if model.content.text != text
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   124
          } yield {
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   125
            val content = Document_Model.File_Content(text)
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   126
            val edits = Text.Edit.replace(0, model.content.text, text)
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   127
            (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
64858
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   128
          }).toList
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   129
        if (changed_models.isEmpty) (false, st)
73605
78aa7846e91f tuned --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   130
        else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
64858
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   131
      })
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   132
  }
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   133
e31cf6eaecb8 update File_Model based on file-system events;
wenzelm
parents: 64836
diff changeset
   134
64836
wenzelm
parents: 64835
diff changeset
   135
  /* syntax */
wenzelm
parents: 64835
diff changeset
   136
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   137
  def syntax_changed(names: List[Document.Node.Name]): Unit =
64836
wenzelm
parents: 64835
diff changeset
   138
  {
wenzelm
parents: 64835
diff changeset
   139
    GUI_Thread.require {}
wenzelm
parents: 64835
diff changeset
   140
wenzelm
parents: 64835
diff changeset
   141
    val models = state.value.models
wenzelm
parents: 64835
diff changeset
   142
    for (name <- names.iterator; model <- models.get(name)) {
wenzelm
parents: 64835
diff changeset
   143
      model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
wenzelm
parents: 64835
diff changeset
   144
    }
wenzelm
parents: 64835
diff changeset
   145
  }
wenzelm
parents: 64835
diff changeset
   146
wenzelm
parents: 64835
diff changeset
   147
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   148
  /* init and exit */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   149
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   150
  def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   151
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   152
    GUI_Thread.require {}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   153
    state.change_result(st =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   154
      st.buffer_models.get(buffer) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   155
        case Some(buffer_model) if buffer_model.node_name == node_name =>
73200
wenzelm
parents: 73199
diff changeset
   156
          buffer_model.init_token_marker()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   157
          (buffer_model, st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   158
        case _ =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   159
          val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
73200
wenzelm
parents: 73199
diff changeset
   160
          buffer.propertiesChanged()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   161
          res
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   162
      })
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   163
  }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   164
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   165
  def exit(buffer: Buffer): Unit =
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   166
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   167
    GUI_Thread.require {}
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
   168
    state.change(st =>
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   169
      if (st.buffer_models.isDefinedAt(buffer)) {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   170
        val res = st.close_buffer(buffer)
73200
wenzelm
parents: 73199
diff changeset
   171
        buffer.propertiesChanged()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   172
        res
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   173
      }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   174
      else st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   175
  }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   176
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   177
  def provide_files(session: Session, files: List[(Document.Node.Name, String)]): Unit =
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
   178
  {
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
   179
    GUI_Thread.require {}
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
   180
    state.change(st =>
73605
78aa7846e91f tuned --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   181
      files.foldLeft(st) {
78aa7846e91f tuned --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   182
        case (st1, (node_name, text)) => st1.provide_file(session, node_name, text)
78aa7846e91f tuned --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   183
      })
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
   184
  }
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
   185
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   186
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   187
  /* required nodes */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   188
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   189
  def required_nodes(): Set[Document.Node.Name] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   190
    (for {
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   191
      (node_name, model) <- state.value.models.iterator
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   192
      if model.node_required
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   193
    } yield node_name).toSet
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   194
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   195
  def node_required(
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   196
    name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false): Unit =
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   197
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   198
    GUI_Thread.require {}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   199
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   200
    val changed =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   201
      state.change_result(st =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   202
        st.models.get(name) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   203
          case None => (false, st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   204
          case Some(model) =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   205
            val required = if (toggle) !model.node_required else set
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   206
            model match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   207
              case model1: File_Model if required != model1.node_required =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   208
                (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   209
              case model1: Buffer_Model if required != model1.node_required =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   210
                model1.set_node_required(required); (true, st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   211
              case _ => (false, st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   212
            }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   213
        })
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   214
    if (changed) {
65243
ba5ce07e06a7 proper plugin access;
wenzelm
parents: 65196
diff changeset
   215
      PIDE.plugin.options_changed()
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66040
diff changeset
   216
      PIDE.editor.flush()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   217
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   218
  }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   219
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   220
  def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   221
    Document_Model.get(view.getBuffer).foreach(model =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   222
      node_required(model.node_name, toggle = toggle, set = set))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   223
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   224
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   225
  /* flushed edits */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   226
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   227
  def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   228
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   229
    GUI_Thread.require {}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   230
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   231
    state.change_result(st =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   232
      {
68477
1be1b7620a42 tuned signature -- facilitate testing;
wenzelm
parents: 67934
diff changeset
   233
        val doc_blobs = st.document_blobs
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   234
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   235
        val buffer_edits =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   236
          (for {
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   237
            (_, model) <- st.buffer_models.iterator
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   238
            edit <- model.flush_edits(doc_blobs, hidden).iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   239
          } yield edit).toList
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   240
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   241
        val file_edits =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   242
          (for {
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   243
            (node_name, model) <- st.file_models_iterator
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   244
            (edits, model1) <- model.flush_edits(doc_blobs, hidden)
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   245
          } yield (edits, node_name -> model1)).toList
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   246
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   247
        val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   248
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   249
        val purge_edits =
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   250
          if (purge) {
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   251
            val purged =
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   252
              (for ((node_name, model) <- st.file_models_iterator)
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   253
               yield (node_name -> model.purge_edits(doc_blobs))).toList
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   254
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   255
            val imports =
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   256
            {
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   257
              val open_nodes =
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   258
                (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   259
              val touched_nodes = model_edits.map(_._1)
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   260
              val pending_nodes = for ((node_name, None) <- purged) yield node_name
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   261
              (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   262
            }
67059
df7d728103f1 tuned signature;
wenzelm
parents: 67014
diff changeset
   263
            val retain = PIDE.resources.dependencies(imports).theories.toSet
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   264
67934
wenzelm
parents: 67310
diff changeset
   265
            for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   266
              yield edit
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   267
          }
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   268
          else Nil
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   269
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   270
        val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
65245
e955b33f432c proper plugin access;
wenzelm
parents: 65243
diff changeset
   271
        PIDE.plugin.file_watcher.purge(
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   272
          (for {
64868
6212d3c396b0 tuned signature;
wenzelm
parents: 64867
diff changeset
   273
            (_, model) <- st1.file_models_iterator
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   274
            file <- model.file
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   275
          } yield file.getParentFile).toSet)
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   276
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   277
        ((doc_blobs, model_edits ::: purge_edits), st1)
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
   278
      })
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   279
  }
43397
dba359c0ae3b more robust init;
wenzelm
parents: 43394
diff changeset
   280
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   281
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   282
  /* file content */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   283
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   284
  sealed case class File_Content(text: String)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   285
  {
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
   286
    lazy val bytes: Bytes = Bytes(Symbol.encode(text))
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   287
    lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   288
    lazy val bibtex_entries: List[Text.Info[String]] =
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66114
diff changeset
   289
      try { Bibtex.entries(text) }
67288
aa9d28034945 avoid spurious noise: Prover IDE is meant to check for errors;
wenzelm
parents: 67266
diff changeset
   290
      catch { case ERROR(_) => Nil }
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   291
  }
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   292
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   293
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   294
  /* HTTP preview */
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   295
67263
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
   296
  private val plain_text_prefix = "plain_text="
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
   297
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   298
  def open_preview(view: View, plain_text: Boolean): Unit =
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   299
  {
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   300
    Document_Model.get(view.getBuffer) match {
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67244
diff changeset
   301
      case Some(model) =>
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67244
diff changeset
   302
        val name = model.node_name
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67244
diff changeset
   303
        val url =
73200
wenzelm
parents: 73199
diff changeset
   304
          PIDE.plugin.http_server.url + PIDE.plugin.http_root + "/preview?" +
67263
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
   305
            (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67244
diff changeset
   306
        PIDE.editor.hyperlink_url(url).follow(view)
66036
b6396880b644 clarified;
wenzelm
parents: 66019
diff changeset
   307
      case _ =>
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   308
    }
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   309
  }
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   310
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   311
  def http_handlers(http_root: String): List[HTTP.Handler] =
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   312
  {
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67244
diff changeset
   313
    val fonts_root = http_root + "/fonts"
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   314
    val preview_root = http_root + "/preview"
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67244
diff changeset
   315
73197
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 73009
diff changeset
   316
    val html =
73665
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   317
      HTTP.Handler.get(preview_root, arg =>
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   318
        for {
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69260
diff changeset
   319
          query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
67263
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
   320
          name = Library.perhaps_unprefix(plain_text_prefix, query)
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
   321
          model <- get(PIDE.resources.node_name(name))
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   322
        }
67254
93b4333f33bb clarified modules;
wenzelm
parents: 67253
diff changeset
   323
        yield {
93b4333f33bb clarified modules;
wenzelm
parents: 67253
diff changeset
   324
          val snapshot = model.await_stable_snapshot()
73201
wenzelm
parents: 73200
diff changeset
   325
          val html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root))
73197
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 73009
diff changeset
   326
          val document =
73276
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73201
diff changeset
   327
            Presentation.html_document(
73297
3e4df2e689ff clarified signature;
wenzelm
parents: 73276
diff changeset
   328
              PIDE.resources, snapshot, html_context, Presentation.elements2,
67263
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67261
diff changeset
   329
              plain_text = query.startsWith(plain_text_prefix))
73197
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 73009
diff changeset
   330
          HTTP.Response.html(document.content)
67254
93b4333f33bb clarified modules;
wenzelm
parents: 67253
diff changeset
   331
        })
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   332
73774
c42144d9dde6 more uniform HTTP resources;
wenzelm
parents: 73665
diff changeset
   333
    List(HTTP.welcome(http_root), HTTP.fonts(fonts_root), html)
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   334
  }
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   335
}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   336
64829
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
   337
sealed abstract class Document_Model extends Document.Model
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   338
{
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   339
  /* perspective */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   340
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   341
  def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   342
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   343
  def node_perspective(
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   344
    doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
43397
dba359c0ae3b more robust init;
wenzelm
parents: 43394
diff changeset
   345
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   346
    GUI_Thread.require {}
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   347
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   348
    if (Isabelle.continuous_checking && is_theory) {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   349
      val snapshot = this.snapshot()
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   350
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   351
      val reparse = snapshot.node.load_commands_changed(doc_blobs)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   352
      val perspective =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   353
        if (hidden) Text.Perspective.empty
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   354
        else {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   355
          val view_ranges = document_view_ranges(snapshot)
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69260
diff changeset
   356
          val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   357
          Text.Perspective(view_ranges ::: load_ranges)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   358
        }
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66040
diff changeset
   359
      val overlays = PIDE.editor.node_overlays(node_name)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   360
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   361
      (reparse, Document.Node.Perspective(node_required, perspective, overlays))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   362
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   363
    else (false, Document.Node.no_perspective_text)
43397
dba359c0ae3b more robust init;
wenzelm
parents: 43394
diff changeset
   364
  }
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   365
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   366
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   367
  /* snapshot */
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   368
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   369
  @tailrec final def await_stable_snapshot(): Document.Snapshot =
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   370
  {
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   371
    val snapshot = this.snapshot()
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   372
    if (snapshot.is_outdated) {
71899
5036edb025b7 clarified signature;
wenzelm
parents: 71816
diff changeset
   373
      PIDE.options.seconds("editor_output_delay").sleep
66019
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   374
      await_stable_snapshot()
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   375
    }
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   376
    else snapshot
69b5ef78fb07 HTML preview via builtin HTTP server;
wenzelm
parents: 65469
diff changeset
   377
  }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   378
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   379
64863
wenzelm
parents: 64858
diff changeset
   380
object File_Model
wenzelm
parents: 64858
diff changeset
   381
{
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   382
  def empty(session: Session): File_Model =
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   383
    File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   384
      false, Document.Node.no_perspective_text, Nil)
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   385
64863
wenzelm
parents: 64858
diff changeset
   386
  def init(session: Session,
wenzelm
parents: 64858
diff changeset
   387
    node_name: Document.Node.Name,
wenzelm
parents: 64858
diff changeset
   388
    text: String,
wenzelm
parents: 64858
diff changeset
   389
    node_required: Boolean = false,
wenzelm
parents: 64858
diff changeset
   390
    last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
wenzelm
parents: 64858
diff changeset
   391
    pending_edits: List[Text.Edit] = Nil): File_Model =
wenzelm
parents: 64858
diff changeset
   392
  {
65469
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 65359
diff changeset
   393
    val file = JEdit_Lib.check_file(node_name.node)
65245
e955b33f432c proper plugin access;
wenzelm
parents: 65243
diff changeset
   394
    file.foreach(PIDE.plugin.file_watcher.register_parent(_))
64863
wenzelm
parents: 64858
diff changeset
   395
64864
eec7ffef0be6 accomodate very big file_models and changed_files;
wenzelm
parents: 64863
diff changeset
   396
    val content = Document_Model.File_Content(text)
71949
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71899
diff changeset
   397
    val node_required1 = node_required || File_Format.registry.is_theory(node_name)
67291
1bd9a0142d7a bibtex theory is always required and thus eventually consolidated;
wenzelm
parents: 67288
diff changeset
   398
    File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
64863
wenzelm
parents: 64858
diff changeset
   399
  }
wenzelm
parents: 64858
diff changeset
   400
}
wenzelm
parents: 64858
diff changeset
   401
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   402
case class File_Model(
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   403
  session: Session,
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   404
  node_name: Document.Node.Name,
64864
eec7ffef0be6 accomodate very big file_models and changed_files;
wenzelm
parents: 64863
diff changeset
   405
  file: Option[JFile],
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   406
  content: Document_Model.File_Content,
64863
wenzelm
parents: 64858
diff changeset
   407
  node_required: Boolean,
wenzelm
parents: 64858
diff changeset
   408
  last_perspective: Document.Node.Perspective_Text,
wenzelm
parents: 64858
diff changeset
   409
  pending_edits: List[Text.Edit]) extends Document_Model
34588
e8ac8794971f superficial tuning;
wenzelm
parents: 34583
diff changeset
   410
{
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   411
  /* text */
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   412
67014
e6a695d6a6b2 tuned signature;
wenzelm
parents: 66959
diff changeset
   413
  def get_text(range: Text.Range): Option[String] =
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   414
    range.try_substring(content.text)
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   415
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   416
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   417
  /* header */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   418
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   419
  def node_header: Document.Node.Header =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   420
    PIDE.resources.special_header(node_name) getOrElse
73009
a9ef39041114 clarified signature;
wenzelm
parents: 72888
diff changeset
   421
      PIDE.resources.check_thy(node_name, Scan.char_reader(content.text), strict = false)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   422
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   423
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   424
  /* content */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   425
64829
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
   426
  def node_position(offset: Text.Offset): Line.Node_Position =
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
   427
    Line.Node_Position(node_name.node,
65196
e8760a98db78 discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents: 65132
diff changeset
   428
      Line.Position.zero.advance(content.text.substring(0, offset)))
64829
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
   429
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   430
  def get_blob: Option[Document.Blob] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   431
    if (is_theory) None
67266
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67263
diff changeset
   432
    else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   433
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   434
  def bibtex_entries: List[Text.Info[String]] =
69260
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68477
diff changeset
   435
    if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil
64680
wenzelm
parents: 64673
diff changeset
   436
wenzelm
parents: 64673
diff changeset
   437
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   438
  /* edits */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   439
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   440
  def update_text(text: String): Option[File_Model] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   441
    Text.Edit.replace(0, content.text, text) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   442
      case Nil => None
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   443
      case edits =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   444
        val content1 = Document_Model.File_Content(text)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   445
        val pending_edits1 = pending_edits ::: edits
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   446
        Some(copy(content = content1, pending_edits = pending_edits1))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   447
    }
38222
dac5fa0ac971 replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents: 38158
diff changeset
   448
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   449
  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   450
    : Option[(List[Document.Edit_Text], File_Model)] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   451
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   452
    val (reparse, perspective) = node_perspective(doc_blobs, hidden)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   453
    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   454
      val edits = node_edits(node_header, pending_edits, perspective)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   455
      Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   456
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   457
    else None
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   458
  }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   459
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   460
  def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
67310
506acf60d6b1 proper purge of auxiliary bibtex theory;
wenzelm
parents: 67308
diff changeset
   461
    if (pending_edits.nonEmpty ||
71949
6c470c918aad more general support for isabelle_scala_service;
wenzelm
parents: 71899
diff changeset
   462
        !File_Format.registry.is_theory(node_name) &&
67310
506acf60d6b1 proper purge of auxiliary bibtex theory;
wenzelm
parents: 67308
diff changeset
   463
          (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   464
    else {
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   465
      val text_edits = List(Text.Edit.remove(0, content.text))
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   466
      Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   467
    }
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64864
diff changeset
   468
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   469
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   470
  /* snapshot */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   471
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   472
  def is_stable: Boolean = pending_edits.isEmpty
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   473
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   474
}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   475
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   476
case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   477
  extends Document_Model
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   478
{
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   479
  /* text */
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   480
67014
e6a695d6a6b2 tuned signature;
wenzelm
parents: 66959
diff changeset
   481
  def get_text(range: Text.Range): Option[String] =
e6a695d6a6b2 tuned signature;
wenzelm
parents: 66959
diff changeset
   482
    JEdit_Lib.get_text(buffer, range)
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   483
c137a9f038a6 clarified signature;
wenzelm
parents: 66101
diff changeset
   484
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   485
  /* header */
54509
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 54464
diff changeset
   486
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 47393
diff changeset
   487
  def node_header(): Document.Node.Header =
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46750
diff changeset
   488
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   489
    GUI_Thread.require {}
54509
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 54464
diff changeset
   490
64673
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 63446
diff changeset
   491
    PIDE.resources.special_header(node_name) getOrElse
64826
c97296294f6d clarified check_thy_reader: check node_name here;
wenzelm
parents: 64825
diff changeset
   492
      JEdit_Lib.buffer_lock(buffer) {
73009
a9ef39041114 clarified signature;
wenzelm
parents: 72888
diff changeset
   493
        PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
46748
8f3ae4d04a2d refined node_header -- more direct buffer access (again);
wenzelm
parents: 46740
diff changeset
   494
      }
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46750
diff changeset
   495
  }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   496
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   497
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   498
  /* perspective */
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   499
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   500
  // owned by GUI thread
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   501
  private var _node_required = false
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   502
  def node_required: Boolean = _node_required
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   503
  def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
52808
143f225e50f5 allow explicit indication of required node: full eval, no prints;
wenzelm
parents: 52807
diff changeset
   504
64883
e89f5ef32aa2 tuned signature;
wenzelm
parents: 64868
diff changeset
   505
  def document_view_iterator: Iterator[Document_View] =
e89f5ef32aa2 tuned signature;
wenzelm
parents: 64868
diff changeset
   506
    for {
e89f5ef32aa2 tuned signature;
wenzelm
parents: 64868
diff changeset
   507
      text_area <- JEdit_Lib.jedit_text_areas(buffer)
e89f5ef32aa2 tuned signature;
wenzelm
parents: 64868
diff changeset
   508
      doc_view <- Document_View.get(text_area)
e89f5ef32aa2 tuned signature;
wenzelm
parents: 64868
diff changeset
   509
    } yield doc_view
e89f5ef32aa2 tuned signature;
wenzelm
parents: 64868
diff changeset
   510
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   511
  override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   512
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   513
    GUI_Thread.require {}
52759
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 50565
diff changeset
   514
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   515
    (for {
64883
e89f5ef32aa2 tuned signature;
wenzelm
parents: 64868
diff changeset
   516
      doc_view <- document_view_iterator
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   517
      range <- doc_view.perspective(snapshot).ranges.iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   518
    } yield range).toList
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   519
  }
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   520
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   521
54509
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 54464
diff changeset
   522
  /* blob */
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 54464
diff changeset
   523
64885
205274ca16ee tuned whitespace;
wenzelm
parents: 64883
diff changeset
   524
  // owned by GUI thread
67266
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67263
diff changeset
   525
  private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   526
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   527
  private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   528
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   529
  def get_blob: Option[Document.Blob] =
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   530
    GUI_Thread.require {
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   531
      if (is_theory) None
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   532
      else {
67266
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67263
diff changeset
   533
        val (bytes, text, chunk) =
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   534
          _blob match {
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   535
            case Some(x) => x
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   536
            case None =>
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
   537
              val bytes = PIDE.resources.make_file_content(buffer)
67266
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67263
diff changeset
   538
              val text = buffer.getText(0, buffer.getLength)
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67263
diff changeset
   539
              val chunk = Symbol.Text_Chunk(text)
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67263
diff changeset
   540
              val x = (bytes, text, chunk)
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67263
diff changeset
   541
              _blob = Some(x)
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67263
diff changeset
   542
              x
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   543
          }
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   544
        val changed = pending_edits.nonEmpty
67266
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67263
diff changeset
   545
        Some(Document.Blob(bytes, text, chunk, changed))
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   546
      }
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   547
    }
54509
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 54464
diff changeset
   548
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 54464
diff changeset
   549
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   550
  /* bibtex entries */
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   551
64885
205274ca16ee tuned whitespace;
wenzelm
parents: 64883
diff changeset
   552
  // owned by GUI thread
205274ca16ee tuned whitespace;
wenzelm
parents: 64883
diff changeset
   553
  private var _bibtex_entries: Option[List[Text.Info[String]]] = None
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   554
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   555
  private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   556
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   557
  def bibtex_entries: List[Text.Info[String]] =
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   558
    GUI_Thread.require {
69260
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68477
diff changeset
   559
      if (Bibtex.is_bibtex(node_name.node)) {
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   560
        _bibtex_entries match {
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   561
          case Some(entries) => entries
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   562
          case None =>
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   563
            val text = JEdit_Lib.buffer_text(buffer)
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64827
diff changeset
   564
            val entries =
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66114
diff changeset
   565
              try { Bibtex.entries(text) }
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64827
diff changeset
   566
              catch { case ERROR(msg) => Output.warning(msg); Nil }
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   567
            _bibtex_entries = Some(entries)
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   568
            entries
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   569
        }
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   570
      }
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   571
      else Nil
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   572
    }
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   573
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   574
50344
608265769ce0 emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents: 50207
diff changeset
   575
  /* pending edits */
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43644
diff changeset
   576
60272
4f72b00d9952 no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents: 59737
diff changeset
   577
  private object pending_edits
38224
809578d7f6af more explicit model of pending text edits;
wenzelm
parents: 38223
diff changeset
   578
  {
38425
e467db701d78 moved Text_Edit to Text.Edit;
wenzelm
parents: 38417
diff changeset
   579
    private val pending = new mutable.ListBuffer[Text.Edit]
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57612
diff changeset
   580
    private var last_perspective = Document.Node.no_perspective_text
44438
0fc38897248a early filtering of unchanged perspective;
wenzelm
parents: 44436
diff changeset
   581
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   582
    def nonEmpty: Boolean = synchronized { pending.nonEmpty }
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   583
    def get_edits: List[Text.Edit] = synchronized { pending.toList }
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   584
    def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   585
    def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   586
      synchronized { last_perspective = perspective }
38224
809578d7f6af more explicit model of pending text edits;
wenzelm
parents: 38223
diff changeset
   587
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   588
    def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
61728
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61539
diff changeset
   589
      synchronized {
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61539
diff changeset
   590
        GUI_Thread.require {}
60272
4f72b00d9952 no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents: 59737
diff changeset
   591
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   592
        val edits = get_edits
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   593
        val (reparse, perspective) = node_perspective(doc_blobs, hidden)
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   594
        if (reparse || edits.nonEmpty || last_perspective != perspective) {
73614
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73605
diff changeset
   595
          pending.clear()
61728
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61539
diff changeset
   596
          last_perspective = perspective
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69260
diff changeset
   597
          node_edits(node_header(), edits, perspective)
61728
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61539
diff changeset
   598
        }
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61539
diff changeset
   599
        else Nil
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43644
diff changeset
   600
      }
38224
809578d7f6af more explicit model of pending text edits;
wenzelm
parents: 38223
diff changeset
   601
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   602
    def edit(edits: List[Text.Edit]): Unit = synchronized
38224
809578d7f6af more explicit model of pending text edits;
wenzelm
parents: 38223
diff changeset
   603
    {
60272
4f72b00d9952 no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents: 59737
diff changeset
   604
      GUI_Thread.require {}
4f72b00d9952 no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents: 59737
diff changeset
   605
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   606
      reset_blob()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   607
      reset_bibtex_entries()
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   608
64883
e89f5ef32aa2 tuned signature;
wenzelm
parents: 64868
diff changeset
   609
      for (doc_view <- document_view_iterator)
61539
bf4969660913 avoid highlighted area getting "stuck" after edit;
wenzelm
parents: 61192
diff changeset
   610
        doc_view.rich_text_area.active_reset()
bf4969660913 avoid highlighted area getting "stuck" after edit;
wenzelm
parents: 61192
diff changeset
   611
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   612
      pending ++= edits
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66040
diff changeset
   613
      PIDE.editor.invoke()
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   614
    }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   615
  }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   616
64835
fd1efd6dd385 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents: 64832
diff changeset
   617
  def is_stable: Boolean = !pending_edits.nonEmpty
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   618
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
60933
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60274
diff changeset
   619
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   620
  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   621
    pending_edits.flush_edits(doc_blobs, hidden)
34828
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   622
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   623
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   624
  /* buffer listener */
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   625
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   626
  private val buffer_listener: BufferListener = new BufferAdapter
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   627
  {
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   628
    override def contentInserted(buffer: JEditBuffer,
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   629
      start_line: Int, offset: Int, num_lines: Int, length: Int): Unit =
34828
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   630
    {
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   631
      pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
34828
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   632
    }
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   633
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   634
    override def preContentRemoved(buffer: JEditBuffer,
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   635
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int): Unit =
34828
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   636
    {
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   637
      pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
34828
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   638
    }
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   639
  }
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   640
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   641
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   642
  /* syntax */
37557
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents: 37555
diff changeset
   643
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   644
  def syntax_changed(): Unit =
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   645
  {
61192
98eba31c51f8 tuned signature;
wenzelm
parents: 60933
diff changeset
   646
    JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
59080
611914621edb added Untyped.method convenience (for *this* class only);
wenzelm
parents: 59079
diff changeset
   647
    for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
611914621edb added Untyped.method convenience (for *this* class only);
wenzelm
parents: 59079
diff changeset
   648
      Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
611914621edb added Untyped.method convenience (for *this* class only);
wenzelm
parents: 59079
diff changeset
   649
        invoke(text_area)
73200
wenzelm
parents: 73199
diff changeset
   650
    buffer.invalidateCachedFoldLevels()
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   651
  }
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   652
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73297
diff changeset
   653
  def init_token_marker(): Unit =
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   654
  {
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   655
    Isabelle.buffer_token_marker(buffer) match {
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   656
      case Some(marker) if marker != buffer.getTokenMarker =>
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   657
        buffer.setTokenMarker(marker)
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   658
        syntax_changed()
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   659
      case _ =>
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   660
    }
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   661
  }
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   662
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   663
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   664
  /* init */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   665
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   666
  def init(old_model: Option[File_Model]): Buffer_Model =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   667
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   668
    GUI_Thread.require {}
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   669
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   670
    old_model match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   671
      case None =>
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   672
        pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   673
      case Some(file_model) =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   674
        set_node_required(file_model.node_required)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   675
        pending_edits.set_last_perspective(file_model.last_perspective)
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   676
        pending_edits.edit(
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   677
          file_model.pending_edits :::
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   678
            Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   679
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   680
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   681
    buffer.addBufferListener(buffer_listener)
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   682
    init_token_marker()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   683
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   684
    this
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   685
  }
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   686
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   687
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   688
  /* exit */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   689
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   690
  def exit(): File_Model =
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   691
  {
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   692
    GUI_Thread.require {}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   693
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   694
    buffer.removeBufferListener(buffer_listener)
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   695
    init_token_marker()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   696
64863
wenzelm
parents: 64858
diff changeset
   697
    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
wenzelm
parents: 64858
diff changeset
   698
      pending_edits.get_last_perspective, pending_edits.get_edits)
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   699
  }
34447
wenzelm
parents: 34446
diff changeset
   700
}