# HG changeset patch
# User wenzelm
# Date 1330283292 -3600
# Node ID 07f9732804ad26d87b98b2b2b58788ab6291e4d2
# Parent  f559866a7aa280cfc03efdbb862f6bc53a9ae01d# Parent  134982ee4ecbdad210d29babccdfb77c7eb99aa3
merged

diff -r f559866a7aa2 -r 07f9732804ad src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Sun Feb 26 15:28:48 2012 +0100
+++ b/src/HOL/ex/CTL.thy	Sun Feb 26 20:08:12 2012 +0100
@@ -4,7 +4,9 @@
 
 header {* CTL formulae *}
 
-theory CTL imports Main begin
+theory CTL
+imports Main
+begin
 
 text {*
   We formalize basic concepts of Computational Tree Logic (CTL)
@@ -127,19 +129,19 @@
 
 lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
 proof -
-  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
+  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
   then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
 qed
 
 lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
 proof -
-  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
   then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
 qed
 
 lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
 proof -
-  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
+  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
 qed
 
@@ -152,7 +154,7 @@
 
 lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
 proof -
-  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
   then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
 qed
 
diff -r f559866a7aa2 -r 07f9732804ad src/Pure/Concurrent/volatile.scala
--- a/src/Pure/Concurrent/volatile.scala	Sun Feb 26 15:28:48 2012 +0100
+++ b/src/Pure/Concurrent/volatile.scala	Sun Feb 26 20:08:12 2012 +0100
@@ -18,8 +18,8 @@
 {
   @volatile private var state: A = init
   def apply(): A = state
-  def change(f: A => A) { state = f(state) }
-  def change_yield[B](f: A => (B, A)): B =
+  def >> (f: A => A) { state = f(state) }
+  def >>>[B] (f: A => (B, A)): B =
   {
     val (result, new_state) = f(state)
     state = new_state
diff -r f559866a7aa2 -r 07f9732804ad src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Sun Feb 26 15:28:48 2012 +0100
+++ b/src/Pure/General/linear_set.scala	Sun Feb 26 20:08:12 2012 +0100
@@ -1,4 +1,5 @@
 /*  Title:      Pure/General/linear_set.scala
+    Module:     PIDE
     Author:     Makarius
     Author:     Fabian Immler, TU Munich
 
diff -r f559866a7aa2 -r 07f9732804ad src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Feb 26 15:28:48 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Feb 26 20:08:12 2012 +0100
@@ -82,9 +82,6 @@
         case exn => exn
       }
 
-    val empty: Node =
-      Node(Exn.Exn(ERROR("Bad theory header")), Command.Perspective.empty, Map(), Linear_Set())
-
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
     {
@@ -95,17 +92,31 @@
         (command, start)
       }
     }
+
+    private val block_size = 1024
+
+    val empty: Node = new Node()
   }
 
-  private val block_size = 1024
+  class Node private(
+    val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
+    val perspective: Command.Perspective = Command.Perspective.empty,
+    val blobs: Map[String, Blob] = Map.empty,
+    val commands: Linear_Set[Command] = Linear_Set.empty)
+  {
+    def clear: Node = new Node(header = header)
 
-  sealed case class Node(
-    val header: Node_Header,
-    val perspective: Command.Perspective,
-    val blobs: Map[String, Blob],
-    val commands: Linear_Set[Command])
-  {
-    def clear: Node = Node.empty.copy(header = header)
+    def update_header(new_header: Node_Header): Node =
+      new Node(new_header, perspective, blobs, commands)
+
+    def update_perspective(new_perspective: Command.Perspective): Node =
+      new Node(header, new_perspective, blobs, commands)
+
+    def update_blobs(new_blobs: Map[String, Blob]): Node =
+      new Node(header, perspective, new_blobs, commands)
+
+    def update_commands(new_commands: Linear_Set[Command]): Node =
+      new Node(header, perspective, blobs, new_commands)
 
 
     /* commands */
@@ -119,7 +130,7 @@
         last_stop = start + command.length
         while (last_stop + 1 > next_block) {
           blocks += (command -> start)
-          next_block += block_size
+          next_block += Node.block_size
         }
       }
       (blocks.toArray, Text.Range(0, last_stop))
@@ -130,7 +141,7 @@
     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
     {
       if (!commands.isEmpty && full_range.contains(i)) {
-        val (cmd0, start0) = full_index._1(i / block_size)
+        val (cmd0, start0) = full_index._1(i / Node.block_size)
         Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
           case (cmd, start) => start + cmd.length <= i }
       }
@@ -154,10 +165,7 @@
       }
 
     def command_start(cmd: Command): Option[Text.Offset] =
-      command_starts.find(_._1 == cmd).map(_._2)
-
-    def command_starts: Iterator[(Command, Text.Offset)] =
-      Node.command_starts(commands.iterator)
+      Node.command_starts(commands.iterator).find(_._1 == cmd).map(_._2)
   }
 
 
