# HG changeset patch
# User wenzelm
# Date 1281203534 -7200
# Node ID 6bbb42843b6ecde79d908b89b13f8c6a07eeeb29
# Parent  9d8848d70b0a6e77bdef4233614907e97c514213
concentrate structural document notions in document.scala;
tuned;

diff -r 9d8848d70b0a -r 6bbb42843b6e src/Pure/PIDE/change.scala
--- 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
diff -r 9d8848d70b0a -r 6bbb42843b6e src/Pure/PIDE/document.scala
--- 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
diff -r 9d8848d70b0a -r 6bbb42843b6e src/Pure/System/session.scala
--- 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) }
 }
diff -r 9d8848d70b0a -r 6bbb42843b6e src/Pure/build-jars
--- 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
diff -r 9d8848d70b0a -r 6bbb42843b6e src/Tools/jEdit/src/jedit/document_model.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())
   }
diff -r 9d8848d70b0a -r 6bbb42843b6e src/Tools/jEdit/src/jedit/document_view.scala
--- 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