merged
authorwenzelm
Sun Feb 26 20:08:12 2012 +0100 (2012-02-26)
changeset 4669007f9732804ad
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.25 +    val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
    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.33 -    val header: Node_Header,
    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.39 +    def update_header(new_header: Node_Header): Node =
    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.22      val header = read(source)
    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.28      header
    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.28          case (name, Document.Node.Header(header)) =>
    8.29            val node = nodes(name)
    8.30 @@ -263,7 +263,7 @@
    8.31              }
    8.32            if (update_header) {
    8.33              doc_edits += (name -> Document.Node.Header(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.13      Swing_Thread.now {
    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