--- 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
--- 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
--- 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
--- 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
}
}
--- 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)
}
--- 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
--- 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
}
}
--- 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))
}
}
}
--- 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