@@ -166,13 +174,18 @@
 
   /* particular document versions */
 
+  type Nodes = Map[Node.Name, Node]
+
   object Version
   {
-    val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
+    val init: Version = new Version()
+
+    def make(nodes: Nodes): Version = new Version(new_id(), nodes)
   }
 
-  type Nodes = Map[Node.Name, Node]
-  sealed case class Version(val id: Version_ID, val nodes: Nodes)
+  class Version private(
+    val id: Version_ID = no_id,
+    val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
   {
     def topological_order: List[Node.Name] =
     {
@@ -192,19 +205,22 @@
 
   object Change
   {
-    val init: Change = Change(Some(Future.value(Version.init)), Nil, Future.value(Version.init))
+    val init: Change = new Change()
+
+    def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
+      new Change(Some(previous), edits, version)
   }
 
-  sealed case class Change(
-    val previous: Option[Future[Version]],
-    val edits: List[Edit_Text],
-    val version: Future[Version])
+  class Change private(
+    val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
+    val edits: List[Edit_Text] = Nil,
+    val version: Future[Version] = Future.value(Version.init))
   {
     def is_finished: Boolean =
       (previous match { case None => true case Some(future) => future.is_finished }) &&
       version.is_finished
 
-    def truncate: Change = copy(previous = None, edits = Nil)
+    def truncate: Change = new Change(None, Nil, version)
   }
 
 
@@ -212,16 +228,25 @@
 
   object History
   {
-    val init: History = History(List(Change.init))
+    val init: History = new History()
   }
 
-  // FIXME pruning, purging of state
-  sealed case class History(val undo_list: List[Change])
+  class History private(
+    val undo_list: List[Change] = List(Change.init))  // non-empty list
   {
-    require(!undo_list.isEmpty)
+    def tip: Change = undo_list.head
+    def + (change: Change): History = new History(change :: undo_list)
 
-    def tip: Change = undo_list.head
-    def +(change: Change): History = copy(undo_list = change :: undo_list)
+    def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] =
+    {
+      val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1
+      val (retained, dropped) = undo_list.splitAt(n max retain)
+
+      retained.splitAt(retained.length - 1) match {
+        case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate)))
+        case _ => None
+      }
+    }
   }
 
 
@@ -248,27 +273,22 @@
    (List[(Document.Command_ID, Option[Document.Exec_ID])],  // exec state assignment
     List[(String, Option[Document.Command_ID])])  // last exec
 
