src/Tools/jEdit/src/document_model.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 46750 69efe9b2994c
child 47058 34761733526c
permissions -rw-r--r--
more explicit indication of swing thread context;
     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, name: Document.Node.Name): Document_Model =
    49   {
    50     exit(buffer)
    51     val model = new Document_Model(session, buffer, name)
    52     buffer.setProperty(key, model)
    53     model.activate()
    54     model
    55   }
    56 }
    57 
    58 
    59 class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
    60 {
    61   /* header */
    62 
    63   def node_header(): Document.Node_Header =
    64   {
    65     Swing_Thread.require()
    66     Isabelle.buffer_lock(buffer) {
    67       Exn.capture {
    68         Isabelle.thy_load.check_header(name,
    69           Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
    70       }
    71     }
    72   }
    73 
    74 
    75   /* perspective */
    76 
    77   def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0)
    78 
    79   def perspective(): Text.Perspective =
    80   {
    81     Swing_Thread.require()
    82     Text.Perspective(
    83       for {
    84         doc_view <- Isabelle.document_views(buffer)
    85         range <- doc_view.perspective().ranges
    86       } yield range)
    87   }
    88 
    89 
    90   /* pending text edits */
    91 
    92   private object pending_edits  // owned by Swing thread
    93   {
    94     private val pending = new mutable.ListBuffer[Text.Edit]
    95     private var pending_perspective = false
    96     private var last_perspective: Text.Perspective = Text.Perspective.empty
    97 
    98     def snapshot(): List[Text.Edit] = pending.toList
    99 
   100     def flush()
   101     {
   102       Swing_Thread.require()
   103 
   104       val new_perspective =
   105         if (pending_perspective) { pending_perspective = false; perspective() }
   106         else last_perspective
   107 
   108       snapshot() match {
   109         case Nil if last_perspective == new_perspective =>
   110         case edits =>
   111           pending.clear
   112           last_perspective = new_perspective
   113           session.edit_node(name, node_header(), new_perspective, edits)
   114       }
   115     }
   116 
   117     private val delay_flush =
   118       Swing_Thread.delay_last(session.input_delay) { flush() }
   119 
   120     def +=(edit: Text.Edit)
   121     {
   122       Swing_Thread.require()
   123       pending += edit
   124       delay_flush(true)
   125     }
   126 
   127     def update_perspective()
   128     {
   129       pending_perspective = true
   130       delay_flush(true)
   131     }
   132 
   133     def init()
   134     {
   135       flush()
   136       session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
   137     }
   138 
   139     def exit()
   140     {
   141       delay_flush(false)
   142       flush()
   143     }
   144   }
   145 
   146   def update_perspective()
   147   {
   148     Swing_Thread.require()
   149     pending_edits.update_perspective()
   150   }
   151 
   152   def full_perspective()
   153   {
   154     pending_edits.flush()
   155     session.edit_node(name, node_header(), Text.Perspective(List(buffer_range())), Nil)
   156   }
   157 
   158 
   159   /* snapshot */
   160 
   161   def snapshot(): Document.Snapshot =
   162   {
   163     Swing_Thread.require()
   164     session.snapshot(name, pending_edits.snapshot())
   165   }
   166 
   167 
   168   /* buffer listener */
   169 
   170   private val buffer_listener: BufferListener = new BufferAdapter
   171   {
   172     override def bufferLoaded(buffer: JEditBuffer)
   173     {
   174       pending_edits.init()
   175     }
   176 
   177     override def contentInserted(buffer: JEditBuffer,
   178       start_line: Int, offset: Int, num_lines: Int, length: Int)
   179     {
   180       if (!buffer.isLoading)
   181         pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
   182     }
   183 
   184     override def preContentRemoved(buffer: JEditBuffer,
   185       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   186     {
   187       if (!buffer.isLoading)
   188         pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
   189     }
   190   }
   191 
   192 
   193   /* activation */
   194 
   195   private def activate()
   196   {
   197     buffer.addBufferListener(buffer_listener)
   198     pending_edits.init()
   199     Token_Markup.refresh_buffer(buffer)
   200   }
   201 
   202   private def deactivate()
   203   {
   204     pending_edits.exit()
   205     buffer.removeBufferListener(buffer_listener)
   206     Token_Markup.refresh_buffer(buffer)
   207   }
   208 }