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