-  val no_assign: Assign = (Nil, Nil)
-
   object State
   {
     class Fail(state: State) extends Exception
 
-    val init: State =
-      State().define_version(Version.init, Assignment.init).assign(Version.init.id, no_assign)._2
-
     object Assignment
     {
-      val init: Assignment = Assignment(Map.empty, Map.empty, false)
+      val init: Assignment = new Assignment()
     }
 
-    case class Assignment(
-      val command_execs: Map[Command_ID, Exec_ID],
-      val last_execs: Map[String, Option[Command_ID]],
-      val is_finished: Boolean)
+    class Assignment private(
+      val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
+      val last_execs: Map[String, Option[Command_ID]] = Map.empty,
+      val is_finished: Boolean = false)
     {
       def check_finished: Assignment = { require(is_finished); this }
-      def unfinished: Assignment = copy(is_finished = false)
+      def unfinished: Assignment = new Assignment(command_execs, last_execs, false)
 
       def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
         add_last_execs: List[(String, Option[Command_ID])]): Assignment =
@@ -279,16 +299,19 @@
             case (res, (command_id, None)) => res - command_id
             case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
           }
-        Assignment(command_execs1, last_execs ++ add_last_execs, true)
+        new Assignment(command_execs1, last_execs ++ add_last_execs, true)
       }
     }
+
+    val init: State =
+      State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
   }
 
-  sealed case class State(
-    val versions: Map[Version_ID, Version] = Map(),
-    val commands: Map[Command_ID, Command.State] = Map(),  // static markup from define_command
-    val execs: Map[Exec_ID, Command.State] = Map(),  // dynamic markup from execution
-    val assignments: Map[Version_ID, State.Assignment] = Map(),
+  sealed case class State private(
+    val versions: Map[Version_ID, Version] = Map.empty,
+    val commands: Map[Command_ID, Command.State] = Map.empty,  // static markup from define_command
+    val execs: Map[Exec_ID, Command.State] = Map.empty,  // dynamic markup from execution
+    val assignments: Map[Version_ID, State.Assignment] = Map.empty,
     val history: History = History.init)
   {
     private def fail[A]: A = throw new State.Fail(this)
@@ -313,7 +336,8 @@
         case None => None
         case Some(st) =>
           val command = st.command
-          version.nodes.get(command.node_name).map((_, command))
+          val node = version.nodes(command.node_name)
+          Some((node, command))
       }
 
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
@@ -336,7 +360,7 @@
           }
       }
 
