src/Tools/jEdit/src/document_model.scala
author wenzelm
Sun, 08 Jan 2017 13:03:14 +0100
changeset 64832 f6a09ac4e640
parent 64831 4792ee012e94
child 64835 fd1efd6dd385
permissions -rw-r--r--
tuned;
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
34693
3e995f100ad2 sealed Edit;
wenzelm
parents: 34685
diff changeset
    14
import scala.collection.mutable
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    15
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    16
import org.gjt.sp.jedit.{jEdit, View}
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    17
import org.gjt.sp.jedit.Buffer
61192
98eba31c51f8 tuned signature;
wenzelm
parents: 60933
diff changeset
    18
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
    19
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    20
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    21
object Document_Model
34588
e8ac8794971f superficial tuning;
wenzelm
parents: 34583
diff changeset
    22
{
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    23
  /* document models */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    24
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    25
  sealed case class State(
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    26
    models: Map[Document.Node.Name, Document_Model] = Map.empty,
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    27
    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    28
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    29
    def models_iterator: Iterator[Document_Model] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    30
      for ((_, model) <- models.iterator) yield model
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
    31
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    32
    def file_models_iterator: Iterator[File_Model] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    33
      for {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    34
        (_, model) <- models.iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    35
        if model.isInstanceOf[File_Model]
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    36
      } yield model.asInstanceOf[File_Model]
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
    37
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    38
    def buffer_models_iterator: Iterator[Buffer_Model] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    39
      for ((_, model) <- buffer_models.iterator) yield model
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
    40
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
    41
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    42
    def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    43
      : (Buffer_Model, State) =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    44
    {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    45
      val old_model =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    46
        models.get(node_name) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    47
          case Some(file_model: File_Model) => Some(file_model)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    48
          case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    49
          case _ => None
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    50
        }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    51
      val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    52
      (buffer_model,
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    53
        copy(models = models + (node_name -> buffer_model),
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    54
          buffer_models = buffer_models + (buffer -> buffer_model)))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    55
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    56
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    57
    def close_buffer(buffer: JEditBuffer): State =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    58
    {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    59
      buffer_models.get(buffer) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    60
        case None => this
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    61
        case Some(buffer_model) =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    62
          val file_model = buffer_model.exit()
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    63
          copy(models = models + (file_model.node_name -> file_model),
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    64
            buffer_models = buffer_models - buffer)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    65
      }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    66
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    67
  }
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    68
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    69
  private val state = Synchronized(State())  // owned by GUI thread
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    70
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    71
  def get(name: Document.Node.Name): Option[Document_Model] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    72
    state.value.models.get(name)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    73
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    74
  def get(buffer: JEditBuffer): Option[Buffer_Model] =
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
    75
    state.value.buffer_models.get(buffer)
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    76
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    77
  def is_stable(): Boolean =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    78
    state.value.models_iterator.forall(_.is_stable)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    79
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
    80
  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
64829
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
    81
    for {
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
    82
      model <- state.value.models_iterator
64832
wenzelm
parents: 64831
diff changeset
    83
      Text.Info(range, entry) <- model.bibtex_entries.iterator
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
    84
    } yield Text.Info(range, (entry, model))
64829
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
    85
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    86
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    87
  /* init and exit */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    88
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    89
  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
    90
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    91
    GUI_Thread.require {}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    92
    state.change_result(st =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    93
      st.buffer_models.get(buffer) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    94
        case Some(buffer_model) if buffer_model.node_name == node_name =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    95
          buffer_model.init_token_marker
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    96
          (buffer_model, st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    97
        case _ =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    98
          val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    99
          buffer.propertiesChanged
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   100
          res
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   101
      })
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   102
  }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   103
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   104
  def exit(buffer: Buffer)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   105
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   106
    GUI_Thread.require {}
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
   107
    state.change(st =>
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   108
      if (st.buffer_models.isDefinedAt(buffer)) {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   109
        val res = st.close_buffer(buffer)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   110
        buffer.propertiesChanged
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   111
        res
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   112
      }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   113
      else st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   114
  }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   115
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   116
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   117
  /* required nodes */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   118
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   119
  def required_nodes(): Set[Document.Node.Name] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   120
    (for {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   121
      model <- state.value.models_iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   122
      if model.node_required
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   123
    } yield model.node_name).toSet
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   124
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   125
  def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   126
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   127
    GUI_Thread.require {}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   128
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   129
    val changed =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   130
      state.change_result(st =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   131
        st.models.get(name) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   132
          case None => (false, st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   133
          case Some(model) =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   134
            val required = if (toggle) !model.node_required else set
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   135
            model match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   136
              case model1: File_Model if required != model1.node_required =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   137
                (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   138
              case model1: Buffer_Model if required != model1.node_required =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   139
                model1.set_node_required(required); (true, st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   140
              case _ => (false, st)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   141
            }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   142
        })
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   143
    if (changed) {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   144
      PIDE.options_changed()
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   145
      PIDE.editor.flush()
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   146
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   147
  }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   148
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   149
  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
   150
    Document_Model.get(view.getBuffer).foreach(model =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   151
      node_required(model.node_name, toggle = toggle, set = set))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   152
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   153
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   154
  /* flushed edits */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   155
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   156
  def flush_edits(hidden: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   157
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   158
    GUI_Thread.require {}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   159
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   160
    state.change_result(st =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   161
      {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   162
        val doc_blobs =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   163
          Document.Blobs(
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   164
            (for {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   165
              model <- st.models_iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   166
              blob <- model.get_blob
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   167
            } yield (model.node_name -> blob)).toMap)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   168
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   169
        val buffer_edits =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   170
          (for {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   171
            model <- st.buffer_models_iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   172
            edit <- model.flush_edits(doc_blobs, hidden).iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   173
          } yield edit).toList
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   174
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   175
        val file_edits =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   176
          (for {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   177
            model <- st.file_models_iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   178
            change <- model.flush_edits(doc_blobs, hidden)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   179
          } yield change).toList
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   180
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   181
        val edits = buffer_edits ::: file_edits.flatMap(_._1)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   182
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   183
        ((doc_blobs, edits),
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   184
          st.copy(
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   185
            models = (st.models /: file_edits) { case (ms, (_, m)) => ms + (m.node_name -> m) }))
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64799
diff changeset
   186
      })
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   187
  }
43397
dba359c0ae3b more robust init;
wenzelm
parents: 43394
diff changeset
   188
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   189
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   190
  /* file content */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   191
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   192
  sealed case class File_Content(text: String)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   193
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   194
    lazy val bytes: Bytes = Bytes(text)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   195
    lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   196
    lazy val bibtex_entries: List[Text.Info[String]] =
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   197
      try { Bibtex.document_entries(text) }
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64827
diff changeset
   198
      catch { case ERROR(msg) => Output.warning(msg); Nil }
64817
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
}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   201
64829
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
   202
