replaced individual Document_Model history by all-inclusive one in Session;
authorwenzelm
Sat Aug 07 14:45:26 2010 +0200 (2010-08-07)
changeset 38222dac5fa0ac971
parent 38221 e0f00f0945b4
child 38223 2a368e8e0a80
replaced individual Document_Model history by all-inclusive one in Session;
Document_Model: provide thy_name externally, i.e. by central Isabelle plugin;
tuned;
src/Pure/PIDE/change.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Pure/PIDE/change.scala	Sat Aug 07 13:19:48 2010 +0200
     1.2 +++ b/src/Pure/PIDE/change.scala	Sat Aug 07 14:45:26 2010 +0200
     1.3 @@ -44,18 +44,6 @@
     1.4  
     1.5    /* editing and state assignment */
     1.6  
     1.7 -  def edit(session: Session, edits: List[Document.Node_Text_Edit]): Change =
     1.8 -  {
     1.9 -    val new_id = session.create_id()
    1.10 -    val result: Future[(List[Document.Edit[Command]], Document)] =
    1.11 -      Future.fork {
    1.12 -        val old_doc = join_document
    1.13 -        old_doc.await_assignment
    1.14 -        Document.text_edits(session, old_doc, new_id, edits)
    1.15 -      }
    1.16 -    new Change(new_id, Some(this), edits, result)
    1.17 -  }
    1.18 -
    1.19    def join_document: Document = result.join._2
    1.20    def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
    1.21  
     2.1 --- a/src/Pure/System/session.scala	Sat Aug 07 13:19:48 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sat Aug 07 14:45:26 2010 +0200
     2.3 @@ -315,4 +315,28 @@
     2.4    def stop() { session_actor ! Stop }
     2.5  
     2.6    def input(change: Change) { session_actor ! change }
     2.7 +
     2.8 +
     2.9 +
    2.10 +  /** editor model **/  // FIXME subclass Editor_Session (!?)
    2.11 +
    2.12 +  @volatile private var history = Change.init // owned by Swing thread (!??)
    2.13 +  def current_change(): Change = history
    2.14 +
    2.15 +  def edit_document(edits: List[Document.Node_Text_Edit])
    2.16 +  {
    2.17 +    Swing_Thread.now {
    2.18 +      val old_change = current_change()
    2.19 +      val new_id = create_id()
    2.20 +      val result: Future[(List[Document.Edit[Command]], Document)] =
    2.21 +        Future.fork {
    2.22 +          val old_doc = old_change.join_document
    2.23 +          old_doc.await_assignment
    2.24 +          Document.text_edits(this, old_doc, new_id, edits)
    2.25 +        }
    2.26 +      val new_change = new Change(new_id, Some(old_change), edits, result)
    2.27 +      history = new_change
    2.28 +      new_change.result.map(_ => input(new_change))
    2.29 +    }
    2.30 +  }
    2.31  }
     3.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 13:19:48 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 14:45:26 2010 +0200
     3.3 @@ -2,7 +2,7 @@
     3.4      Author:     Fabian Immler, TU Munich
     3.5      Author:     Makarius
     3.6  
     3.7 -Document model connected to jEdit buffer.
     3.8 +Document model connected to jEdit buffer -- single node in theory graph.
     3.9  */
    3.10  
    3.11  package isabelle.jedit
    3.12 @@ -149,10 +149,10 @@
    3.13  
    3.14    private val key = "isabelle.document_model"
    3.15  
    3.16 -  def init(session: Session, buffer: Buffer): Document_Model =
    3.17 +  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
    3.18    {
    3.19      Swing_Thread.assert()
    3.20 -    val model = new Document_Model(session, buffer)
    3.21 +    val model = new Document_Model(session, buffer, thy_name)
    3.22      buffer.setProperty(key, model)
    3.23      model.activate()
    3.24      model
    3.25 @@ -180,7 +180,7 @@
    3.26  }
    3.27  
    3.28  
    3.29 -class Document_Model(val session: Session, val buffer: Buffer)
    3.30 +class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
    3.31  {
    3.32    /* visible line end */
    3.33  
    3.34 @@ -195,33 +195,22 @@
    3.35    }
    3.36  
    3.37  
    3.38 -  /* global state -- owned by Swing thread */
    3.39 +  /* text edits */
    3.40 +
    3.41 +  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
    3.42  
    3.43 -  @volatile private var history = Change.init // owned by Swing thread
    3.44 -  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
    3.45 +  private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
    3.46 +    if (!edits_buffer.isEmpty) {
    3.47 +      session.edit_document(List((thy_name, edits_buffer.toList)))
    3.48 +      edits_buffer.clear
    3.49 +    }
    3.50 +  }
    3.51  
    3.52  
    3.53    /* snapshot */
    3.54  
    3.55 -  // FIXME proper error handling
    3.56 -  val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2
    3.57 -
    3.58 -  def current_change(): Change = history
    3.59 -
    3.60    def snapshot(): Change.Snapshot =
    3.61 -    Swing_Thread.now { history.snapshot(thy_name, edits_buffer.toList) }
    3.62 -
    3.63 -
    3.64 -  /* text edits */
    3.65 -
    3.66 -  private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
    3.67 -    if (!edits_buffer.isEmpty) {
    3.68 -      val new_change = history.edit(session, List((thy_name, edits_buffer.toList)))
    3.69 -      edits_buffer.clear
    3.70 -      history = new_change
    3.71 -      new_change.result.map(_ => session.input(new_change))
    3.72 -    }
    3.73 -  }
    3.74 +    Swing_Thread.now { session.current_change().snapshot(thy_name, edits_buffer.toList) }
    3.75  
    3.76  
    3.77    /* buffer listener */
     4.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Sat Aug 07 13:19:48 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Aug 07 14:45:26 2010 +0200
     4.3 @@ -162,7 +162,10 @@
     4.4    def activate_buffer(view: View, buffer: Buffer)
     4.5    {
     4.6      if (prover_started(view)) {
     4.7 -      val model = Document_Model.init(session, buffer)
     4.8 +      // FIXME proper error handling
     4.9 +      val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))
    4.10 +
    4.11 +      val model = Document_Model.init(session, buffer, thy_name)
    4.12        for (text_area <- jedit_text_areas(buffer))
    4.13          Document_View.init(model, text_area)
    4.14      }