src/Tools/jEdit/src/document_model.scala
author wenzelm
Tue Aug 23 12:20:12 2011 +0200 (2011-08-23)
changeset 44385 e7fdb008aa7d
parent 44379 1079ab6b342b
child 44436 546adfa8a6fc
permissions -rw-r--r--
propagate editor perspective through document model;
     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     def snapshot(): List[Text.Edit] = pending.toList
    91 
    92     def flush()
    93     {
    94       Swing_Thread.require()
    95       snapshot() match {
    96         case Nil =>
    97         case edits =>
    98           pending.clear
    99           session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
   100       }
   101     }
   102 
   103     def init()
   104     {
   105       flush()
   106       session.init_node(node_name, master_dir,
   107         node_header(), perspective(), Isabelle.buffer_text(buffer))
   108     }
   109 
   110     private val delay_flush =
   111       Swing_Thread.delay_last(session.input_delay) { flush() }
   112 
   113     def +=(edit: Text.Edit)
   114     {
   115       Swing_Thread.require()
   116       pending += edit
   117       delay_flush()
   118     }
   119   }
   120 
   121 
   122   /* snapshot */
   123 
   124   def snapshot(): Document.Snapshot =
   125   {
   126     Swing_Thread.require()
   127     session.snapshot(node_name, pending_edits.snapshot())
   128   }
   129 
   130 
   131   /* buffer listener */
   132 
   133   private val buffer_listener: BufferListener = new BufferAdapter
   134   {
   135     override def bufferLoaded(buffer: JEditBuffer)
   136     {
   137       pending_edits.init()
   138     }
   139 
   140     override def contentInserted(buffer: JEditBuffer,
   141       start_line: Int, offset: Int, num_lines: Int, length: Int)
   142     {
   143       if (!buffer.isLoading)
   144         pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
   145     }
   146 
   147     override def preContentRemoved(buffer: JEditBuffer,
   148       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   149     {
   150       if (!buffer.isLoading)
   151         pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
   152     }
   153   }
   154 
   155 
   156   /* activation */
   157 
   158   private def activate()
   159   {
   160     buffer.addBufferListener(buffer_listener)
   161     pending_edits.init()
   162     Token_Markup.refresh_buffer(buffer)
   163   }
   164 
   165   private def deactivate()
   166   {
   167     pending_edits.flush()
   168     buffer.removeBufferListener(buffer_listener)
   169     Token_Markup.refresh_buffer(buffer)
   170   }
   171 }