more abstract class Document.Version;
authorwenzelm
Sun Feb 26 17:44:09 2012 +0100 (2012-02-26 ago)
changeset 46681c083a3f621c0
parent 46680 234f1730582d
child 46682 4a74fbd6f28b
more abstract class Document.Version;
tuned (NB: Version.nodes is total);
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sun Feb 26 17:15:33 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Feb 26 17:44:09 2012 +0100
     1.3 @@ -178,10 +178,12 @@
     1.4  
     1.5    object Version
     1.6    {
     1.7 -    val init: Version = Version()
     1.8 +    val init: Version = new Version()
     1.9 +
    1.10 +    def make(nodes: Nodes): Version = new Version(new_id(), nodes)
    1.11    }
    1.12  
    1.13 -  sealed case class Version(
    1.14 +  class Version private(
    1.15      val id: Version_ID = no_id,
    1.16      val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
    1.17    {
    1.18 @@ -336,7 +338,8 @@
    1.19          case None => None
    1.20          case Some(st) =>
    1.21            val command = st.command
    1.22 -          version.nodes.get(command.node_name).map((_, command))
    1.23 +          val node = version.nodes(command.node_name)
    1.24 +          Some((node, command))
    1.25        }
    1.26  
    1.27      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 17:15:33 2012 +0100
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 17:44:09 2012 +0100
     2.3 @@ -145,7 +145,7 @@
     2.4    {
     2.5      val nodes = previous.nodes
     2.6      val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
     2.7 -    val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
     2.8 +    val version = Document.Version.make(new_nodes getOrElse nodes)
     2.9      (perspective, version)
    2.10    }
    2.11  
    2.12 @@ -274,7 +274,7 @@
    2.13                nodes = nodes1
    2.14            }
    2.15        }
    2.16 -      (doc_edits.toList, Document.Version(Document.new_id(), nodes))
    2.17 +      (doc_edits.toList, Document.Version.make(nodes))
    2.18      }
    2.19    }
    2.20  }
     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 17:15:33 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 17:44:09 2012 +0100
     3.3 @@ -146,14 +146,13 @@
     3.4    {
     3.5      Swing_Thread.now {
     3.6        val snapshot = Isabelle.session.snapshot()
     3.7 -      val nodes = restriction getOrElse snapshot.version.nodes.keySet
     3.8 +      val names = restriction getOrElse snapshot.version.nodes.keySet
     3.9  
    3.10 -      var nodes_status1 = nodes_status
    3.11 -      for {
    3.12 -        name <- nodes
    3.13 -        node <- snapshot.version.nodes.get(name)
    3.14 -        val status = Protocol.node_status(snapshot.state, snapshot.version, node)
    3.15 -      } nodes_status1 += (name -> status)
    3.16 +      val nodes_status1 =
    3.17 +        (nodes_status /: names)((status, name) => {
    3.18 +          val node = snapshot.version.nodes(name)
    3.19 +          status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node))
    3.20 +        })
    3.21  
    3.22        if (nodes_status != nodes_status1) {
    3.23          nodes_status = nodes_status1