src/Tools/jEdit/src/document_model.scala
author wenzelm
Mon Aug 22 16:12:23 2011 +0200 (2011-08-22)
changeset 44379 1079ab6b342b
parent 44358 2a2df4de1bbe
child 44385 e7fdb008aa7d
permissions -rw-r--r--
added official Text.Range.Ordering;
some support for text perspective;
     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   /* pending text edits */
    64 
    65   def node_header(): Exn.Result[Thy_Header] =
    66     Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
    67 
    68   private object pending_edits  // owned by Swing thread
    69   {
    70     private val pending = new mutable.ListBuffer[Text.Edit]
    71     def snapshot(): List[Text.Edit] = pending.toList
    72 
    73     def flush()
    74     {
    75       Swing_Thread.require()
    76       snapshot() match {
    77         case Nil =>
    78         case edits =>
    79           pending.clear
    80           session.edit_node(node_name, master_dir, node_header(), edits)
    81       }
    82     }
    83 
    84     def init()
    85     {
    86       flush()
    87       session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
    88     }
    89 
    90     private val delay_flush =
    91       Swing_Thread.delay_last(session.input_delay) { flush() }
    92 
    93     def +=(edit: Text.Edit)
    94     {
    95       Swing_Thread.require()
    96       pending += edit
    97       delay_flush()
    98     }
    99   }
   100 
   101 
   102   /* perspective */
   103 
   104   def perspective(): Text.Perspective =
   105   {
   106     Swing_Thread.require()
   107     Text.perspective(
   108       for {
   109         doc_view <- Isabelle.document_views(buffer)
   110         range <- doc_view.perspective()
   111       } yield range)
   112   }
   113 
   114 
   115   /* snapshot */
   116 
   117   def snapshot(): Document.Snapshot =
   118   {
   119     Swing_Thread.require()
   120     session.snapshot(node_name, pending_edits.snapshot())
   121   }
   122 
   123 
   124   /* buffer listener */
   125 
   126   private val buffer_listener: BufferListener = new BufferAdapter
   127   {
   128     override def bufferLoaded(buffer: JEditBuffer)
   129     {
   130       pending_edits.init()
   131     }
   132 
   133     override def contentInserted(buffer: JEditBuffer,
   134       start_line: Int, offset: Int, num_lines: Int, length: Int)
   135     {
   136       if (!buffer.isLoading)
   137         pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
   138     }
   139 
   140     override def preContentRemoved(buffer: JEditBuffer,
   141       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   142     {
   143       if (!buffer.isLoading)
   144         pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
   145     }
   146   }
   147 
   148 
   149   /* activation */
   150 
   151   private def activate()
   152   {
   153     buffer.addBufferListener(buffer_listener)
   154     pending_edits.init()
   155     Token_Markup.refresh_buffer(buffer)
   156   }
   157 
   158   private def deactivate()
   159   {
   160     pending_edits.flush()
   161     buffer.removeBufferListener(buffer_listener)
   162     Token_Markup.refresh_buffer(buffer)
   163   }
   164 }