src/Tools/jEdit/src/document_model.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 57610 518e28a7c74b
child 57615 df1b3452d71c
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     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 (node in theory graph or
     6 auxiliary file).
     7 */
     8 
     9 package isabelle.jedit
    10 
    11 
    12 import isabelle._
    13 
    14 import scala.collection.mutable
    15 
    16 import org.gjt.sp.jedit.Buffer
    17 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
    18 
    19 
    20 object Document_Model
    21 {
    22   /* document model of buffer */
    23 
    24   private val key = "PIDE.document_model"
    25 
    26   def apply(buffer: Buffer): Option[Document_Model] =
    27   {
    28     GUI_Thread.require {}
    29     buffer.getProperty(key) match {
    30       case model: Document_Model => Some(model)
    31       case _ => None
    32     }
    33   }
    34 
    35   def exit(buffer: Buffer)
    36   {
    37     GUI_Thread.require {}
    38     apply(buffer) match {
    39       case None =>
    40       case Some(model) =>
    41         model.deactivate()
    42         buffer.unsetProperty(key)
    43         buffer.propertiesChanged
    44     }
    45   }
    46 
    47   def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
    48   {
    49     GUI_Thread.require {}
    50     apply(buffer).map(_.deactivate)
    51     val model = new Document_Model(session, buffer, node_name)
    52     buffer.setProperty(key, model)
    53     model.activate()
    54     buffer.propertiesChanged
    55     model
    56   }
    57 }
    58 
    59 
    60 class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
    61 {
    62   /* header */
    63 
    64   def is_theory: Boolean = node_name.is_theory
    65 
    66   def node_header(): Document.Node.Header =
    67   {
    68     GUI_Thread.require {}
    69 
    70     if (is_theory) {
    71       JEdit_Lib.buffer_lock(buffer) {
    72         Exn.capture {
    73           PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer))
    74         } match {
    75           case Exn.Res(header) => header
    76           case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
    77         }
    78       }
    79     }
    80     else Document.Node.no_header
    81   }
    82 
    83 
    84   /* perspective */
    85 
    86   // owned by GUI thread
    87   private var _node_required = false
    88   def node_required: Boolean = _node_required
    89   def node_required_=(b: Boolean)
    90   {
    91     GUI_Thread.require {}
    92     if (_node_required != b && is_theory) {
    93       _node_required = b
    94       PIDE.options_changed()
    95       PIDE.editor.flush()
    96     }
    97   }
    98 
    99   def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
   100   {
   101     GUI_Thread.require {}
   102 
   103     if (Isabelle.continuous_checking && is_theory) {
   104       val snapshot = this.snapshot()
   105 
   106       val document_view_ranges =
   107         if (is_theory) {
   108           for {
   109             doc_view <- PIDE.document_views(buffer)
   110             range <- doc_view.perspective(snapshot).ranges
   111           } yield range
   112         }
   113         else Nil
   114 
   115       val load_ranges =
   116         for {
   117           cmd <- snapshot.node.load_commands
   118           blob_name <- cmd.blobs_names
   119           blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
   120           if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
   121           start <- snapshot.node.command_start(cmd)
   122           range = snapshot.convert(cmd.proper_range + start)
   123         } yield range
   124 
   125       val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs))
   126 
   127       (reparse,
   128         Document.Node.Perspective(node_required,
   129           Text.Perspective(document_view_ranges ::: load_ranges),
   130           PIDE.editor.node_overlays(node_name)))
   131     }
   132     else (false, Document.Node.empty_perspective_text)
   133   }
   134 
   135 
   136   /* blob */
   137 
   138   private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by GUI thread
   139 
   140   private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
   141 
   142   def get_blob(): Option[Document.Blob] =
   143     GUI_Thread.require {
   144       if (is_theory) None
   145       else {
   146         val (bytes, chunk) =
   147           _blob match {
   148             case Some(x) => x
   149             case None =>
   150               val bytes = PIDE.resources.file_content(buffer)
   151               val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
   152               _blob = Some((bytes, chunk))
   153               (bytes, chunk)
   154           }
   155         val changed = pending_edits.is_pending()
   156         Some(Document.Blob(bytes, chunk, changed))
   157       }
   158     }
   159 
   160 
   161   /* edits */
   162 
   163   def node_edits(
   164       clear: Boolean,
   165       text_edits: List[Text.Edit],
   166       perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
   167     get_blob() match {
   168       case None =>
   169         val header_edit = session.header_edit(node_name, node_header())
   170         if (clear)
   171           List(header_edit,
   172             node_name -> Document.Node.Clear(),
   173             node_name -> Document.Node.Edits(text_edits),
   174             node_name -> perspective)
   175         else
   176           List(header_edit,
   177             node_name -> Document.Node.Edits(text_edits),
   178             node_name -> perspective)
   179       case Some(blob) =>
   180         List(node_name -> Document.Node.Blob(blob),
   181           node_name -> Document.Node.Edits(text_edits))
   182     }
   183 
   184 
   185   /* pending edits */
   186 
   187   private object pending_edits  // owned by GUI thread
   188   {
   189     private var pending_clear = false
   190     private val pending = new mutable.ListBuffer[Text.Edit]
   191     private var last_perspective = Document.Node.empty_perspective_text
   192 
   193     def is_pending(): Boolean = pending_clear || !pending.isEmpty
   194     def snapshot(): List[Text.Edit] = pending.toList
   195 
   196     def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   197     {
   198       val clear = pending_clear
   199       val edits = snapshot()
   200       val (reparse, perspective) = node_perspective(doc_blobs)
   201       if (clear || reparse || !edits.isEmpty || last_perspective != perspective) {
   202         pending_clear = false
   203         pending.clear
   204         last_perspective = perspective
   205         node_edits(clear, edits, perspective)
   206       }
   207       else Nil
   208     }
   209 
   210     def edit(clear: Boolean, e: Text.Edit)
   211     {
   212       reset_blob()
   213 
   214       if (clear) {
   215         pending_clear = true
   216         pending.clear
   217       }
   218       pending += e
   219       PIDE.editor.invoke()
   220     }
   221   }
   222 
   223   def snapshot(): Document.Snapshot =
   224     GUI_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
   225 
   226   def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   227     GUI_Thread.require { pending_edits.flushed_edits(doc_blobs) }
   228 
   229 
   230   /* buffer listener */
   231 
   232   private val buffer_listener: BufferListener = new BufferAdapter
   233   {
   234     override def bufferLoaded(buffer: JEditBuffer)
   235     {
   236       pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   237     }
   238 
   239     override def contentInserted(buffer: JEditBuffer,
   240       start_line: Int, offset: Int, num_lines: Int, length: Int)
   241     {
   242       if (!buffer.isLoading)
   243         pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
   244     }
   245 
   246     override def preContentRemoved(buffer: JEditBuffer,
   247       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   248     {
   249       if (!buffer.isLoading)
   250         pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
   251     }
   252   }
   253 
   254 
   255   /* activation */
   256 
   257   private def activate()
   258   {
   259     pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   260     buffer.addBufferListener(buffer_listener)
   261     Token_Markup.refresh_buffer(buffer)
   262   }
   263 
   264   private def deactivate()
   265   {
   266     buffer.removeBufferListener(buffer_listener)
   267     Token_Markup.refresh_buffer(buffer)
   268   }
   269 }