sealed abstract class Document_Model extends Document.Model
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   203
{
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   204
  /* content */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   205
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   206
  def bibtex_entries: List[Text.Info[String]]
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   207
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   208
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   209
  /* perspective */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   210
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   211
  def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
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
  def node_perspective(
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   214
    doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
43397
dba359c0ae3b more robust init;
wenzelm
parents: 43394
diff changeset
   215
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   216
    GUI_Thread.require {}
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
    if (Isabelle.continuous_checking && is_theory) {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   219
      val snapshot = this.snapshot()
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   220
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   221
      val reparse = snapshot.node.load_commands_changed(doc_blobs)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   222
      val perspective =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   223
        if (hidden) Text.Perspective.empty
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   224
        else {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   225
          val view_ranges = document_view_ranges(snapshot)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   226
          val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   227
          Text.Perspective(view_ranges ::: load_ranges)
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
      val overlays = PIDE.editor.node_overlays(node_name)
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
      (reparse, Document.Node.Perspective(node_required, perspective, overlays))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   232
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   233
    else (false, Document.Node.no_perspective_text)
43397
dba359c0ae3b more robust init;
wenzelm
parents: 43394
diff changeset
   234
  }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   235
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   236
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   237
case class File_Model(
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   238
  session: Session,
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   239
  node_name: Document.Node.Name,
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   240
  content: Document_Model.File_Content,
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   241
  node_required: Boolean = false,
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   242
  last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   243
  pending_edits: List[Text.Edit] = Nil) extends Document_Model
34588
e8ac8794971f superficial tuning;
wenzelm
parents: 34583
diff changeset
   244
{
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   245
  /* header */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   246
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   247
  def node_header: Document.Node.Header =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   248
    PIDE.resources.special_header(node_name) getOrElse
64826
c97296294f6d clarified check_thy_reader: check node_name here;
wenzelm
parents: 64825
diff changeset
   249
      PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   250
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   251
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   252
  /* content */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   253
64829
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
   254
  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
   255
    Line.Node_Position(node_name.node,
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
   256
      Line.Position.zero.advance(content.text.substring(0, offset), Text.Length))
07f209e957bc refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents: 64828
diff changeset
   257
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   258
  def get_blob: Option[Document.Blob] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   259
    if (is_theory) None
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   260
    else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   261
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   262
  def bibtex_entries: List[Text.Info[String]] =
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64827
diff changeset
   263
    if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil
64680
wenzelm
parents: 64673
diff changeset
   264
wenzelm
parents: 64673
diff changeset
   265
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   266
  /* edits */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   267
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   268
  def update_text(text: String): Option[File_Model] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   269
    Text.Edit.replace(0, content.text, text) match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   270
      case Nil => None
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   271
      case edits =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   272
        val content1 = Document_Model.File_Content(text)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   273
        val pending_edits1 = pending_edits ::: edits
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   274
        Some(copy(content = content1, pending_edits = pending_edits1))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   275
    }
38222
dac5fa0ac971 replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents: 38158
diff changeset
   276
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   277
  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   278
    : Option[(List[Document.Edit_Text], File_Model)] =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   279
  {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   280
    val (reparse, perspective) = node_perspective(doc_blobs, hidden)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   281
    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64826
diff changeset
   282
      val edits = node_edits(pending_edits, perspective)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   283
      Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   284
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   285
    else None
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   286
  }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   287
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   288
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   289
  /* snapshot */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   290
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   291
  def is_stable: Boolean = pending_edits.isEmpty
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   292
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   293
}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   294
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   295
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
   296
  extends Document_Model
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   297
{
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   298
  /* 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
   299
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 47393
diff changeset
   300
  def node_header(): Document.Node.Header =
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46750
diff changeset
   301
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   302
    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
   303
64673
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 63446
diff changeset
   304
    PIDE.resources.special_header(node_name) getOrElse
64826
c97296294f6d clarified check_thy_reader: check node_name here;
wenzelm
parents: 64825
diff changeset
   305
      JEdit_Lib.buffer_lock(buffer) {
c97296294f6d clarified check_thy_reader: check node_name here;
wenzelm
parents: 64825
diff changeset
   306
        PIDE.resources.check_thy_reader(
c97296294f6d clarified check_thy_reader: check node_name here;
wenzelm
parents: 64825
diff changeset
   307
          "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
46748
8f3ae4d04a2d refined node_header -- more direct buffer access (again);
wenzelm
parents: 46740
diff changeset
   308
      }
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46750
diff changeset
   309
  }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   310
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   311
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   312
  /* perspective */
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   313
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   314
  // 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
   315
  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
   316
  def node_required: Boolean = _node_required
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   317
  def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }
52808
143f225e50f5 allow explicit indication of required node: full eval, no prints;
wenzelm
parents: 52807
diff changeset
   318
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   319
  override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   320
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   321
    GUI_Thread.require {}
52759
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 50565
diff changeset
   322
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   323
    (for {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   324
      doc_view <- PIDE.document_views(buffer).iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   325
      range <- doc_view.perspective(snapshot).ranges.iterator
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   326
    } yield range).toList
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   327
  }
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   328
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44379
diff changeset
   329
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
   330
  /* 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
   331
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   332
  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by GUI thread
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   333
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   334
  private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   335
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   336
  def get_blob: Option[Document.Blob] =
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57610
diff changeset
   337
    GUI_Thread.require {
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   338
      if (is_theory) None
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   339
      else {
56473
5b5c750e9763 simplified Text.Chunk -- eliminated ooddities;
wenzelm
parents: 56469
diff changeset
   340
        val (bytes, chunk) =
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   341
          _blob match {
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   342
            case Some(x) => x
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   343
            case None =>
56208
06cc31dff138 clarifed module name;
wenzelm
parents: 55791
diff changeset
   344
              val bytes = PIDE.resources.file_content(buffer)
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56662
diff changeset
   345
              val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
56473
5b5c750e9763 simplified Text.Chunk -- eliminated ooddities;
wenzelm
parents: 56469
diff changeset
   346
              _blob = Some((bytes, chunk))
5b5c750e9763 simplified Text.Chunk -- eliminated ooddities;
wenzelm
parents: 56469
diff changeset
   347
              (bytes, chunk)
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
   348
          }
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   349
        val changed = pending_edits.nonEmpty
56473
5b5c750e9763 simplified Text.Chunk -- eliminated ooddities;
wenzelm
parents: 56469
diff changeset
   350
        Some(Document.Blob(bytes, chunk, changed))
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   351
      }
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   352
    }
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
   353
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
   354
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   355
  /* bibtex entries */
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   356
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   357
  private var _bibtex_entries: Option[List[Text.Info[String]]] = None  // owned by GUI thread
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   358
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   359
  private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   360
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   361
  def bibtex_entries: List[Text.Info[String]] =
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   362
    GUI_Thread.require {
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64827
diff changeset
   363
      if (Bibtex.check_name(node_name)) {
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   364
        _bibtex_entries match {
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   365
          case Some(entries) => entries
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   366
          case None =>
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   367
            val text = JEdit_Lib.buffer_text(buffer)
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64827
diff changeset
   368
            val entries =
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   369
              try { Bibtex.document_entries(text) }
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64827
diff changeset
   370
              catch { case ERROR(msg) => Output.warning(msg); Nil }
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   371
            _bibtex_entries = Some(entries)
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   372
            entries
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   373
        }
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   374
      }
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   375
      else Nil
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   376
    }
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   377
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 57883
diff changeset
   378
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
   379
  /* pending edits */
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43644
diff changeset
   380
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
   381
  private object pending_edits
38224
809578d7f6af more explicit model of pending text edits;
wenzelm
parents: 38223
diff changeset
   382
  {
38425
e467db701d78 moved Text_Edit to Text.Edit;
wenzelm
parents: 38417
diff changeset
   383
    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
   384
    private var last_perspective = Document.Node.no_perspective_text
44438
0fc38897248a early filtering of unchanged perspective;
wenzelm
parents: 44436
diff changeset
   385
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   386
    def nonEmpty: Boolean = synchronized { pending.nonEmpty }
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   387
    def get_edits: List[Text.Edit] = synchronized { pending.toList }
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   388
    def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   389
    def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   390
      synchronized { last_perspective = perspective }
38224
809578d7f6af more explicit model of pending text edits;
wenzelm
parents: 38223
diff changeset
   391
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   392
    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: 61538
diff changeset
   393
      synchronized {
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61538
diff changeset
   394
        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
   395
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   396
        val edits = get_edits
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   397
        val (reparse, perspective) = node_perspective(doc_blobs, hidden)
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   398
        if (reparse || edits.nonEmpty || last_perspective != perspective) {
61728
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61538
diff changeset
   399
          pending.clear
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61538
diff changeset
   400
          last_perspective = perspective
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   401
          node_edits(edits, perspective)
61728
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61538
diff changeset
   402
        }
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61538
diff changeset
   403
        else Nil
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43644
diff changeset
   404
      }
38224
809578d7f6af more explicit model of pending text edits;
wenzelm
parents: 38223
diff changeset
   405
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   406
    def edit(edits: List[Text.Edit]): Unit = synchronized
38224
809578d7f6af more explicit model of pending text edits;
wenzelm
parents: 38223
diff changeset
   407
    {
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
   408
      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
   409
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   410
      reset_blob()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   411
      reset_bibtex_entries()
54511
1fd24c96ce9b caching of blob;
wenzelm
parents: 54509
diff changeset
   412
61538
bf4969660913 avoid highlighted area getting "stuck" after edit;
wenzelm
parents: 61192
diff changeset
   413
      for (doc_view <- PIDE.document_views(buffer))
bf4969660913 avoid highlighted area getting "stuck" after edit;
wenzelm
parents: 61192
diff changeset
   414
        doc_view.rich_text_area.active_reset()
bf4969660913 avoid highlighted area getting "stuck" after edit;
wenzelm
parents: 61192
diff changeset
   415
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   416
      pending ++= edits
54461
6c360a6ade0e centralized management of pending buffer edits;
wenzelm
parents: 54441
diff changeset
   417
      PIDE.editor.invoke()
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   418
    }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   419
  }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   420
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   421
  def is_stable(): Boolean = !pending_edits.nonEmpty
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   422
  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
   423
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   424
  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
   425
    pending_edits.flush_edits(doc_blobs, hidden)
34828
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   426
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   427
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   428
  /* buffer listener */
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   429
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   430
  private val buffer_listener: BufferListener = new BufferAdapter
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   431
  {
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   432
    override def contentInserted(buffer: JEditBuffer,
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   433
      start_line: Int, offset: Int, num_lines: Int, length: Int)
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   434
    {
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   435
      pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
34828
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   436
    }
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   437
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   438
    override def preContentRemoved(buffer: JEditBuffer,
38426
2858ec7b6dd8 specific types Text.Offset and Text.Range;
wenzelm
parents: 38425
diff changeset
   439
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
34828
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   440
    {
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   441
      pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
34828
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   442
    }
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   443
  }
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   444
c2308b317244 misc tuning;
wenzelm
parents: 34827
diff changeset
   445
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   446
  /* syntax */
37557
1ae272fd4082 refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents: 37555
diff changeset
   447
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   448
  def syntax_changed()
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   449
  {
61192
98eba31c51f8 tuned signature;
wenzelm
parents: 60933
diff changeset
   450
    JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
59080
611914621edb added Untyped.method convenience (for *this* class only);
wenzelm
parents: 59079
diff changeset
   451
    for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
611914621edb added Untyped.method convenience (for *this* class only);
wenzelm
parents: 59079
diff changeset
   452
      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
   453
        invoke(text_area)
62246
d9410066dbd5 more thorough syntax_changed: new commands need require new folds;
wenzelm
parents: 61728
diff changeset
   454
    buffer.invalidateCachedFoldLevels
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   455
  }
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   456
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   457
  def init_token_marker()
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   458
  {
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   459
    Isabelle.buffer_token_marker(buffer) match {
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   460
      case Some(marker) if marker != buffer.getTokenMarker =>
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   461
        buffer.setTokenMarker(marker)
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   462
        syntax_changed()
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   463
      case _ =>
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   464
    }
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   465
  }
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
   466
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   467
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   468
  /* init */
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
  def init(old_model: Option[File_Model]): Buffer_Model =
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
    GUI_Thread.require {}
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   473
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   474
    old_model match {
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   475
      case None =>
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   476
        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
   477
      case Some(file_model) =>
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   478
        set_node_required(file_model.node_required)
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   479
        pending_edits.set_last_perspective(file_model.last_perspective)
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   480
        pending_edits.edit(
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   481
          file_model.pending_edits :::
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   482
            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
   483
    }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   484
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   485
    buffer.addBufferListener(buffer_listener)
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   486
    init_token_marker()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   487
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   488
    this
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   489
  }
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   490
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   491
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   492
  /* exit */
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   493
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   494
  def exit(): File_Model =
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   495
  {
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   496
    GUI_Thread.require {}
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   497
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   498
    buffer.removeBufferListener(buffer_listener)
59078
cf255dc2b48f more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
wenzelm
parents: 59077
diff changeset
   499
    init_token_marker()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   500
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   501
    val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer))
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   502
    File_Model(session, node_name, content, node_required,
64818
67a0a563d2b3 clarified buffer events: exit model while loading;
wenzelm
parents: 64817
diff changeset
   503
      pending_edits.get_last_perspective, pending_edits.get_edits)
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   504
  }
34447
wenzelm
parents: 34446
diff changeset
   505
}