src/Tools/jEdit/src/document_model.scala
author wenzelm
Tue Apr 08 20:03:00 2014 +0200 (2014-04-08)
changeset 56473 5b5c750e9763
parent 56469 ffc94a271633
child 56662 f373fb77e0a4
permissions -rw-r--r--
simplified Text.Chunk -- eliminated ooddities;
afford strict symbol_index, which is usually empty anyway;
     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     Swing_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     Swing_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     Swing_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     Swing_Thread.require()
    69 
    70     if (is_theory) {
    71       JEdit_Lib.buffer_lock(buffer) {
    72         Exn.capture {
    73           PIDE.resources.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
    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 Swing thread
    87   private var _node_required = false
    88   def node_required: Boolean = _node_required
    89   def node_required_=(b: Boolean)
    90   {
    91     Swing_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   val empty_perspective: Document.Node.Perspective_Text =
   100     Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
   101 
   102   def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
   103   {
   104     Swing_Thread.require()
   105 
   106     if (Isabelle.continuous_checking && is_theory) {
   107       val snapshot = this.snapshot()
   108 
   109       val document_view_ranges =
   110         if (is_theory) {
   111           for {
   112             doc_view <- PIDE.document_views(buffer)
   113             range <- doc_view.perspective(snapshot).ranges
   114           } yield range
   115         }
   116         else Nil
   117 
   118       val load_ranges =
   119         for {
   120           cmd <- snapshot.node.load_commands
   121           blob_name <- cmd.blobs_names
   122           blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
   123           if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
   124           start <- snapshot.node.command_start(cmd)
   125           range = snapshot.convert(cmd.proper_range + start)
   126         } yield range
   127 
   128       val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs))
   129 
   130       (reparse,
   131         Document.Node.Perspective(node_required,
   132           Text.Perspective(document_view_ranges ::: load_ranges),
   133           PIDE.editor.node_overlays(node_name)))
   134     }
   135     else (false, empty_perspective)
   136   }
   137 
   138 
   139   /* blob */
   140 
   141   private var _blob: Option[(Bytes, Text.Chunk)] = None  // owned by Swing thread
   142 
   143   private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
   144 
   145   def get_blob(): Option[Document.Blob] =
   146     Swing_Thread.require {
   147       if (is_theory) None
   148       else {
   149         val (bytes, chunk) =
   150           _blob match {
   151             case Some(x) => x
   152             case None =>
   153               val bytes = PIDE.resources.file_content(buffer)
   154               val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
   155               _blob = Some((bytes, chunk))
   156               (bytes, chunk)
   157           }
   158         val changed = pending_edits.is_pending()
   159         Some(Document.Blob(bytes, chunk, changed))
   160       }
   161     }
   162 
   163 
   164   /* edits */
   165 
   166   def node_edits(
   167       clear: Boolean,
   168       text_edits: List[Text.Edit],
   169       perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
   170     get_blob() match {
   171       case None =>
   172         val header_edit = session.header_edit(node_name, node_header())
   173         if (clear)
   174           List(header_edit,
   175             node_name -> Document.Node.Clear(),
   176             node_name -> Document.Node.Edits(text_edits),
   177             node_name -> perspective)
   178         else
   179           List(header_edit,
   180             node_name -> Document.Node.Edits(text_edits),
   181             node_name -> perspective)
   182       case Some(blob) =>
   183         List(node_name -> Document.Node.Blob(blob),
   184           node_name -> Document.Node.Edits(text_edits))
   185     }
   186 
   187 
   188   /* pending edits */
   189 
   190   private object pending_edits  // owned by Swing thread
   191   {
   192     private var pending_clear = false
   193     private val pending = new mutable.ListBuffer[Text.Edit]
   194     private var last_perspective = empty_perspective
   195 
   196     def is_pending(): Boolean = pending_clear || !pending.isEmpty
   197     def snapshot(): List[Text.Edit] = pending.toList
   198 
   199     def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   200     {
   201       val clear = pending_clear
   202       val edits = snapshot()
   203       val (reparse, perspective) = node_perspective(doc_blobs)
   204       if (clear || reparse || !edits.isEmpty || last_perspective != perspective) {
   205         pending_clear = false
   206         pending.clear
   207         last_perspective = perspective
   208         node_edits(clear, edits, perspective)
   209       }
   210       else Nil
   211     }
   212 
   213     def edit(clear: Boolean, e: Text.Edit)
   214     {
   215       reset_blob()
   216 
   217       if (clear) {
   218         pending_clear = true
   219         pending.clear
   220       }
   221       pending += e
   222       PIDE.editor.invoke()
   223     }
   224   }
   225 
   226   def snapshot(): Document.Snapshot =
   227     Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
   228 
   229   def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   230     Swing_Thread.require { pending_edits.flushed_edits(doc_blobs) }
   231 
   232 
   233   /* buffer listener */
   234 
   235   private val buffer_listener: BufferListener = new BufferAdapter
   236   {
   237     override def bufferLoaded(buffer: JEditBuffer)
   238     {
   239       pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   240     }
   241 
   242     override def contentInserted(buffer: JEditBuffer,
   243       start_line: Int, offset: Int, num_lines: Int, length: Int)
   244     {
   245       if (!buffer.isLoading)
   246         pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
   247     }
   248 
   249     override def preContentRemoved(buffer: JEditBuffer,
   250       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   251     {
   252       if (!buffer.isLoading)
   253         pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
   254     }
   255   }
   256 
   257 
   258   /* activation */
   259 
   260   private def activate()
   261   {
   262     pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   263     buffer.addBufferListener(buffer_listener)
   264     Token_Markup.refresh_buffer(buffer)
   265   }
   266 
   267   private def deactivate()
   268   {
   269     buffer.removeBufferListener(buffer_listener)
   270     Token_Markup.refresh_buffer(buffer)
   271   }
   272 }