-    def assign(id: Version_ID, arg: Assign): (List[Command], State) =
+    def assign(id: Version_ID, arg: Assign = (Nil, Nil)): (List[Command], State) =
     {
       val version = the_version(id)
       val (command_execs, last_execs) = arg
@@ -392,22 +416,18 @@
         edits: List[Edit_Text],
         version: Future[Version]): (Change, State) =
     {
-      val change = Change(Some(previous), edits, version)
+      val change = Change.make(previous, edits, version)
       (change, copy(history = history + change))
     }
 
     def prune_history(retain: Int = 0): (List[Version], State) =
     {
-      val undo_list = history.undo_list
-      val n = undo_list.iterator.zipWithIndex.find(p => is_stable(p._1)).get._2 + 1
-      val (retained, dropped) = undo_list.splitAt(n max retain)
-
-      retained.splitAt(retained.length - 1) match {
-        case (prefix, List(last)) =>
+      history.prune(is_stable, retain) match {
+        case Some((dropped, history1)) =>
           val dropped_versions = dropped.map(change => change.version.get_finished)
-          val state1 = copy(history = History(prefix ::: List(last.truncate)))
+          val state1 = copy(history = history1)
           (dropped_versions, state1)
-        case _ => fail
+        case None => fail
       }
     }
 
diff -r f559866a7aa2 -r 07f9732804ad src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun Feb 26 15:28:48 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sun Feb 26 20:08:12 2012 +0100
@@ -80,9 +80,10 @@
 
   /* node status */
 
-  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
+  sealed case class Node_Status(
+    unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
   {
-    def total: Int = unprocessed + running + finished + failed
+    def total: Int = unprocessed + running + finished + warned + failed
   }
 
   def node_status(
@@ -91,16 +92,21 @@
     var unprocessed = 0
     var running = 0
     var finished = 0
+    var warned = 0
     var failed = 0
     node.commands.foreach(command =>
       {
-        val status = command_status(state.command_state(version, command).status)
+        val st = state.command_state(version, command)
+        val status = command_status(st.status)
         if (status.is_running) running += 1
-        else if (status.is_finished) finished += 1
+        else if (status.is_finished) {
+          if (st.results.exists(p => is_warning(p._2))) warned += 1
+          else finished += 1
+        }
         else if (status.is_failed) failed += 1
         else unprocessed += 1
       })
-    Node_Status(unprocessed, running, finished, failed)
+    Node_Status(unprocessed, running, finished, warned, failed)
   }
 
 
diff -r f559866a7aa2 -r 07f9732804ad src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Feb 26 15:28:48 2012 +0100
+++ b/src/Pure/System/session.scala	Sun Feb 26 20:08:12 2012 +0100
@@ -262,12 +262,12 @@
       val text_edits: List[Document.Edit_Text] =
         List((name, Document.Node.Perspective(text_perspective)))
       val change =
-        global_state.change_yield(
-          _.continue_history(Future.value(previous), text_edits, Future.value(version)))
+        global_state >>>
+          (_.continue_history(Future.value(previous), text_edits, Future.value(version)))
 
       val assignment = global_state().the_assignment(previous).check_finished
-      global_state.change(_.define_version(version, assignment))
-      global_state.change_yield(_.assign(version.id, Document.no_assign))
+      global_state >> (_.define_version(version, assignment))
+      global_state >>> (_.assign(version.id))
 
       prover.get.update_perspective(previous.id, version.id, name, perspective)
     }
@@ -286,7 +286,7 @@
 
       val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
       val version = Future.promise[Document.Version]
-      val change = global_state.change_yield(_.continue_history(previous, text_edits, version))
+      val change = global_state >>> (_.continue_history(previous, text_edits, version))
 
       change_parser ! Text_Edits(syntax, name, previous, text_edits, version)
     }
@@ -298,7 +298,7 @@
     def handle_assign(id: Document.Version_ID, assign: Document.Assign)
     //{{{
     {
-      val cmds = global_state.change_yield(_.assign(id, assign))
+      val cmds = global_state >>> (_.assign(id, assign))
       for (cmd <- cmds) delay_commands_changed.invoke(cmd)
     }
     //}}}
@@ -309,7 +309,7 @@
     def handle_removed(removed: List[Document.Version_ID])
     //{{{
     {
-      global_state.change(_.removed_versions(removed))
+      global_state >> (_.removed_versions(removed))
     }
     //}}}
 
@@ -327,7 +327,7 @@
       def id_command(command: Command)
       {
         if (!global_state().defined_command(command.id)) {
-          global_state.change(_.define_command(command))
+          global_state >> (_.define_command(command))
           prover.get.define_command(command)
         }
       }
@@ -337,7 +337,7 @@
       }
 
       val assignment = global_state().the_assignment(previous).check_finished
-      global_state.change(_.define_version(version, assignment))
+      global_state >> (_.define_version(version, assignment))
       prover.get.update(previous.id, version.id, doc_edits)
     }
     //}}}
@@ -358,7 +358,7 @@
 
         case Position.Id(state_id) if !result.is_raw =>
           try {
-            val st = global_state.change_yield(_.accumulate(state_id, result.message))
+            val st = global_state >>> (_.accumulate(state_id, result.message))
             delay_commands_changed.invoke(st.command)
           }
           catch {
@@ -374,7 +374,7 @@
           }
           // FIXME separate timeout event/message!?
           if (prover.isDefined && System.currentTimeMillis() > prune_next) {
-            val old_versions = global_state.change_yield(_.prune_history(prune_size))
+            val old_versions = global_state >>> (_.prune_history(prune_size))
             if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
             prune_next = System.currentTimeMillis() + prune_delay.ms
           }
