src/Tools/jEdit/src/document_model.scala
author wenzelm
Sun Oct 05 18:14:26 2014 +0200 (2014-10-05 ago)
changeset 58546 72e2b2a609c4
parent 58543 9c1389befa56
child 58547 6080615b8b96
permissions -rw-r--r--
clarified modules;
     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         for {
   108           doc_view <- PIDE.document_views(buffer)
   109           range <- doc_view.perspective(snapshot).ranges
   110         } yield range
   111 
   112       val load_ranges =
   113         for {
   114           cmd <- snapshot.node.load_commands
   115           blob_name <- cmd.blobs_names
   116           blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
   117           if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
   118           start <- snapshot.node.command_start(cmd)
   119           range = snapshot.convert(cmd.proper_range + start)
   120         } yield range
   121 
   122       val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs))
   123 
   124       (reparse,
   125         Document.Node.Perspective(node_required,
   126           Text.Perspective(document_view_ranges ::: load_ranges),
   127           PIDE.editor.node_overlays(node_name)))
   128     }
   129     else (false, Document.Node.no_perspective_text)
   130   }
   131 
   132 
   133   /* blob */
   134 
   135   private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by GUI thread
   136 
   137   private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
   138 
   139   def get_blob(): Option[Document.Blob] =
   140     GUI_Thread.require {
   141       if (is_theory) None
   142       else {
   143         val (bytes, chunk) =
   144           _blob match {
   145             case Some(x) => x
   146             case None =>
   147               val bytes = PIDE.resources.file_content(buffer)
   148               val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
   149               _blob = Some((bytes, chunk))
   150               (bytes, chunk)
   151           }
   152         val changed = pending_edits.is_pending()
   153         Some(Document.Blob(bytes, chunk, changed))
   154       }
   155     }
   156 
   157 
   158   /* bibtex entries */
   159 
   160   private var _bibtex: Option[List[(String, Text.Offset)]] = None  // owned by GUI thread
   161 
   162   private def reset_bibtex(): Unit = GUI_Thread.require { _bibtex = None }
   163 
   164   def bibtex_entries(): List[(String, Text.Offset)] =
   165     GUI_Thread.require {
   166       if (Bibtex_JEdit.check(buffer)) {
   167         _bibtex match {
   168           case Some(entries) => entries
   169           case None =>
   170             val chunks =
   171               try { Bibtex.parse(JEdit_Lib.buffer_text(buffer)) }
   172               catch { case ERROR(msg) => Output.warning(msg); Nil }
   173             val entries =
   174             {
   175               val result = new mutable.ListBuffer[(String, Text.Offset)]
   176               var offset = 0
   177               for (chunk <- chunks) {
   178                 if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
   179                 offset += chunk.source.length
   180               }
   181               result.toList
   182             }
   183             _bibtex = Some(entries)
   184             entries
   185         }
   186       }
   187       else Nil
   188     }
   189 
   190 
   191   /* edits */
   192 
   193   def node_edits(
   194       clear: Boolean,
   195       text_edits: List[Text.Edit],
   196       perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
   197   {
   198     val edits: List[Document.Edit_Text] =
   199       get_blob() match {
   200         case None =>
   201           val header_edit = session.header_edit(node_name, node_header())
   202           if (clear)
   203             List(header_edit,
   204               node_name -> Document.Node.Clear(),
   205               node_name -> Document.Node.Edits(text_edits),
   206               node_name -> perspective)
   207           else
   208             List(header_edit,
   209               node_name -> Document.Node.Edits(text_edits),
   210               node_name -> perspective)
   211         case Some(blob) =>
   212           List(node_name -> Document.Node.Blob(blob),
   213             node_name -> Document.Node.Edits(text_edits))
   214       }
   215     edits.filterNot(_._2.is_void)
   216   }
   217 
   218 
   219   /* pending edits */
   220 
   221   private object pending_edits  // owned by GUI thread
   222   {
   223     private var pending_clear = false
   224     private val pending = new mutable.ListBuffer[Text.Edit]
   225     private var last_perspective = Document.Node.no_perspective_text
   226 
   227     def is_pending(): Boolean = pending_clear || !pending.isEmpty
   228     def snapshot(): List[Text.Edit] = pending.toList
   229 
   230     def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   231     {
   232       val clear = pending_clear
   233       val edits = snapshot()
   234       val (reparse, perspective) = node_perspective(doc_blobs)
   235       if (clear || reparse || !edits.isEmpty || last_perspective != perspective) {
   236         pending_clear = false
   237         pending.clear
   238         last_perspective = perspective
   239         node_edits(clear, edits, perspective)
   240       }
   241       else Nil
   242     }
   243 
   244     def edit(clear: Boolean, e: Text.Edit)
   245     {
   246       reset_blob()
   247       reset_bibtex()
   248 
   249       if (clear) {
   250         pending_clear = true
   251         pending.clear
   252       }
   253       pending += e
   254       PIDE.editor.invoke()
   255     }
   256   }
   257 
   258   def snapshot(): Document.Snapshot =
   259     GUI_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
   260 
   261   def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   262     GUI_Thread.require { pending_edits.flushed_edits(doc_blobs) }
   263 
   264 
   265   /* buffer listener */
   266 
   267   private val buffer_listener: BufferListener = new BufferAdapter
   268   {
   269     override def bufferLoaded(buffer: JEditBuffer)
   270     {
   271       pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   272     }
   273 
   274     override def contentInserted(buffer: JEditBuffer,
   275       start_line: Int, offset: Int, num_lines: Int, length: Int)
   276     {
   277       if (!buffer.isLoading)
   278         pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
   279     }
   280 
   281     override def preContentRemoved(buffer: JEditBuffer,
   282       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   283     {
   284       if (!buffer.isLoading)
   285         pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
   286     }
   287   }
   288 
   289 
   290   /* activation */
   291 
   292   private def activate()
   293   {
   294     pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   295     buffer.addBufferListener(buffer_listener)
   296     Token_Markup.refresh_buffer(buffer)
   297   }
   298 
   299   private def deactivate()
   300   {
   301     buffer.removeBufferListener(buffer_listener)
   302     Token_Markup.refresh_buffer(buffer)
   303   }
   304 }