src/Tools/jEdit/src/document_model.scala
author wenzelm
Wed Aug 24 13:03:39 2011 +0200 (2011-08-24 ago)
changeset 44436 546adfa8a6fc
parent 44385 e7fdb008aa7d
child 44438 0fc38897248a
permissions -rw-r--r--
update_perspective without actual edits, bypassing the full state assignment protocol;
edit_nodes/Perspective: do not touch_descendants here;
propagate editor scroll events via update_perspective;
misc tuning;
     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 -- single node in theory graph.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import scala.collection.mutable
    14 
    15 import org.gjt.sp.jedit.Buffer
    16 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
    17 import org.gjt.sp.jedit.textarea.TextArea
    18 
    19 import java.awt.font.TextAttribute
    20 
    21 
    22 object Document_Model
    23 {
    24   /* document model of buffer */
    25 
    26   private val key = "isabelle.document_model"
    27 
    28   def apply(buffer: Buffer): Option[Document_Model] =
    29   {
    30     Swing_Thread.require()
    31     buffer.getProperty(key) match {
    32       case model: Document_Model => Some(model)
    33       case _ => None
    34     }
    35   }
    36 
    37   def exit(buffer: Buffer)
    38   {
    39     Swing_Thread.require()
    40     apply(buffer) match {
    41       case None =>
    42       case Some(model) =>
    43         model.deactivate()
    44         buffer.unsetProperty(key)
    45     }
    46   }
    47 
    48   def init(session: Session, buffer: Buffer,
    49     master_dir: String, node_name: String, thy_name: String): Document_Model =
    50   {
    51     exit(buffer)
    52     val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
    53     buffer.setProperty(key, model)
    54     model.activate()
    55     model
    56   }
    57 }
    58 
    59 
    60 class Document_Model(val session: Session, val buffer: Buffer,
    61   val master_dir: String, val node_name: String, val thy_name: String)
    62 {
    63   /* header */
    64 
    65   def node_header(): Exn.Result[Thy_Header] =
    66   {
    67     Swing_Thread.require()
    68     Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
    69   }
    70 
    71 
    72   /* perspective */
    73 
    74   def perspective(): Text.Perspective =
    75   {
    76     Swing_Thread.require()
    77     Text.perspective(
    78       for {
    79         doc_view <- Isabelle.document_views(buffer)
    80         range <- doc_view.perspective()
    81       } yield range)
    82   }
    83 
    84 
    85   /* pending text edits */
    86 
    87   private object pending_edits  // owned by Swing thread
    88   {
    89     private val pending = new mutable.ListBuffer[Text.Edit]
    90     private var pending_perspective = false
    91     def snapshot(): List[Text.Edit] = pending.toList
    92 
    93     def flush()
    94     {
    95       Swing_Thread.require()
    96       snapshot() match {
    97         case Nil if !pending_perspective =>
    98         case edits =>
    99           pending.clear
   100           pending_perspective = false
   101           session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
   102       }
   103     }
   104 
   105     def init()
   106     {
   107       flush()
   108       session.init_node(node_name, master_dir,
   109         node_header(), perspective(), Isabelle.buffer_text(buffer))
   110     }
   111 
   112     private val delay_flush =
   113       Swing_Thread.delay_last(session.input_delay) { flush() }
   114 
   115     def +=(edit: Text.Edit)
   116     {
   117       Swing_Thread.require()
   118       pending += edit
   119       delay_flush()
   120     }
   121 
   122     def update_perspective()
   123     {
   124       pending_perspective = true
   125       delay_flush()
   126     }
   127   }
   128 
   129   def update_perspective()
   130   {
   131     Swing_Thread.require()
   132     pending_edits.update_perspective()
   133   }
   134 
   135 
   136   /* snapshot */
   137 
   138   def snapshot(): Document.Snapshot =
   139   {
   140     Swing_Thread.require()
   141     session.snapshot(node_name, pending_edits.snapshot())
   142   }
   143 
   144 
   145   /* buffer listener */
   146 
   147   private val buffer_listener: BufferListener = new BufferAdapter
   148   {
   149     override def bufferLoaded(buffer: JEditBuffer)
   150     {
   151       pending_edits.init()
   152     }
   153 
   154     override def contentInserted(buffer: JEditBuffer,
   155       start_line: Int, offset: Int, num_lines: Int, length: Int)
   156     {
   157       if (!buffer.isLoading)
   158         pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
   159     }
   160 
   161     override def preContentRemoved(buffer: JEditBuffer,
   162       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   163     {
   164       if (!buffer.isLoading)
   165         pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
   166     }
   167   }
   168 
   169 
   170   /* activation */
   171 
   172   private def activate()
   173   {
   174     buffer.addBufferListener(buffer_listener)
   175     pending_edits.init()
   176     Token_Markup.refresh_buffer(buffer)
   177   }
   178 
   179   private def deactivate()
   180   {
   181     pending_edits.flush()
   182     buffer.removeBufferListener(buffer_listener)
   183     Token_Markup.refresh_buffer(buffer)
   184   }
   185 }