# HG changeset patch # User wenzelm # Date 1281185126 -7200 # Node ID dac5fa0ac971df3acc93cfca4862679e0ca426c8 # Parent e0f00f0945b4046ff483025da68d20dea2e90d5e replaced individual Document_Model history by all-inclusive one in Session; Document_Model: provide thy_name externally, i.e. by central Isabelle plugin; tuned; diff -r e0f00f0945b4 -r dac5fa0ac971 src/Pure/PIDE/change.scala --- a/src/Pure/PIDE/change.scala Sat Aug 07 13:19:48 2010 +0200 +++ b/src/Pure/PIDE/change.scala Sat Aug 07 14:45:26 2010 +0200 @@ -44,18 +44,6 @@ /* editing and state assignment */ - def edit(session: Session, edits: List[Document.Node_Text_Edit]): Change = - { - val new_id = session.create_id() - val result: Future[(List[Document.Edit[Command]], Document)] = - Future.fork { - val old_doc = join_document - old_doc.await_assignment - Document.text_edits(session, old_doc, new_id, edits) - } - new Change(new_id, Some(this), edits, result) - } - def join_document: Document = result.join._2 def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished diff -r e0f00f0945b4 -r dac5fa0ac971 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sat Aug 07 13:19:48 2010 +0200 +++ b/src/Pure/System/session.scala Sat Aug 07 14:45:26 2010 +0200 @@ -315,4 +315,28 @@ def stop() { session_actor ! Stop } def input(change: Change) { session_actor ! change } + + + + /** editor model **/ // FIXME subclass Editor_Session (!?) + + @volatile private var history = Change.init // owned by Swing thread (!??) + def current_change(): Change = history + + def edit_document(edits: List[Document.Node_Text_Edit]) + { + Swing_Thread.now { + val old_change = current_change() + val new_id = create_id() + val result: Future[(List[Document.Edit[Command]], Document)] = + Future.fork { + val old_doc = old_change.join_document + old_doc.await_assignment + Document.text_edits(this, old_doc, new_id, edits) + } + val new_change = new Change(new_id, Some(old_change), edits, result) + history = new_change + new_change.result.map(_ => input(new_change)) + } + } } diff -r e0f00f0945b4 -r dac5fa0ac971 src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Sat Aug 07 13:19:48 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Sat Aug 07 14:45:26 2010 +0200 @@ -2,7 +2,7 @@ Author: Fabian Immler, TU Munich Author: Makarius -Document model connected to jEdit buffer. +Document model connected to jEdit buffer -- single node in theory graph. */ package isabelle.jedit @@ -149,10 +149,10 @@ private val key = "isabelle.document_model" - def init(session: Session, buffer: Buffer): Document_Model = + def init(session: Session, buffer: Buffer, thy_name: String): Document_Model = { Swing_Thread.assert() - val model = new Document_Model(session, buffer) + val model = new Document_Model(session, buffer, thy_name) buffer.setProperty(key, model) model.activate() model @@ -180,7 +180,7 @@ } -class Document_Model(val session: Session, val buffer: Buffer) +class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String) { /* visible line end */ @@ -195,33 +195,22 @@ } - /* global state -- owned by Swing thread */ + /* text edits */ + + private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread - @volatile private var history = Change.init // owned by Swing thread - private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread + private val edits_delay = Swing_Thread.delay_last(session.input_delay) { + if (!edits_buffer.isEmpty) { + session.edit_document(List((thy_name, edits_buffer.toList))) + edits_buffer.clear + } + } /* snapshot */ - // FIXME proper error handling - val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2 - - def current_change(): Change = history - def snapshot(): Change.Snapshot = - Swing_Thread.now { history.snapshot(thy_name, edits_buffer.toList) } - - - /* text edits */ - - private val edits_delay = Swing_Thread.delay_last(session.input_delay) { - if (!edits_buffer.isEmpty) { - val new_change = history.edit(session, List((thy_name, edits_buffer.toList))) - edits_buffer.clear - history = new_change - new_change.result.map(_ => session.input(new_change)) - } - } + Swing_Thread.now { session.current_change().snapshot(thy_name, edits_buffer.toList) } /* buffer listener */ diff -r e0f00f0945b4 -r dac5fa0ac971 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Sat Aug 07 13:19:48 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Sat Aug 07 14:45:26 2010 +0200 @@ -162,7 +162,10 @@ def activate_buffer(view: View, buffer: Buffer) { if (prover_started(view)) { - val model = Document_Model.init(session, buffer) + // FIXME proper error handling + val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) + + val model = Document_Model.init(session, buffer, thy_name) for (text_area <- jedit_text_areas(buffer)) Document_View.init(model, text_area) }