concentrate structural document notions in document.scala;
authorwenzelm
Sat Aug 07 19:52:14 2010 +0200 (2010-08-07)
changeset 382276bbb42843b6e
parent 38226 9d8848d70b0a
child 38228 ada3ab6b9085
concentrate structural document notions in document.scala;
tuned;
src/Pure/PIDE/change.scala
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Pure/build-jars
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/document_view.scala
     1.1 --- a/src/Pure/PIDE/change.scala	Sat Aug 07 17:24:46 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,72 +0,0 @@
     1.4 -/*  Title:      Pure/PIDE/change.scala
     1.5 -    Author:     Fabian Immler, TU Munich
     1.6 -    Author:     Makarius
     1.7 -
     1.8 -Changes of plain text, resulting in document edits.
     1.9 -*/
    1.10 -
    1.11 -package isabelle
    1.12 -
    1.13 -
    1.14 -object Change
    1.15 -{
    1.16 -  val init = new Change(Document.NO_ID, None, Nil, Future.value(Nil, Document.init))
    1.17 -
    1.18 -  abstract class Snapshot
    1.19 -  {
    1.20 -    val document: Document
    1.21 -    val node: Document.Node
    1.22 -    val is_outdated: Boolean
    1.23 -    def convert(offset: Int): Int
    1.24 -    def revert(offset: Int): Int
    1.25 -  }
    1.26 -}
    1.27 -
    1.28 -class Change(
    1.29 -  val id: Document.Version_ID,
    1.30 -  val parent: Option[Change],
    1.31 -  val edits: List[Document.Node_Text_Edit],
    1.32 -  val result: Future[(List[Document.Edit[Command]], Document)])
    1.33 -{
    1.34 -  /* ancestor versions */
    1.35 -
    1.36 -  def ancestors: Iterator[Change] = new Iterator[Change]
    1.37 -  {
    1.38 -    private var state: Option[Change] = Some(Change.this)
    1.39 -    def hasNext = state.isDefined
    1.40 -    def next =
    1.41 -      state match {
    1.42 -        case Some(change) => state = change.parent; change
    1.43 -        case None => throw new NoSuchElementException("next on empty iterator")
    1.44 -      }
    1.45 -  }
    1.46 -
    1.47 -
    1.48 -  /* editing and state assignment */
    1.49 -
    1.50 -  def join_document: Document = result.join._2
    1.51 -  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
    1.52 -
    1.53 -
    1.54 -  /* snapshot */
    1.55 -
    1.56 -  def snapshot(name: String, pending_edits: List[Text_Edit]): Change.Snapshot =
    1.57 -  {
    1.58 -    val latest = this
    1.59 -    val stable = latest.ancestors.find(_.is_assigned)
    1.60 -    require(stable.isDefined)
    1.61 -
    1.62 -    val edits =
    1.63 -      (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
    1.64 -          (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
    1.65 -    lazy val reverse_edits = edits.reverse
    1.66 -
    1.67 -    new Change.Snapshot {
    1.68 -      val document = stable.get.join_document
    1.69 -      val node = document.nodes(name)
    1.70 -      val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
    1.71 -      def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
    1.72 -      def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.73 -    }
    1.74 -  }
    1.75 -}
    1.76 \ No newline at end of file
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 07 17:24:46 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 07 19:52:14 2010 +0200
     2.3 @@ -14,33 +14,31 @@
     2.4  
     2.5  object Document
     2.6  {
     2.7 -  /* unique identifiers */
     2.8 +  /* formal identifiers */
     2.9  
    2.10 +  type Version_ID = String
    2.11 +  type Command_ID = String
    2.12    type State_ID = String
    2.13 -  type Command_ID = String
    2.14 -  type Version_ID = String
    2.15  
    2.16    val NO_ID = ""
    2.17  
    2.18  
    2.19 -  /* command start positions */
    2.20  
    2.21 -  def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
    2.22 -  {
    2.23 -    var i = offset
    2.24 -    for (command <- commands) yield {
    2.25 -      val start = i
    2.26 -      i += command.length
    2.27 -      (command, start)
    2.28 -    }
    2.29 -  }
    2.30 -
    2.31 -
    2.32 -  /* named document nodes */
    2.33 +  /** named document nodes **/
    2.34  
    2.35    object Node
    2.36    {
    2.37      val empty: Node = new Node(Linear_Set())
    2.38 +
    2.39 +    def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
    2.40 +    {
    2.41 +      var i = offset
    2.42 +      for (command <- commands) yield {
    2.43 +        val start = i
    2.44 +        i += command.length
    2.45 +        (command, start)
    2.46 +      }
    2.47 +    }
    2.48    }
    2.49  
    2.50    class Node(val commands: Linear_Set[Command])
    2.51 @@ -48,7 +46,7 @@
    2.52      /* command ranges */
    2.53  
    2.54      def command_starts: Iterator[(Command, Int)] =
    2.55 -      Document.command_starts(commands.iterator)
    2.56 +      Node.command_starts(commands.iterator)
    2.57  
    2.58      def command_start(cmd: Command): Option[Int] =
    2.59        command_starts.find(_._1 == cmd).map(_._2)
    2.60 @@ -85,7 +83,7 @@
    2.61  
    2.62  
    2.63  
    2.64 -  /** editing **/
    2.65 +  /** changes of plain text, eventually resulting in document edits **/
    2.66  
    2.67    type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
    2.68  
    2.69 @@ -93,6 +91,65 @@
    2.70     (String,  // node name
    2.71      Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
    2.72  
    2.73 +  abstract class Snapshot
    2.74 +  {
    2.75 +    val document: Document
    2.76 +    val node: Document.Node
    2.77 +    val is_outdated: Boolean
    2.78 +    def convert(offset: Int): Int
    2.79 +    def revert(offset: Int): Int
    2.80 +  }
    2.81 +
    2.82 +  object Change
    2.83 +  {
    2.84 +    val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init))
    2.85 +  }
    2.86 +
    2.87 +  class Change(
    2.88 +    val id: Version_ID,
    2.89 +    val parent: Option[Change],
    2.90 +    val edits: List[Node_Text_Edit],
    2.91 +    val result: Future[(List[Edit[Command]], Document)])
    2.92 +  {
    2.93 +    def ancestors: Iterator[Change] = new Iterator[Change]
    2.94 +    {
    2.95 +      private var state: Option[Change] = Some(Change.this)
    2.96 +      def hasNext = state.isDefined
    2.97 +      def next =
    2.98 +        state match {
    2.99 +          case Some(change) => state = change.parent; change
   2.100 +          case None => throw new NoSuchElementException("next on empty iterator")
   2.101 +        }
   2.102 +    }
   2.103 +
   2.104 +    def join_document: Document = result.join._2
   2.105 +    def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
   2.106 +
   2.107 +    def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot =
   2.108 +    {
   2.109 +      val latest = Change.this
   2.110 +      val stable = latest.ancestors.find(_.is_assigned)
   2.111 +      require(stable.isDefined)
   2.112 +
   2.113 +      val edits =
   2.114 +        (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
   2.115 +            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
   2.116 +      lazy val reverse_edits = edits.reverse
   2.117 +
   2.118 +      new Snapshot {
   2.119 +        val document = stable.get.join_document
   2.120 +        val node = document.nodes(name)
   2.121 +        val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
   2.122 +        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
   2.123 +        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   2.124 +      }
   2.125 +    }
   2.126 +  }
   2.127 +
   2.128 +
   2.129 +
   2.130 +  /** editing **/
   2.131 +
   2.132    def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
   2.133        edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
   2.134    {
   2.135 @@ -114,7 +171,7 @@
   2.136      {
   2.137        eds match {
   2.138          case e :: es =>
   2.139 -          command_starts(commands.iterator).find {
   2.140 +          Node.command_starts(commands.iterator).find {
   2.141              case (cmd, cmd_start) =>
   2.142                e.can_edit(cmd.source, cmd_start) ||
   2.143                  e.is_insert && e.start == cmd_start + cmd.length
     3.1 --- a/src/Pure/System/session.scala	Sat Aug 07 17:24:46 2010 +0200
     3.2 +++ b/src/Pure/System/session.scala	Sat Aug 07 19:52:14 2010 +0200
     3.3 @@ -92,7 +92,7 @@
     3.4  
     3.5      /* document changes */
     3.6  
     3.7 -    def handle_change(change: Change)
     3.8 +    def handle_change(change: Document.Change)
     3.9      //{{{
    3.10      {
    3.11        require(change.parent.isDefined)
    3.12 @@ -244,7 +244,7 @@
    3.13              prover = null
    3.14            }
    3.15  
    3.16 -        case change: Change if prover != null =>
    3.17 +        case change: Document.Change if prover != null =>
    3.18            handle_change(change)
    3.19  
    3.20          case result: Isabelle_Process.Result =>
    3.21 @@ -315,8 +315,8 @@
    3.22  
    3.23    private val editor_history = new Actor
    3.24    {
    3.25 -    @volatile private var history = Change.init
    3.26 -    def current_change(): Change = history
    3.27 +    @volatile private var history = Document.Change.init
    3.28 +    def current_change(): Document.Change = history
    3.29  
    3.30      def act
    3.31      {
    3.32 @@ -331,7 +331,7 @@
    3.33                  old_doc.await_assignment
    3.34                  Document.text_edits(Session.this, old_doc, new_id, edits)
    3.35                }
    3.36 -            val new_change = new Change(new_id, Some(old_change), edits, result)
    3.37 +            val new_change = new Document.Change(new_id, Some(old_change), edits, result)
    3.38              history = new_change
    3.39              new_change.result.map(_ => session_actor ! new_change)
    3.40  
    3.41 @@ -351,6 +351,6 @@
    3.42  
    3.43    def stop() { session_actor ! Stop }
    3.44  
    3.45 -  def current_change(): Change = editor_history.current_change()
    3.46 +  def current_change(): Document.Change = editor_history.current_change()
    3.47    def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history ! Edit_Document(edits) }
    3.48  }
     4.1 --- a/src/Pure/build-jars	Sat Aug 07 17:24:46 2010 +0200
     4.2 +++ b/src/Pure/build-jars	Sat Aug 07 19:52:14 2010 +0200
     4.3 @@ -37,7 +37,6 @@
     4.4    Isar/outer_syntax.scala
     4.5    Isar/parse.scala
     4.6    Isar/token.scala
     4.7 -  PIDE/change.scala
     4.8    PIDE/command.scala
     4.9    PIDE/document.scala
    4.10    PIDE/event_bus.scala
     5.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 17:24:46 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 19:52:14 2010 +0200
     5.3 @@ -225,7 +225,7 @@
     5.4  
     5.5    /* snapshot */
     5.6  
     5.7 -  def snapshot(): Change.Snapshot = {
     5.8 +  def snapshot(): Document.Snapshot = {
     5.9      Swing_Thread.require()
    5.10      session.current_change().snapshot(thy_name, pending_edits.snapshot())
    5.11    }
     6.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat Aug 07 17:24:46 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Aug 07 19:52:14 2010 +0200
     6.3 @@ -24,7 +24,7 @@
     6.4  
     6.5  object Document_View
     6.6  {
     6.7 -  def choose_color(snapshot: Change.Snapshot, command: Command): Color =
     6.8 +  def choose_color(snapshot: Document.Snapshot, command: Command): Color =
     6.9    {
    6.10      val state = snapshot.document.current_state(command)
    6.11      if (snapshot.is_outdated) new Color(240, 240, 240)
    6.12 @@ -116,7 +116,7 @@
    6.13      }
    6.14    }
    6.15  
    6.16 -  def full_repaint(snapshot: Change.Snapshot, changed: Set[Command])
    6.17 +  def full_repaint(snapshot: Document.Snapshot, changed: Set[Command])
    6.18    {
    6.19      Swing_Thread.require()
    6.20  
    6.21 @@ -158,7 +158,8 @@
    6.22          if (range.hasNext) {
    6.23            val (cmd0, start0) = range.next
    6.24            new Iterable[(Command, Int)] {
    6.25 -            def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
    6.26 +            def iterator =
    6.27 +              Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
    6.28            }
    6.29          }
    6.30          else Iterable.empty