author wenzelm Sun Feb 26 20:08:12 2012 +0100 (2012-02-26) changeset 46690 07f9732804ad parent 46689 f559866a7aa2 parent 46688 134982ee4ecb child 46691 72d81e789106 child 46698 f1dfcf8be88d
merged
```     1.1 --- a/src/HOL/ex/CTL.thy	Sun Feb 26 15:28:48 2012 +0100
1.2 +++ b/src/HOL/ex/CTL.thy	Sun Feb 26 20:08:12 2012 +0100
1.3 @@ -4,7 +4,9 @@
1.4
1.5  header {* CTL formulae *}
1.6
1.7 -theory CTL imports Main begin
1.8 +theory CTL
1.9 +imports Main
1.10 +begin
1.11
1.12  text {*
1.13    We formalize basic concepts of Computational Tree Logic (CTL)
1.14 @@ -127,19 +129,19 @@
1.15
1.16  lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
1.17  proof -
1.18 -  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
1.19 +  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
1.20    then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
1.21  qed
1.22
1.23  lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
1.24  proof -
1.25 -  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
1.26 +  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
1.27    then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
1.28  qed
1.29
1.30  lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
1.31  proof -
1.32 -  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
1.33 +  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
1.34    then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
1.35  qed
1.36
1.37 @@ -152,7 +154,7 @@
1.38
1.39  lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
1.40  proof -
1.41 -  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
1.42 +  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
1.43    then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
1.44  qed
1.45
```
```     2.1 --- a/src/Pure/Concurrent/volatile.scala	Sun Feb 26 15:28:48 2012 +0100
2.2 +++ b/src/Pure/Concurrent/volatile.scala	Sun Feb 26 20:08:12 2012 +0100
2.3 @@ -18,8 +18,8 @@
2.4  {
2.5    @volatile private var state: A = init
2.6    def apply(): A = state
2.7 -  def change(f: A => A) { state = f(state) }
2.8 -  def change_yield[B](f: A => (B, A)): B =
2.9 +  def >> (f: A => A) { state = f(state) }
2.10 +  def >>>[B] (f: A => (B, A)): B =
2.11    {
2.12      val (result, new_state) = f(state)
2.13      state = new_state
```
```     3.1 --- a/src/Pure/General/linear_set.scala	Sun Feb 26 15:28:48 2012 +0100
3.2 +++ b/src/Pure/General/linear_set.scala	Sun Feb 26 20:08:12 2012 +0100
3.3 @@ -1,4 +1,5 @@
3.4  /*  Title:      Pure/General/linear_set.scala
3.5 +    Module:     PIDE
3.6      Author:     Makarius
3.7      Author:     Fabian Immler, TU Munich
3.8
```
```     4.1 --- a/src/Pure/PIDE/document.scala	Sun Feb 26 15:28:48 2012 +0100
4.2 +++ b/src/Pure/PIDE/document.scala	Sun Feb 26 20:08:12 2012 +0100
4.3 @@ -82,9 +82,6 @@
4.4          case exn => exn
4.5        }
4.6
4.7 -    val empty: Node =
4.8 -      Node(Exn.Exn(ERROR("Bad theory header")), Command.Perspective.empty, Map(), Linear_Set())
4.9 -
4.10      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
4.11        : Iterator[(Command, Text.Offset)] =
4.12      {
4.13 @@ -95,17 +92,31 @@
4.14          (command, start)
4.15        }
4.16      }
4.17 +
4.18 +    private val block_size = 1024
4.19 +
4.20 +    val empty: Node = new Node()
4.21    }
4.22
4.23 -  private val block_size = 1024
4.24 +  class Node private(
4.26 +    val perspective: Command.Perspective = Command.Perspective.empty,
4.27 +    val blobs: Map[String, Blob] = Map.empty,
4.28 +    val commands: Linear_Set[Command] = Linear_Set.empty)
4.29 +  {
4.30 +    def clear: Node = new Node(header = header)
4.31
4.32 -  sealed case class Node(
4.34 -    val perspective: Command.Perspective,
4.35 -    val blobs: Map[String, Blob],
4.36 -    val commands: Linear_Set[Command])
4.37 -  {
4.38 -    def clear: Node = Node.empty.copy(header = header)
4.40 +      new Node(new_header, perspective, blobs, commands)
4.41 +
4.42 +    def update_perspective(new_perspective: Command.Perspective): Node =
4.43 +      new Node(header, new_perspective, blobs, commands)
4.44 +
4.45 +    def update_blobs(new_blobs: Map[String, Blob]): Node =
4.46 +      new Node(header, perspective, new_blobs, commands)
4.47 +
4.48 +    def update_commands(new_commands: Linear_Set[Command]): Node =
4.49 +      new Node(header, perspective, blobs, new_commands)
4.50
4.51
4.52      /* commands */
4.53 @@ -119,7 +130,7 @@
4.54          last_stop = start + command.length
4.55          while (last_stop + 1 > next_block) {
4.56            blocks += (command -> start)
4.57 -          next_block += block_size
4.58 +          next_block += Node.block_size
4.59          }
4.60        }
4.61        (blocks.toArray, Text.Range(0, last_stop))
4.62 @@ -130,7 +141,7 @@
4.63      def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
4.64      {
4.65        if (!commands.isEmpty && full_range.contains(i)) {
4.66 -        val (cmd0, start0) = full_index._1(i / block_size)
4.67 +        val (cmd0, start0) = full_index._1(i / Node.block_size)
4.68          Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
4.69            case (cmd, start) => start + cmd.length <= i }
4.70        }
4.71 @@ -154,10 +165,7 @@
4.72        }
4.73
4.74      def command_start(cmd: Command): Option[Text.Offset] =
4.75 -      command_starts.find(_._1 == cmd).map(_._2)
4.76 -
4.77 -    def command_starts: Iterator[(Command, Text.Offset)] =
4.78 -      Node.command_starts(commands.iterator)
4.79 +      Node.command_starts(commands.iterator).find(_._1 == cmd).map(_._2)
4.80    }
4.81
4.82
4.83 @@ -166,13 +174,18 @@
4.84
4.85    /* particular document versions */
4.86
4.87 +  type Nodes = Map[Node.Name, Node]
4.88 +
4.89    object Version
4.90    {
4.91 -    val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
4.92 +    val init: Version = new Version()
4.93 +
4.94 +    def make(nodes: Nodes): Version = new Version(new_id(), nodes)
4.95    }
4.96
4.97 -  type Nodes = Map[Node.Name, Node]
4.98 -  sealed case class Version(val id: Version_ID, val nodes: Nodes)
4.99 +  class Version private(
4.100 +    val id: Version_ID = no_id,
4.101 +    val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
4.102    {
4.103      def topological_order: List[Node.Name] =
4.104      {
4.105 @@ -192,19 +205,22 @@
4.106
4.107    object Change
4.108    {
4.109 -    val init: Change = Change(Some(Future.value(Version.init)), Nil, Future.value(Version.init))
4.110 +    val init: Change = new Change()
4.111 +
4.112 +    def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
4.113 +      new Change(Some(previous), edits, version)
4.114    }
4.115
4.116 -  sealed case class Change(
4.117 -    val previous: Option[Future[Version]],
4.118 -    val edits: List[Edit_Text],
4.119 -    val version: Future[Version])
4.120 +  class Change private(
4.121 +    val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
4.122 +    val edits: List[Edit_Text] = Nil,
4.123 +    val version: Future[Version] = Future.value(Version.init))
4.124    {
4.125      def is_finished: Boolean =
4.126        (previous match { case None => true case Some(future) => future.is_finished }) &&
4.127        version.is_finished
4.128
4.129 -    def truncate: Change = copy(previous = None, edits = Nil)
4.130 +    def truncate: Change = new Change(None, Nil, version)
4.131    }
4.132
4.133
4.134 @@ -212,16 +228,25 @@
4.135
4.136    object History
4.137    {
4.138 -    val init: History = History(List(Change.init))
4.139 +    val init: History = new History()
4.140    }
4.141
4.142 -  // FIXME pruning, purging of state
4.143 -  sealed case class History(val undo_list: List[Change])
4.144 +  class History private(
4.145 +    val undo_list: List[Change] = List(Change.init))  // non-empty list
4.146    {
4.147 -    require(!undo_list.isEmpty)
4.148 +    def tip: Change = undo_list.head
4.149 +    def + (change: Change): History = new History(change :: undo_list)
4.150
4.151 -    def tip: Change = undo_list.head
4.152 -    def +(change: Change): History = copy(undo_list = change :: undo_list)
4.153 +    def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] =
4.154 +    {
4.155 +      val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1
4.156 +      val (retained, dropped) = undo_list.splitAt(n max retain)
4.157 +
4.158 +      retained.splitAt(retained.length - 1) match {
4.159 +        case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate)))
4.160 +        case _ => None
4.161 +      }
4.162 +    }
4.163    }
4.164
4.165
4.166 @@ -248,27 +273,22 @@
4.167     (List[(Document.Command_ID, Option[Document.Exec_ID])],  // exec state assignment
4.168      List[(String, Option[Document.Command_ID])])  // last exec
4.169
4.170 -  val no_assign: Assign = (Nil, Nil)
4.171 -
4.172    object State
4.173    {
4.174      class Fail(state: State) extends Exception
4.175
4.176 -    val init: State =
4.177 -      State().define_version(Version.init, Assignment.init).assign(Version.init.id, no_assign)._2
4.178 -
4.179      object Assignment
4.180      {
4.181 -      val init: Assignment = Assignment(Map.empty, Map.empty, false)
4.182 +      val init: Assignment = new Assignment()
4.183      }
4.184
4.185 -    case class Assignment(
4.186 -      val command_execs: Map[Command_ID, Exec_ID],
4.187 -      val last_execs: Map[String, Option[Command_ID]],
4.188 -      val is_finished: Boolean)
4.189 +    class Assignment private(
4.190 +      val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
4.191 +      val last_execs: Map[String, Option[Command_ID]] = Map.empty,
4.192 +      val is_finished: Boolean = false)
4.193      {
4.194        def check_finished: Assignment = { require(is_finished); this }
4.195 -      def unfinished: Assignment = copy(is_finished = false)
4.196 +      def unfinished: Assignment = new Assignment(command_execs, last_execs, false)
4.197
4.198        def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
4.199          add_last_execs: List[(String, Option[Command_ID])]): Assignment =
4.200 @@ -279,16 +299,19 @@
4.201              case (res, (command_id, None)) => res - command_id
4.202              case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
4.203            }
4.204 -        Assignment(command_execs1, last_execs ++ add_last_execs, true)
4.205 +        new Assignment(command_execs1, last_execs ++ add_last_execs, true)
4.206        }
4.207      }
4.208 +
4.209 +    val init: State =
4.210 +      State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
4.211    }
4.212
4.213 -  sealed case class State(
4.214 -    val versions: Map[Version_ID, Version] = Map(),
4.215 -    val commands: Map[Command_ID, Command.State] = Map(),  // static markup from define_command
4.216 -    val execs: Map[Exec_ID, Command.State] = Map(),  // dynamic markup from execution
4.217 -    val assignments: Map[Version_ID, State.Assignment] = Map(),
4.218 +  sealed case class State private(
4.219 +    val versions: Map[Version_ID, Version] = Map.empty,
4.220 +    val commands: Map[Command_ID, Command.State] = Map.empty,  // static markup from define_command
4.221 +    val execs: Map[Exec_ID, Command.State] = Map.empty,  // dynamic markup from execution
4.222 +    val assignments: Map[Version_ID, State.Assignment] = Map.empty,
4.223      val history: History = History.init)
4.224    {
4.225      private def fail[A]: A = throw new State.Fail(this)
4.226 @@ -313,7 +336,8 @@
4.227          case None => None
4.228          case Some(st) =>
4.229            val command = st.command
4.230 -          version.nodes.get(command.node_name).map((_, command))
4.231 +          val node = version.nodes(command.node_name)
4.232 +          Some((node, command))
4.233        }
4.234
4.235      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
4.236 @@ -336,7 +360,7 @@
4.237            }
4.238        }
4.239
4.240 -    def assign(id: Version_ID, arg: Assign): (List[Command], State) =
4.241 +    def assign(id: Version_ID, arg: Assign = (Nil, Nil)): (List[Command], State) =
4.242      {
4.243        val version = the_version(id)
4.244        val (command_execs, last_execs) = arg
4.245 @@ -392,22 +416,18 @@
4.246          edits: List[Edit_Text],
4.247          version: Future[Version]): (Change, State) =
4.248      {
4.249 -      val change = Change(Some(previous), edits, version)
4.250 +      val change = Change.make(previous, edits, version)
4.251        (change, copy(history = history + change))
4.252      }
4.253
4.254      def prune_history(retain: Int = 0): (List[Version], State) =
4.255      {
4.256 -      val undo_list = history.undo_list
4.257 -      val n = undo_list.iterator.zipWithIndex.find(p => is_stable(p._1)).get._2 + 1
4.258 -      val (retained, dropped) = undo_list.splitAt(n max retain)
4.259 -
4.260 -      retained.splitAt(retained.length - 1) match {
4.261 -        case (prefix, List(last)) =>
4.262 +      history.prune(is_stable, retain) match {
4.263 +        case Some((dropped, history1)) =>
4.264            val dropped_versions = dropped.map(change => change.version.get_finished)
4.265 -          val state1 = copy(history = History(prefix ::: List(last.truncate)))
4.266 +          val state1 = copy(history = history1)
4.267            (dropped_versions, state1)
4.268 -        case _ => fail
4.269 +        case None => fail
4.270        }
4.271      }
4.272
```
```     5.1 --- a/src/Pure/PIDE/protocol.scala	Sun Feb 26 15:28:48 2012 +0100
5.2 +++ b/src/Pure/PIDE/protocol.scala	Sun Feb 26 20:08:12 2012 +0100
5.3 @@ -80,9 +80,10 @@
5.4
5.5    /* node status */
5.6
5.7 -  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
5.8 +  sealed case class Node_Status(
5.9 +    unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
5.10    {
5.11 -    def total: Int = unprocessed + running + finished + failed
5.12 +    def total: Int = unprocessed + running + finished + warned + failed
5.13    }
5.14
5.15    def node_status(
5.16 @@ -91,16 +92,21 @@
5.17      var unprocessed = 0
5.18      var running = 0
5.19      var finished = 0
5.20 +    var warned = 0
5.21      var failed = 0
5.22      node.commands.foreach(command =>
5.23        {
5.24 -        val status = command_status(state.command_state(version, command).status)
5.25 +        val st = state.command_state(version, command)
5.26 +        val status = command_status(st.status)
5.27          if (status.is_running) running += 1
5.28 -        else if (status.is_finished) finished += 1
5.29 +        else if (status.is_finished) {
5.30 +          if (st.results.exists(p => is_warning(p._2))) warned += 1
5.31 +          else finished += 1
5.32 +        }
5.33          else if (status.is_failed) failed += 1
5.34          else unprocessed += 1
5.35        })
5.36 -    Node_Status(unprocessed, running, finished, failed)
5.37 +    Node_Status(unprocessed, running, finished, warned, failed)
5.38    }
5.39
5.40
```
```     6.1 --- a/src/Pure/System/session.scala	Sun Feb 26 15:28:48 2012 +0100
6.2 +++ b/src/Pure/System/session.scala	Sun Feb 26 20:08:12 2012 +0100
6.3 @@ -262,12 +262,12 @@
6.4        val text_edits: List[Document.Edit_Text] =
6.5          List((name, Document.Node.Perspective(text_perspective)))
6.6        val change =
6.7 -        global_state.change_yield(
6.8 -          _.continue_history(Future.value(previous), text_edits, Future.value(version)))
6.9 +        global_state >>>
6.10 +          (_.continue_history(Future.value(previous), text_edits, Future.value(version)))
6.11
6.12        val assignment = global_state().the_assignment(previous).check_finished
6.13 -      global_state.change(_.define_version(version, assignment))
6.14 -      global_state.change_yield(_.assign(version.id, Document.no_assign))
6.15 +      global_state >> (_.define_version(version, assignment))
6.16 +      global_state >>> (_.assign(version.id))
6.17
6.18        prover.get.update_perspective(previous.id, version.id, name, perspective)
6.19      }
6.20 @@ -286,7 +286,7 @@
6.21
6.22        val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
6.23        val version = Future.promise[Document.Version]
6.24 -      val change = global_state.change_yield(_.continue_history(previous, text_edits, version))
6.25 +      val change = global_state >>> (_.continue_history(previous, text_edits, version))
6.26
6.27        change_parser ! Text_Edits(syntax, name, previous, text_edits, version)
6.28      }
6.29 @@ -298,7 +298,7 @@
6.30      def handle_assign(id: Document.Version_ID, assign: Document.Assign)
6.31      //{{{
6.32      {
6.33 -      val cmds = global_state.change_yield(_.assign(id, assign))
6.34 +      val cmds = global_state >>> (_.assign(id, assign))
6.35        for (cmd <- cmds) delay_commands_changed.invoke(cmd)
6.36      }
6.37      //}}}
6.38 @@ -309,7 +309,7 @@
6.39      def handle_removed(removed: List[Document.Version_ID])
6.40      //{{{
6.41      {
6.42 -      global_state.change(_.removed_versions(removed))
6.43 +      global_state >> (_.removed_versions(removed))
6.44      }
6.45      //}}}
6.46
6.47 @@ -327,7 +327,7 @@
6.48        def id_command(command: Command)
6.49        {
6.50          if (!global_state().defined_command(command.id)) {
6.51 -          global_state.change(_.define_command(command))
6.52 +          global_state >> (_.define_command(command))
6.53            prover.get.define_command(command)
6.54          }
6.55        }
6.56 @@ -337,7 +337,7 @@
6.57        }
6.58
6.59        val assignment = global_state().the_assignment(previous).check_finished
6.60 -      global_state.change(_.define_version(version, assignment))
6.61 +      global_state >> (_.define_version(version, assignment))
6.62        prover.get.update(previous.id, version.id, doc_edits)
6.63      }
6.64      //}}}
6.65 @@ -358,7 +358,7 @@
6.66
6.67          case Position.Id(state_id) if !result.is_raw =>
6.68            try {
6.69 -            val st = global_state.change_yield(_.accumulate(state_id, result.message))
6.70 +            val st = global_state >>> (_.accumulate(state_id, result.message))
6.71              delay_commands_changed.invoke(st.command)
6.72            }
6.73            catch {
6.74 @@ -374,7 +374,7 @@
6.75            }
6.76            // FIXME separate timeout event/message!?
6.77            if (prover.isDefined && System.currentTimeMillis() > prune_next) {
6.78 -            val old_versions = global_state.change_yield(_.prune_history(prune_size))
6.79 +            val old_versions = global_state >>> (_.prune_history(prune_size))
6.80              if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
6.81              prune_next = System.currentTimeMillis() + prune_delay.ms
6.82            }
6.83 @@ -441,7 +441,7 @@
6.84
6.85          case Stop =>
6.86            if (phase == Session.Ready) {
6.87 -            global_state.change(_ => Document.State.init)  // FIXME event bus!?
6.88 +            global_state >> (_ => Document.State.init)  // FIXME event bus!?
6.89              phase = Session.Shutdown
6.90              prover.get.terminate
6.91              prover = None
```
```     7.1 --- a/src/Pure/Thy/thy_header.scala	Sun Feb 26 15:28:48 2012 +0100
7.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Feb 26 20:08:12 2012 +0100
7.3 @@ -23,7 +23,7 @@
7.4    val USES = "uses"
7.5    val BEGIN = "begin"
7.6
7.7 -  val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
7.8 +  private val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
7.9
7.10
7.11    /* theory file name */
7.12 @@ -38,7 +38,6 @@
7.13      s match { case Thy_Name(name) => Some(name) case _ => None }
7.14
7.15    def thy_path(path: Path): Path = path.ext("thy")
7.16 -  def thy_path(name: String): Path = Path.basic(name).ext("thy")
7.17
7.18
7.19    /* header */
7.20 @@ -105,8 +104,8 @@
7.21    {
7.23      val name1 = header.name
7.24 -    if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
7.25 -    Path.explode(name)
7.26 +    val path = Path.explode(name)
7.27 +    if (name != name1) error("Bad file name " + thy_path(path) + " for theory " + quote(name1))
7.29    }
7.30  }
```
```     8.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 15:28:48 2012 +0100
8.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 20:08:12 2012 +0100
8.3 @@ -135,7 +135,7 @@
8.4      val perspective = command_perspective(node, text_perspective)
8.5      val new_nodes =
8.6        if (node.perspective same perspective) None
8.7 -      else Some(nodes + (name -> node.copy(perspective = perspective)))
8.8 +      else Some(nodes + (name -> node.update_perspective(perspective)))
8.9      (perspective, new_nodes)
8.10    }
8.11
8.12 @@ -145,7 +145,7 @@
8.13    {
8.14      val nodes = previous.nodes
8.15      val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
8.16 -    val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
8.17 +    val version = Document.Version.make(new_nodes getOrElse nodes)
8.18      (perspective, version)
8.19    }
8.20
8.21 @@ -252,7 +252,7 @@
8.22              inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
8.23
8.24            doc_edits += (name -> Document.Node.Edits(cmd_edits))
8.25 -          nodes += (name -> node.copy(commands = commands2))
8.26 +          nodes += (name -> node.update_commands(commands2))
8.27
8.29            val node = nodes(name)
8.30 @@ -263,7 +263,7 @@
8.31              }
8.32            if (update_header) {
8.34 -            nodes += (name -> node.copy(header = header))
8.35 +            nodes += (name -> node.update_header(header))
8.36            }
8.37
8.38          case (name, Document.Node.Perspective(text_perspective)) =>
8.39 @@ -274,7 +274,7 @@
8.40                nodes = nodes1
8.41            }
8.42        }
8.43 -      (doc_edits.toList, Document.Version(Document.new_id(), nodes))
8.44 +      (doc_edits.toList, Document.Version.make(nodes))
8.45      }
8.46    }
8.47  }
```
```     9.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 15:28:48 2012 +0100
9.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 20:08:12 2012 +0100
9.3 @@ -116,6 +116,7 @@
9.4              (n, color) <- List(
9.5                (st.unprocessed, Isabelle_Rendering.unprocessed1_color),
9.6                (st.running, Isabelle_Rendering.running_color),
9.7 +              (st.warned, Isabelle_Rendering.warning_color),
9.8                (st.failed, Isabelle_Rendering.error_color)) }
9.9            {
9.10              gfx.setColor(color)
9.11 @@ -146,14 +147,13 @@
9.12    {
9.14        val snapshot = Isabelle.session.snapshot()
9.15 -      val nodes = restriction getOrElse snapshot.version.nodes.keySet
9.16 +      val names = restriction getOrElse snapshot.version.nodes.keySet
9.17
9.18 -      var nodes_status1 = nodes_status
9.19 -      for {
9.20 -        name <- nodes
9.21 -        node <- snapshot.version.nodes.get(name)
9.22 -        val status = Protocol.node_status(snapshot.state, snapshot.version, node)
9.23 -      } nodes_status1 += (name -> status)
9.24 +      val nodes_status1 =
9.25 +        (nodes_status /: names)((status, name) => {
9.26 +          val node = snapshot.version.nodes(name)
9.27 +          status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node))
9.28 +        })
9.29
9.30        if (nodes_status != nodes_status1) {
9.31          nodes_status = nodes_status1
```