src/Tools/jEdit/src/document_model.scala
author wenzelm
Sun Dec 16 18:02:28 2012 +0100 (2012-12-16)
changeset 50565 b00ea974613c
parent 50363 2f8dc9e65401
child 52759 a20631db9c8a
permissions -rw-r--r--
tuned property name;
     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 = "PIDE.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         buffer.propertiesChanged
    46     }
    47   }
    48 
    49   def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
    50   {
    51     Swing_Thread.require()
    52     apply(buffer).map(_.deactivate)
    53     val model = new Document_Model(session, buffer, name)
    54     buffer.setProperty(key, model)
    55     model.activate()
    56     buffer.propertiesChanged
    57     model
    58   }
    59 }
    60 
    61 
    62 class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
    63 {
    64   /* header */
    65 
    66   def node_header(): Document.Node.Header =
    67   {
    68     Swing_Thread.require()
    69     JEdit_Lib.buffer_lock(buffer) {
    70       Exn.capture {
    71         PIDE.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
    72       } match {
    73         case Exn.Res(header) => header
    74         case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
    75       }
    76     }
    77   }
    78 
    79 
    80   /* perspective */
    81 
    82   def node_perspective(): Text.Perspective =
    83   {
    84     Swing_Thread.require()
    85     Text.Perspective(
    86       for {
    87         doc_view <- PIDE.document_views(buffer)
    88         range <- doc_view.perspective().ranges
    89       } yield range)
    90   }
    91 
    92 
    93   /* edits */
    94 
    95   def init_edits(): List[Document.Edit_Text] =
    96   {
    97     Swing_Thread.require()
    98     val header = node_header()
    99     val text = JEdit_Lib.buffer_text(buffer)
   100     val perspective = node_perspective()
   101 
   102     List(session.header_edit(name, header),
   103       name -> Document.Node.Clear(),
   104       name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
   105       name -> Document.Node.Perspective(perspective))
   106   }
   107 
   108   def node_edits(perspective: Text.Perspective, text_edits: List[Text.Edit])
   109     : List[Document.Edit_Text] =
   110   {
   111     Swing_Thread.require()
   112     val header = node_header()
   113 
   114     List(session.header_edit(name, header),
   115       name -> Document.Node.Edits(text_edits),
   116       name -> Document.Node.Perspective(perspective))
   117   }
   118 
   119 
   120   /* pending edits */
   121 
   122   private object pending_edits  // owned by Swing thread
   123   {
   124     private val pending = new mutable.ListBuffer[Text.Edit]
   125     private var last_perspective: Text.Perspective = Text.Perspective.empty
   126 
   127     def snapshot(): List[Text.Edit] = pending.toList
   128 
   129     def flush()
   130     {
   131       Swing_Thread.require()
   132 
   133       val edits = snapshot()
   134       val new_perspective = node_perspective()
   135       if (!edits.isEmpty || last_perspective != new_perspective) {
   136         pending.clear
   137         last_perspective = new_perspective
   138         session.update(node_edits(new_perspective, edits))
   139       }
   140     }
   141 
   142     private val delay_flush =
   143       Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
   144 
   145     def +=(edit: Text.Edit)
   146     {
   147       Swing_Thread.require()
   148       pending += edit
   149       delay_flush.invoke()
   150     }
   151 
   152     def update_perspective()
   153     {
   154       delay_flush.invoke()
   155     }
   156 
   157     def init()
   158     {
   159       flush()
   160       session.update(init_edits())
   161     }
   162 
   163     def exit()
   164     {
   165       delay_flush.revoke()
   166       flush()
   167     }
   168   }
   169 
   170   def update_perspective()
   171   {
   172     Swing_Thread.require()
   173     pending_edits.update_perspective()
   174   }
   175 
   176   def full_perspective()
   177   {
   178     pending_edits.flush()
   179     session.update(node_edits(Text.Perspective(List(JEdit_Lib.buffer_range(buffer))), Nil))
   180   }
   181 
   182 
   183   /* snapshot */
   184 
   185   def snapshot(): Document.Snapshot =
   186   {
   187     Swing_Thread.require()
   188     session.snapshot(name, pending_edits.snapshot())
   189   }
   190 
   191 
   192   /* buffer listener */
   193 
   194   private val buffer_listener: BufferListener = new BufferAdapter
   195   {
   196     override def bufferLoaded(buffer: JEditBuffer)
   197     {
   198       pending_edits.init()
   199     }
   200 
   201     override def contentInserted(buffer: JEditBuffer,
   202       start_line: Int, offset: Int, num_lines: Int, length: Int)
   203     {
   204       if (!buffer.isLoading)
   205         pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
   206     }
   207 
   208     override def preContentRemoved(buffer: JEditBuffer,
   209       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   210     {
   211       if (!buffer.isLoading)
   212         pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
   213     }
   214   }
   215 
   216 
   217   /* activation */
   218 
   219   private def activate()
   220   {
   221     buffer.addBufferListener(buffer_listener)
   222     pending_edits.flush()
   223     Token_Markup.refresh_buffer(buffer)
   224   }
   225 
   226   private def deactivate()
   227   {
   228     pending_edits.exit()
   229     buffer.removeBufferListener(buffer_listener)
   230     Token_Markup.refresh_buffer(buffer)
   231   }
   232 }