@@ -441,7 +441,7 @@
 
         case Stop =>
           if (phase == Session.Ready) {
-            global_state.change(_ => Document.State.init)  // FIXME event bus!?
+            global_state >> (_ => Document.State.init)  // FIXME event bus!?
             phase = Session.Shutdown
             prover.get.terminate
             prover = None
diff -r f559866a7aa2 -r 07f9732804ad src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Feb 26 15:28:48 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Feb 26 20:08:12 2012 +0100
@@ -23,7 +23,7 @@
   val USES = "uses"
   val BEGIN = "begin"
 
-  val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
+  private val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 
 
   /* theory file name */
@@ -38,7 +38,6 @@
     s match { case Thy_Name(name) => Some(name) case _ => None }
 
   def thy_path(path: Path): Path = path.ext("thy")
-  def thy_path(name: String): Path = Path.basic(name).ext("thy")
 
 
   /* header */
@@ -105,8 +104,8 @@
   {
     val header = read(source)
     val name1 = header.name
-    if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
-    Path.explode(name)
+    val path = Path.explode(name)
+    if (name != name1) error("Bad file name " + thy_path(path) + " for theory " + quote(name1))
     header
   }
 }
diff -r f559866a7aa2 -r 07f9732804ad src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 15:28:48 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 20:08:12 2012 +0100
@@ -135,7 +135,7 @@
     val perspective = command_perspective(node, text_perspective)
     val new_nodes =
       if (node.perspective same perspective) None
-      else Some(nodes + (name -> node.copy(perspective = perspective)))
+      else Some(nodes + (name -> node.update_perspective(perspective)))
     (perspective, new_nodes)
   }
 
@@ -145,7 +145,7 @@
   {
     val nodes = previous.nodes
     val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
-    val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
+    val version = Document.Version.make(new_nodes getOrElse nodes)
     (perspective, version)
   }
 
@@ -252,7 +252,7 @@
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
           doc_edits += (name -> Document.Node.Edits(cmd_edits))
-          nodes += (name -> node.copy(commands = commands2))
+          nodes += (name -> node.update_commands(commands2))
 
         case (name, Document.Node.Header(header)) =>
           val node = nodes(name)
@@ -263,7 +263,7 @@
             }
           if (update_header) {
             doc_edits += (name -> Document.Node.Header(header))
-            nodes += (name -> node.copy(header = header))
+            nodes += (name -> node.update_header(header))
           }
 
         case (name, Document.Node.Perspective(text_perspective)) =>
@@ -274,7 +274,7 @@
               nodes = nodes1
           }
       }
-      (doc_edits.toList, Document.Version(Document.new_id(), nodes))
+      (doc_edits.toList, Document.Version.make(nodes))
     }
   }
 }
diff -r f559866a7aa2 -r 07f9732804ad src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 15:28:48 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 20:08:12 2012 +0100
@@ -116,6 +116,7 @@
             (n, color) <- List(
               (st.unprocessed, Isabelle_Rendering.unprocessed1_color),
               (st.running, Isabelle_Rendering.running_color),
+              (st.warned, Isabelle_Rendering.warning_color),
               (st.failed, Isabelle_Rendering.error_color)) }
           {
             gfx.setColor(color)
@@ -146,14 +147,13 @@
   {
     Swing_Thread.now {
       val snapshot = Isabelle.session.snapshot()
-      val nodes = restriction getOrElse snapshot.version.nodes.keySet
+      val names = restriction getOrElse snapshot.version.nodes.keySet
 
-      var nodes_status1 = nodes_status
-      for {
-        name <- nodes
-        node <- snapshot.version.nodes.get(name)
-        val status = Protocol.node_status(snapshot.state, snapshot.version, node)
-      } nodes_status1 += (name -> status)
+      val nodes_status1 =
+        (nodes_status /: names)((status, name) => {
+          val node = snapshot.version.nodes(name)
+          status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node))
+        })
 
       if (nodes_status != nodes_status1) {
         nodes_status = nodes_status1