renamed class Document to Document.Version etc.;
authorwenzelm
Sun Aug 15 14:18:52 2010 +0200 (2010-08-15)
changeset 38417b8922ae21111
parent 38416 56e76cd46b4f
child 38418 9a7af64d71bb
renamed class Document to Document.Version etc.;
renamed Change.prev to Change.previous, and Change.document to Change.current;
tuned;
src/Pure/PIDE/document.scala
src/Pure/System/isar_document.ML
src/Pure/System/isar_document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sun Aug 15 13:17:45 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 15 14:18:52 2010 +0200
     1.3 @@ -78,9 +78,14 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* initial document */
     1.8 +  /* document versions */
     1.9  
    1.10 -  val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty))
    1.11 +  object Version
    1.12 +  {
    1.13 +    val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty))
    1.14 +  }
    1.15 +
    1.16 +  class Version(val id: Version_ID, val nodes: Map[String, Node])
    1.17  
    1.18  
    1.19  
    1.20 @@ -94,8 +99,8 @@
    1.21  
    1.22    abstract class Snapshot
    1.23    {
    1.24 -    val document: Document
    1.25 -    val node: Document.Node
    1.26 +    val version: Version
    1.27 +    val node: Node
    1.28      val is_outdated: Boolean
    1.29      def convert(offset: Int): Int
    1.30      def revert(offset: Int): Int
    1.31 @@ -105,16 +110,16 @@
    1.32  
    1.33    object Change
    1.34    {
    1.35 -    val init = new Change(Future.value(Document.init), Nil, Future.value(Nil, Document.init))
    1.36 +    val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init))
    1.37    }
    1.38  
    1.39    class Change(
    1.40 -    val prev: Future[Document],
    1.41 +    val previous: Future[Version],
    1.42      val edits: List[Node_Text_Edit],
    1.43 -    val result: Future[(List[Edit[Command]], Document)])
    1.44 +    val result: Future[(List[Edit[Command]], Version)])
    1.45    {
    1.46 -    val document: Future[Document] = result.map(_._2)
    1.47 -    def is_finished: Boolean = prev.is_finished && document.is_finished
    1.48 +    val current: Future[Version] = result.map(_._2)
    1.49 +    def is_finished: Boolean = previous.is_finished && current.is_finished
    1.50    }
    1.51  
    1.52  
    1.53 @@ -125,7 +130,7 @@
    1.54    {
    1.55      class Fail(state: State) extends Exception
    1.56  
    1.57 -    val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
    1.58 +    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
    1.59  
    1.60      class Assignment(former_assignment: Map[Command, Exec_ID])
    1.61      {
    1.62 @@ -142,20 +147,20 @@
    1.63    }
    1.64  
    1.65    case class State(
    1.66 -    val documents: Map[Version_ID, Document] = Map(),
    1.67 +    val versions: Map[Version_ID, Version] = Map(),
    1.68      val commands: Map[Command_ID, Command.State] = Map(),
    1.69 -    val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
    1.70 -    val assignments: Map[Document, State.Assignment] = Map(),
    1.71 +    val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
    1.72 +    val assignments: Map[Version, State.Assignment] = Map(),
    1.73      val disposed: Set[ID] = Set())  // FIXME unused!?
    1.74    {
    1.75      private def fail[A]: A = throw new State.Fail(this)
    1.76  
    1.77 -    def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
    1.78 +    def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State =
    1.79      {
    1.80 -      val id = document.id
    1.81 -      if (documents.isDefinedAt(id) || disposed(id)) fail
    1.82 -      copy(documents = documents + (id -> document),
    1.83 -        assignments = assignments + (document -> new State.Assignment(former_assignment)))
    1.84 +      val id = version.id
    1.85 +      if (versions.isDefinedAt(id) || disposed(id)) fail
    1.86 +      copy(versions = versions + (id -> version),
    1.87 +        assignments = assignments + (version -> new State.Assignment(former_assignment)))
    1.88      }
    1.89  
    1.90      def define_command(command: Command): State =
    1.91 @@ -167,16 +172,16 @@
    1.92  
    1.93      def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
    1.94  
    1.95 -    def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
    1.96 +    def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
    1.97      def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
    1.98      def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
    1.99 -    def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
   1.100 +    def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
   1.101  
   1.102      def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
   1.103        execs.get(id) match {
   1.104 -        case Some((st, docs)) =>
   1.105 +        case Some((st, occs)) =>
   1.106            val new_st = st.accumulate(message)
   1.107 -          (new_st, copy(execs = execs + (id -> (new_st, docs))))
   1.108 +          (new_st, copy(execs = execs + (id -> (new_st, occs))))
   1.109          case None =>
   1.110            commands.get(id) match {
   1.111              case Some(st) =>
   1.112 @@ -188,38 +193,33 @@
   1.113  
   1.114      def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
   1.115      {
   1.116 -      val doc = the_document(id)
   1.117 -      val docs = Set(doc)  // FIXME unused (!?)
   1.118 +      val version = the_version(id)
   1.119 +      val occs = Set(version)  // FIXME unused (!?)
   1.120  
   1.121        var new_execs = execs
   1.122        val assigned_execs =
   1.123          for ((cmd_id, exec_id) <- edits) yield {
   1.124            val st = the_command(cmd_id)
   1.125            if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
   1.126 -          new_execs += (exec_id -> (st, docs))
   1.127 +          new_execs += (exec_id -> (st, occs))
   1.128            (st.command, exec_id)
   1.129          }
   1.130 -      the_assignment(doc).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
   1.131 +      the_assignment(version).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
   1.132        copy(execs = new_execs)
   1.133      }
   1.134  
   1.135 -    def is_assigned(document: Document): Boolean =
   1.136 -      assignments.get(document) match {
   1.137 +    def is_assigned(version: Version): Boolean =
   1.138 +      assignments.get(version) match {
   1.139          case Some(assgn) => assgn.is_finished
   1.140          case None => false
   1.141        }
   1.142  
   1.143 -    def command_state(document: Document, command: Command): Command.State =
   1.144 +    def command_state(version: Version, command: Command): Command.State =
   1.145      {
   1.146 -      val assgn = the_assignment(document)
   1.147 +      val assgn = the_assignment(version)
   1.148        require(assgn.is_finished)
   1.149        the_exec_state(assgn.join.getOrElse(command, fail))
   1.150      }
   1.151    }
   1.152  }
   1.153  
   1.154 -
   1.155 -class Document(
   1.156 -    val id: Document.Version_ID,
   1.157 -    val nodes: Map[String, Document.Node])
   1.158 -
     2.1 --- a/src/Pure/System/isar_document.ML	Sun Aug 15 13:17:45 2010 +0200
     2.2 +++ b/src/Pure/System/isar_document.ML	Sun Aug 15 14:18:52 2010 +0200
     2.3 @@ -27,11 +27,11 @@
     2.4  fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
     2.5  
     2.6  
     2.7 -(** documents **)
     2.8 +(** document versions **)
     2.9  
    2.10  datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
    2.11  type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
    2.12 -type document = node Graph.T;   (*development graph via static imports*)
    2.13 +type version = node Graph.T;   (*development graph via static imports*)
    2.14  
    2.15  
    2.16  (* command entries *)
    2.17 @@ -97,8 +97,8 @@
    2.18  
    2.19  val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
    2.20  
    2.21 -fun the_node (document: document) name =
    2.22 -  Graph.get_node document name handle Graph.UNDEF _ => empty_node;
    2.23 +fun the_node (version: version) name =
    2.24 +  Graph.get_node version name handle Graph.UNDEF _ => empty_node;
    2.25  
    2.26  fun edit_node (id, SOME id2) = insert_after id id2
    2.27    | edit_node (id, NONE) = delete_after id;
    2.28 @@ -166,19 +166,19 @@
    2.29  
    2.30  local
    2.31  
    2.32 -val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
    2.33 +val global_versions = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: version)]);
    2.34  
    2.35  in
    2.36  
    2.37 -fun define_document (id: Document.version_id) document =
    2.38 +fun define_version (id: Document.version_id) version =
    2.39    NAMED_CRITICAL "Isar" (fn () =>
    2.40 -    Unsynchronized.change global_documents (Inttab.update_new (id, document))
    2.41 -      handle Inttab.DUP dup => err_dup "document" dup);
    2.42 +    Unsynchronized.change global_versions (Inttab.update_new (id, version))
    2.43 +      handle Inttab.DUP dup => err_dup "version" dup);
    2.44  
    2.45 -fun the_document (id: Document.version_id) =
    2.46 -  (case Inttab.lookup (! global_documents) id of
    2.47 -    NONE => err_undef "document" id
    2.48 -  | SOME document => document);
    2.49 +fun the_version (id: Document.version_id) =
    2.50 +  (case Inttab.lookup (! global_versions) id of
    2.51 +    NONE => err_undef "version" id
    2.52 +  | SOME version => version);
    2.53  
    2.54  end;
    2.55  
    2.56 @@ -197,20 +197,20 @@
    2.57  
    2.58  in
    2.59  
    2.60 -fun execute document =
    2.61 +fun execute version =
    2.62    NAMED_CRITICAL "Isar" (fn () =>
    2.63      let
    2.64        val old_execution = ! execution;
    2.65        val _ = List.app Future.cancel old_execution;
    2.66        fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
    2.67        (* FIXME proper node deps *)
    2.68 -      val new_execution = Graph.keys document |> map (fn name =>
    2.69 +      val new_execution = Graph.keys version |> map (fn name =>
    2.70          Future.fork_pri 1 (fn () =>
    2.71            let
    2.72              val _ = await_cancellation ();
    2.73              val exec =
    2.74                fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
    2.75 -                (the_node document name);
    2.76 +                (the_node version name);
    2.77            in exec () end));
    2.78      in execution := new_execution end);
    2.79  
    2.80 @@ -249,11 +249,11 @@
    2.81  fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
    2.82    NAMED_CRITICAL "Isar" (fn () =>
    2.83      let
    2.84 -      val old_document = the_document old_id;
    2.85 -      val new_document = fold edit_nodes edits old_document;
    2.86 +      val old_version = the_version old_id;
    2.87 +      val new_version = fold edit_nodes edits old_version;
    2.88  
    2.89        fun update_node name node =
    2.90 -        (case first_entry (is_changed (the_node old_document name)) node of
    2.91 +        (case first_entry (is_changed (the_node old_version name)) node of
    2.92            NONE => ([], node)
    2.93          | SOME (prev, id, _) =>
    2.94              let
    2.95 @@ -263,13 +263,13 @@
    2.96              in (rev updates, node') end);
    2.97  
    2.98        (* FIXME proper node deps *)
    2.99 -      val (updatess, new_document') =
   2.100 -        (Graph.keys new_document, new_document)
   2.101 +      val (updatess, new_version') =
   2.102 +        (Graph.keys new_version, new_version)
   2.103            |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
   2.104  
   2.105 -      val _ = define_document new_id new_document';
   2.106 +      val _ = define_version new_id new_version';
   2.107        val _ = updates_status new_id (flat updatess);
   2.108 -      val _ = execute new_document';
   2.109 +      val _ = execute new_version';
   2.110      in () end);
   2.111  
   2.112  end;
   2.113 @@ -283,7 +283,7 @@
   2.114      (fn [id, text] => define_command (Document.parse_id id) text);
   2.115  
   2.116  val _ =
   2.117 -  Isabelle_Process.add_command "Isar_Document.edit_document"
   2.118 +  Isabelle_Process.add_command "Isar_Document.edit_version"
   2.119      (fn [old_id, new_id, edits] =>
   2.120        edit_document (Document.parse_id old_id) (Document.parse_id new_id)
   2.121          (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
     3.1 --- a/src/Pure/System/isar_document.scala	Sun Aug 15 13:17:45 2010 +0200
     3.2 +++ b/src/Pure/System/isar_document.scala	Sun Aug 15 14:18:52 2010 +0200
     3.3 @@ -46,9 +46,9 @@
     3.4      input("Isar_Document.define_command", Document.ID(id), text)
     3.5  
     3.6  
     3.7 -  /* documents */
     3.8 +  /* document versions */
     3.9  
    3.10 -  def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
    3.11 +  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
    3.12        edits: List[Document.Edit[Document.Command_ID]])
    3.13    {
    3.14      def make_id1(id1: Option[Document.Command_ID]): XML.Body =
    3.15 @@ -60,7 +60,7 @@
    3.16            XML_Data.make_option(XML_Data.make_list(
    3.17                XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
    3.18  
    3.19 -    input("Isar_Document.edit_document",
    3.20 +    input("Isar_Document.edit_version",
    3.21        Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
    3.22    }
    3.23  }
     4.1 --- a/src/Pure/System/session.scala	Sun Aug 15 13:17:45 2010 +0200
     4.2 +++ b/src/Pure/System/session.scala	Sun Aug 15 14:18:52 2010 +0200
     4.3 @@ -81,14 +81,14 @@
     4.4      {
     4.5        require(change.is_finished)
     4.6  
     4.7 -      val old_doc = change.prev.join
     4.8 -      val (node_edits, doc) = change.result.join
     4.9 +      val previous = change.previous.join
    4.10 +      val (node_edits, current) = change.result.join
    4.11  
    4.12 -      var former_assignment = current_state().the_assignment(old_doc).join
    4.13 +      var former_assignment = current_state().the_assignment(previous).join
    4.14        for {
    4.15          (name, Some(cmd_edits)) <- node_edits
    4.16          (prev, None) <- cmd_edits
    4.17 -        removed <- old_doc.nodes(name).commands.get_after(prev)
    4.18 +        removed <- previous.nodes(name).commands.get_after(prev)
    4.19        } former_assignment -= removed
    4.20  
    4.21        val id_edits =
    4.22 @@ -113,8 +113,8 @@
    4.23                }
    4.24              (name -> Some(ids))
    4.25          }
    4.26 -      change_state(_.define_document(doc, former_assignment))
    4.27 -      prover.edit_document(old_doc.id, doc.id, id_edits)
    4.28 +      change_state(_.define_version(current, former_assignment))
    4.29 +      prover.edit_version(previous.id, current.id, id_edits)
    4.30      }
    4.31      //}}}
    4.32  
    4.33 @@ -142,8 +142,8 @@
    4.34          case None =>
    4.35            if (result.is_status) {
    4.36              result.body match {
    4.37 -              case List(Isar_Document.Assign(doc_id, edits)) =>
    4.38 -                try { change_state(_.assign(doc_id, edits)) }
    4.39 +              case List(Isar_Document.Assign(id, edits)) =>
    4.40 +                try { change_state(_.assign(id, edits)) }
    4.41                  catch { case _: Document.State.Fail => bad_result(result) }
    4.42                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    4.43                case List(Keyword.Keyword_Decl(name)) => syntax += name
    4.44 @@ -286,7 +286,7 @@
    4.45  
    4.46    /** editor history **/
    4.47  
    4.48 -  private case class Edit_Document(edits: List[Document.Node_Text_Edit])
    4.49 +  private case class Edit_Version(edits: List[Document.Node_Text_Edit])
    4.50  
    4.51    private val editor_history = new Actor
    4.52    {
    4.53 @@ -298,7 +298,7 @@
    4.54        val history_snapshot = history
    4.55  
    4.56        val found_stable = history_snapshot.find(change =>
    4.57 -        change.is_finished && state_snapshot.is_assigned(change.document.join))
    4.58 +        change.is_finished && state_snapshot.is_assigned(change.current.join))
    4.59        require(found_stable.isDefined)
    4.60        val stable = found_stable.get
    4.61        val latest = history_snapshot.head
    4.62 @@ -309,15 +309,15 @@
    4.63        lazy val reverse_edits = edits.reverse
    4.64  
    4.65        new Document.Snapshot {
    4.66 -        val document = stable.document.join
    4.67 -        val node = document.nodes(name)
    4.68 +        val version = stable.current.join
    4.69 +        val node = version.nodes(name)
    4.70          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    4.71          def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
    4.72          def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    4.73          def lookup_command(id: Document.Command_ID): Option[Command] =
    4.74            state_snapshot.lookup_command(id)
    4.75          def state(command: Command): Command.State =
    4.76 -          try { state_snapshot.command_state(document, command) }
    4.77 +          try { state_snapshot.command_state(version, command) }
    4.78            catch { case _: Document.State.Fail => command.empty_state }
    4.79        }
    4.80      }
    4.81 @@ -326,20 +326,20 @@
    4.82      {
    4.83        loop {
    4.84          react {
    4.85 -          case Edit_Document(edits) =>
    4.86 +          case Edit_Version(edits) =>
    4.87              val history_snapshot = history
    4.88              require(!history_snapshot.isEmpty)
    4.89  
    4.90 -            val prev = history_snapshot.head.document
    4.91 -            val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
    4.92 +            val prev = history_snapshot.head.current
    4.93 +            val result =
    4.94                isabelle.Future.fork {
    4.95 -                val old_doc = prev.join
    4.96 -                val former_assignment = current_state().the_assignment(old_doc).join  // FIXME async!?
    4.97 -                Thy_Syntax.text_edits(Session.this, old_doc, edits)
    4.98 +                val previous = prev.join
    4.99 +                val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
   4.100 +                Thy_Syntax.text_edits(Session.this, previous, edits)
   4.101                }
   4.102              val new_change = new Document.Change(prev, edits, result)
   4.103              history ::= new_change
   4.104 -            new_change.document.map(_ => session_actor ! new_change)
   4.105 +            new_change.current.map(_ => session_actor ! new_change)
   4.106              reply(())
   4.107  
   4.108            case bad => System.err.println("editor_model: ignoring bad message " + bad)
   4.109 @@ -361,5 +361,5 @@
   4.110    def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   4.111      editor_history.snapshot(name, pending_edits)
   4.112  
   4.113 -  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
   4.114 +  def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
   4.115  }
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 13:17:45 2010 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 14:18:52 2010 +0200
     5.3 @@ -38,8 +38,8 @@
     5.4  
     5.5    /** text edits **/
     5.6  
     5.7 -  def text_edits(session: Session, old_doc: Document, edits: List[Document.Node_Text_Edit])
     5.8 -      : (List[Document.Edit[Command]], Document) =
     5.9 +  def text_edits(session: Session, previous: Document.Version,
    5.10 +      edits: List[Document.Node_Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
    5.11    {
    5.12      /* phase 1: edit individual command source */
    5.13  
    5.14 @@ -110,7 +110,7 @@
    5.15  
    5.16      {
    5.17        val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
    5.18 -      var nodes = old_doc.nodes
    5.19 +      var nodes = previous.nodes
    5.20  
    5.21        for ((name, text_edits) <- edits) {
    5.22          val commands0 = nodes(name).commands
    5.23 @@ -127,7 +127,7 @@
    5.24          doc_edits += (name -> Some(cmd_edits))
    5.25          nodes += (name -> new Document.Node(commands2))
    5.26        }
    5.27 -      (doc_edits.toList, new Document(session.create_id(), nodes))
    5.28 +      (doc_edits.toList, new Document.Version(session.create_id(), nodes))
    5.29      }
    5.30    }
    5.31  }
     6.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 13:17:45 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 14:18:52 2010 +0200
     6.3 @@ -203,7 +203,7 @@
     6.4      def snapshot(): List[Text_Edit] = pending.toList
     6.5  
     6.6      private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
     6.7 -      if (!pending.isEmpty) session.edit_document(List((thy_name, flush())))
     6.8 +      if (!pending.isEmpty) session.edit_version(List((thy_name, flush())))
     6.9      }
    6.10  
    6.11      def flush(): List[Text_Edit] =
    6.12 @@ -225,7 +225,8 @@
    6.13  
    6.14    /* snapshot */
    6.15  
    6.16 -  def snapshot(): Document.Snapshot = {
    6.17 +  def snapshot(): Document.Snapshot =
    6.18 +  {
    6.19      Swing_Thread.require()
    6.20      session.snapshot(thy_name, pending_edits.snapshot())
    6.21    }
     7.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 15 13:17:45 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 15 14:18:52 2010 +0200
     7.3 @@ -95,9 +95,9 @@
     7.4      import Isabelle_Sidekick.int_to_pos
     7.5  
     7.6      val root = data.root
     7.7 -    val doc = Swing_Thread.now { model.snapshot().node }  // FIXME cover all nodes (!??)
     7.8 +    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     7.9      for {
    7.10 -      (command, command_start) <- doc.command_range(0)
    7.11 +      (command, command_start) <- snapshot.node.command_range(0)
    7.12        if command.is_command && !stopped
    7.13      }
    7.14      {
    7.15 @@ -113,8 +113,7 @@
    7.16            override def getStart: Position = command_start
    7.17            override def setEnd(end: Position) = ()
    7.18            override def getEnd: Position = command_start + command.length
    7.19 -          override def toString = name
    7.20 -        })
    7.21 +          override def toString = name})
    7.22        root.add(node)
    7.23      }
    7.24    }