--- a/src/Pure/PIDE/change.scala Sat Aug 07 17:24:46 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-/* Title: Pure/PIDE/change.scala
- Author: Fabian Immler, TU Munich
- Author: Makarius
-
-Changes of plain text, resulting in document edits.
-*/
-
-package isabelle
-
-
-object Change
-{
- val init = new Change(Document.NO_ID, None, Nil, Future.value(Nil, Document.init))
-
- abstract class Snapshot
- {
- val document: Document
- val node: Document.Node
- val is_outdated: Boolean
- def convert(offset: Int): Int
- def revert(offset: Int): Int
- }
-}
-
-class Change(
- val id: Document.Version_ID,
- val parent: Option[Change],
- val edits: List[Document.Node_Text_Edit],
- val result: Future[(List[Document.Edit[Command]], Document)])
-{
- /* ancestor versions */
-
- def ancestors: Iterator[Change] = new Iterator[Change]
- {
- private var state: Option[Change] = Some(Change.this)
- def hasNext = state.isDefined
- def next =
- state match {
- case Some(change) => state = change.parent; change
- case None => throw new NoSuchElementException("next on empty iterator")
- }
- }
-
-
- /* editing and state assignment */
-
- def join_document: Document = result.join._2
- def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
-
-
- /* snapshot */
-
- def snapshot(name: String, pending_edits: List[Text_Edit]): Change.Snapshot =
- {
- val latest = this
- val stable = latest.ancestors.find(_.is_assigned)
- require(stable.isDefined)
-
- val edits =
- (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
- (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
- lazy val reverse_edits = edits.reverse
-
- new Change.Snapshot {
- val document = stable.get.join_document
- val node = document.nodes(name)
- val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
- def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
- def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
- }
- }
-}
\ No newline at end of file
--- a/src/Pure/PIDE/document.scala Sat Aug 07 17:24:46 2010 +0200
+++ b/src/Pure/PIDE/document.scala Sat Aug 07 19:52:14 2010 +0200
@@ -14,33 +14,31 @@
object Document
{
- /* unique identifiers */
+ /* formal identifiers */
+ type Version_ID = String
+ type Command_ID = String
type State_ID = String
- type Command_ID = String
- type Version_ID = String
val NO_ID = ""
- /* command start positions */
- def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
- {
- var i = offset
- for (command <- commands) yield {
- val start = i
- i += command.length
- (command, start)
- }
- }
-
-
- /* named document nodes */
+ /** named document nodes **/
object Node
{
val empty: Node = new Node(Linear_Set())
+
+ def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
+ {
+ var i = offset
+ for (command <- commands) yield {
+ val start = i
+ i += command.length
+ (command, start)
+ }
+ }
}
class Node(val commands: Linear_Set[Command])
@@ -48,7 +46,7 @@
/* command ranges */
def command_starts: Iterator[(Command, Int)] =
- Document.command_starts(commands.iterator)
+ Node.command_starts(commands.iterator)
def command_start(cmd: Command): Option[Int] =
command_starts.find(_._1 == cmd).map(_._2)
@@ -85,7 +83,7 @@
- /** editing **/
+ /** changes of plain text, eventually resulting in document edits **/
type Node_Text_Edit = (String, List[Text_Edit]) // FIXME None: remove
@@ -93,6 +91,65 @@
(String, // node name
Option[List[(Option[C], Option[C])]]) // None: remove, Some: insert/remove commands
+ abstract class Snapshot
+ {
+ val document: Document
+ val node: Document.Node
+ val is_outdated: Boolean
+ def convert(offset: Int): Int
+ def revert(offset: Int): Int
+ }
+
+ object Change
+ {
+ val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init))
+ }
+
+ class Change(
+ val id: Version_ID,
+ val parent: Option[Change],
+ val edits: List[Node_Text_Edit],
+ val result: Future[(List[Edit[Command]], Document)])
+ {
+ def ancestors: Iterator[Change] = new Iterator[Change]
+ {
+ private var state: Option[Change] = Some(Change.this)
+ def hasNext = state.isDefined
+ def next =
+ state match {
+ case Some(change) => state = change.parent; change
+ case None => throw new NoSuchElementException("next on empty iterator")
+ }
+ }
+
+ def join_document: Document = result.join._2
+ def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
+
+ def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot =
+ {
+ val latest = Change.this
+ val stable = latest.ancestors.find(_.is_assigned)
+ require(stable.isDefined)
+
+ val edits =
+ (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
+ (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+ lazy val reverse_edits = edits.reverse
+
+ new Snapshot {
+ val document = stable.get.join_document
+ val node = document.nodes(name)
+ val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
+ def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
+ def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+ }
+ }
+ }
+
+
+
+ /** editing **/
+
def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
{
@@ -114,7 +171,7 @@
{
eds match {
case e :: es =>
- command_starts(commands.iterator).find {
+ Node.command_starts(commands.iterator).find {
case (cmd, cmd_start) =>
e.can_edit(cmd.source, cmd_start) ||
e.is_insert && e.start == cmd_start + cmd.length
--- a/src/Pure/System/session.scala Sat Aug 07 17:24:46 2010 +0200
+++ b/src/Pure/System/session.scala Sat Aug 07 19:52:14 2010 +0200
@@ -92,7 +92,7 @@
/* document changes */
- def handle_change(change: Change)
+ def handle_change(change: Document.Change)
//{{{
{
require(change.parent.isDefined)
@@ -244,7 +244,7 @@
prover = null
}
- case change: Change if prover != null =>
+ case change: Document.Change if prover != null =>
handle_change(change)
case result: Isabelle_Process.Result =>
@@ -315,8 +315,8 @@
private val editor_history = new Actor
{
- @volatile private var history = Change.init
- def current_change(): Change = history
+ @volatile private var history = Document.Change.init
+ def current_change(): Document.Change = history
def act
{
@@ -331,7 +331,7 @@
old_doc.await_assignment
Document.text_edits(Session.this, old_doc, new_id, edits)
}
- val new_change = new Change(new_id, Some(old_change), edits, result)
+ val new_change = new Document.Change(new_id, Some(old_change), edits, result)
history = new_change
new_change.result.map(_ => session_actor ! new_change)
@@ -351,6 +351,6 @@
def stop() { session_actor ! Stop }
- def current_change(): Change = editor_history.current_change()
+ def current_change(): Document.Change = editor_history.current_change()
def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history ! Edit_Document(edits) }
}
--- a/src/Pure/build-jars Sat Aug 07 17:24:46 2010 +0200
+++ b/src/Pure/build-jars Sat Aug 07 19:52:14 2010 +0200
@@ -37,7 +37,6 @@
Isar/outer_syntax.scala
Isar/parse.scala
Isar/token.scala
- PIDE/change.scala
PIDE/command.scala
PIDE/document.scala
PIDE/event_bus.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala Sat Aug 07 17:24:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Sat Aug 07 19:52:14 2010 +0200
@@ -225,7 +225,7 @@
/* snapshot */
- def snapshot(): Change.Snapshot = {
+ def snapshot(): Document.Snapshot = {
Swing_Thread.require()
session.current_change().snapshot(thy_name, pending_edits.snapshot())
}
--- a/src/Tools/jEdit/src/jedit/document_view.scala Sat Aug 07 17:24:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Sat Aug 07 19:52:14 2010 +0200
@@ -24,7 +24,7 @@
object Document_View
{
- def choose_color(snapshot: Change.Snapshot, command: Command): Color =
+ def choose_color(snapshot: Document.Snapshot, command: Command): Color =
{
val state = snapshot.document.current_state(command)
if (snapshot.is_outdated) new Color(240, 240, 240)
@@ -116,7 +116,7 @@
}
}
- def full_repaint(snapshot: Change.Snapshot, changed: Set[Command])
+ def full_repaint(snapshot: Document.Snapshot, changed: Set[Command])
{
Swing_Thread.require()
@@ -158,7 +158,8 @@
if (range.hasNext) {
val (cmd0, start0) = range.next
new Iterable[(Command, Int)] {
- def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
+ def iterator =
+ Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
}
}
else Iterable.empty