author wenzelm Thu, 01 Sep 2011 14:35:51 +0200 changeset 44638 74fb317aaeb5 parent 44637 13f86edf3db3 (current diff) parent 44617 5db68864a967 (diff) child 44639 83dc04ccabd5 child 44646 a6047ddd9377
merged
```--- a/src/FOL/ex/Nat_Class.thy	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/FOL/ex/Nat_Class.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -26,9 +26,8 @@
and rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
begin

-definition
-  add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 60) where
-  "m + n = rec(m, n, \<lambda>x y. Suc(y))"
+definition add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 60)
+  where "m + n = rec(m, n, \<lambda>x y. Suc(y))"

lemma Suc_n_not_n: "Suc(k) \<noteq> (k::'a)"
apply (rule_tac n = k in induct)```
```--- a/src/FOL/ex/Natural_Numbers.thy	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/FOL/ex/Natural_Numbers.thy	Thu Sep 01 14:35:51 2011 +0200
@@ -46,9 +46,8 @@
qed

-definition
-  add :: "[nat, nat] => nat"    (infixl "+" 60) where
-  "m + n = rec(m, n, \<lambda>x y. Suc(y))"
+definition add :: "nat => nat => nat"    (infixl "+" 60)
+  where "m + n = rec(m, n, \<lambda>x y. Suc(y))"

lemma add_0 [simp]: "0 + n = n"
```--- a/src/Pure/PIDE/command.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -80,10 +80,11 @@
/* dummy commands */

def unparsed(source: String): Command =
-    new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source)))
+    new Command(Document.no_id, Document.Node.Name("", "", ""),
+      List(Token(Token.Kind.UNPARSED, source)))

-  def span(toks: List[Token]): Command =
-    new Command(Document.no_id, toks)
+  def span(node_name: Document.Node.Name, toks: List[Token]): Command =
+    new Command(Document.no_id, node_name, toks)

/* perspective */
@@ -110,6 +111,7 @@

class Command(
val id: Document.Command_ID,
+    val node_name: Document.Node.Name,
val span: List[Token])
{
/* classification */```
```--- a/src/Pure/PIDE/document.ML	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -25,7 +25,7 @@
type state
val init_state: state
val define_command: command_id -> string -> state -> state
-  val join_commands: state -> unit
+  val join_commands: state -> state
val cancel_execution: state -> Future.task list
val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
val update: version_id -> version_id -> edit list -> state ->
@@ -230,7 +230,9 @@

abstype state = State of
{versions: version Inttab.table,  (*version_id -> document content*)
-  commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
+  commands:
+    Toplevel.transition future Inttab.table *  (*command_id -> transition (future parsing)*)
+    Toplevel.transition future list,  (*recent commands to be joined*)
execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
(*exec_id -> command_id with eval/print process*)
execution: Future.group}  (*global execution process*)
@@ -244,7 +246,7 @@

val init_state =
make_state (Inttab.make [(no_id, empty_version)],
-    Inttab.make [(no_id, Future.value Toplevel.empty)],
+    (Inttab.make [(no_id, Future.value Toplevel.empty)], []),
Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
Future.new_group NONE);

@@ -266,7 +268,7 @@
(* commands *)

fun define_command (id: command_id) text =
-  map_state (fn (versions, commands, execs, execution) =>
+  map_state (fn (versions, (commands, recent), execs, execution) =>
let
val id_string = print_id id;
val tr =
@@ -276,15 +278,16 @@
val commands' =
Inttab.update_new (id, tr) commands
handle Inttab.DUP dup => err_dup "command" dup;
-    in (versions, commands', execs, execution) end);
+    in (versions, (commands', tr :: recent), execs, execution) end);

fun the_command (State {commands, ...}) (id: command_id) =
-  (case Inttab.lookup commands id of
+  (case Inttab.lookup (#1 commands) id of
NONE => err_undef "command" id
| SOME tr => tr);

-fun join_commands (State {commands, ...}) =
-  Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands ();
+val join_commands =
+    map_state (fn (versions, (commands, recent), execs, execution) =>
+      (Future.join_results recent; (versions, (commands, []), execs, execution)));

(* command executions *)
@@ -328,10 +331,7 @@
fun run int tr st =
(case Toplevel.transition int tr st of
SOME (st', NONE) => ([], SOME st')
-  | SOME (_, SOME (exn, _)) =>
-      (case ML_Compiler.exn_messages exn of
-        [] => Exn.interrupt ()
-      | errs => (errs, NONE))
+  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
| NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));

in
@@ -342,15 +342,21 @@
val is_proof = Keyword.is_proof (Toplevel.name_of tr);
val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);

+    val _ = Multithreading.interrupted ();
+    val _ = Toplevel.status tr Markup.forked;
val start = Timing.start ();
val (errs, result) =
if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
val _ = timing tr (Timing.result start);
+    val _ = Toplevel.status tr Markup.joined;
val _ = List.app (Toplevel.error_msg tr) errs;
in
(case result of
-      NONE => (Toplevel.status tr Markup.failed; (st, no_print))
+      NONE =>
+       (if null errs then Exn.interrupt () else ();
+        Toplevel.status tr Markup.failed;
+        (st, no_print))
| SOME st' =>
(Toplevel.status tr Markup.finished;
proof_status tr st';
@@ -526,7 +532,7 @@
(fn deps => fn (name, node) =>
(singleton o Future.forks)
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
-                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
+                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
(iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));

in (versions, commands, execs, execution) end);```
```--- a/src/Pure/PIDE/document.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -31,7 +31,7 @@

/* named nodes -- development graph */

-  type Edit[A, B] = (String, Node.Edit[A, B])
+  type Edit[A, B] = (Node.Name, Node.Edit[A, B])
type Edit_Text = Edit[Text.Edit, Text.Perspective]
type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]

@@ -39,6 +39,16 @@

object Node
{
+    sealed case class Name(node: String, dir: String, theory: String)
+    {
+      override def hashCode: Int = node.hashCode
+      override def equals(that: Any): Boolean =
+        that match {
+          case other: Name => node == other.node
+          case _ => false
+        }
+    }
+
sealed abstract class Edit[A, B]
{
def foreach(f: A => Unit)
@@ -149,7 +159,7 @@
val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
}

-  type Nodes = Map[String, Node]
+  type Nodes = Map[Node.Name, Node]
sealed case class Version(val id: Version_ID, val nodes: Nodes)

@@ -271,13 +281,12 @@

def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)

-    def find_command(version: Version, id: ID): Option[(String, Node, Command)] =
+    def find_command(version: Version, id: ID): Option[(Node, Command)] =
commands.get(id) orElse execs.get(id) match {
case None => None
case Some(st) =>
val command = st.command
-          version.nodes.find({ case (_, node) => node.commands(command) })
-            .map({ case (name, node) => (name, node, command) })
+          version.nodes.get(command.node_name).map((_, command))
}

def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
@@ -336,10 +345,10 @@
def tip_stable: Boolean = is_stable(history.tip)
def tip_version: Version = history.tip.version.get_finished

-    def last_exec_offset(name: String): Text.Offset =
+    def last_exec_offset(name: Node.Name): Text.Offset =
{
val version = tip_version
-      the_assignment(version).last_execs.get(name) match {
+      the_assignment(version).last_execs.get(name.node) match {
case Some(Some(id)) =>
val node = version.nodes(name)
val cmd = the_command(id).command
@@ -360,9 +369,19 @@
(change, copy(history = history + change))
}

+    def command_state(version: Version, command: Command): Command.State =
+    {
+      require(is_assigned(version))
+      try {
+        the_exec(the_assignment(version).check_finished.command_execs
+          .getOrElse(command.id, fail))
+      }
+      catch { case _: State.Fail => command.empty_state }
+    }
+

// persistent user-view
-    def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
+    def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot =
{
val stable = recent_stable.get
val latest = history.tip
@@ -379,13 +398,7 @@
val version = stable.version.get_finished
val node = version.nodes(name)
val is_outdated = !(pending_edits.isEmpty && latest == stable)
-
-        def command_state(command: Command): Command.State =
-          try {
-            the_exec(the_assignment(version).check_finished.command_execs
-              .getOrElse(command.id, fail))
-          }
-          catch { case _: State.Fail => command.empty_state }
+        def command_state(command: Command): Command.State = state.command_state(version, command)

def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))```
```--- a/src/Pure/PIDE/isar_document.ML	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -12,6 +12,10 @@
(fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));

val _ =
+    (fn [] => ignore (Document.cancel_execution (Document.state ())));
+
+val _ =
(fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
let
@@ -48,17 +52,17 @@
end;

val running = Document.cancel_execution state;
-        val (assignment, state') = Document.update old_id new_id edits state;
+        val (assignment, state1) = Document.update old_id new_id edits state;
-        val _ = Document.join_commands state';
+        val state2 = Document.join_commands state1;
val _ =
Output.status (Markup.markup (Markup.assign new_id)
(assignment |>
let open XML.Encode
in pair (list (pair int (option int))) (list (pair string (option int))) end
|> YXML.string_of_body));
-        val state'' = Document.execute new_id state';
-      in state'' end));
+        val state3 = Document.execute new_id state2;
+      in state3 end));

val _ =
```--- a/src/Pure/PIDE/isar_document.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -33,8 +33,8 @@
/* toplevel transactions */

sealed abstract class Status
+  case object Unprocessed extends Status
case class Forked(forks: Int) extends Status
-  case object Unprocessed extends Status
case object Finished extends Status
case object Failed extends Status

@@ -51,6 +51,25 @@
else Unprocessed
}

+  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
+
+  def node_status(
+    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
+  {
+    var unprocessed = 0
+    var running = 0
+    var finished = 0
+    var failed = 0
+    node.commands.foreach(command =>
+      command_status(state.command_state(version, command).status) match {
+        case Unprocessed => unprocessed += 1
+        case Forked(_) => running += 1
+        case Finished => finished += 1
+        case Failed => failed += 1
+      })
+    Node_Status(unprocessed, running, finished, failed)
+  }
+

/* result messages */

@@ -135,15 +154,20 @@

/* document versions */

+  def cancel_execution()
+  {
+    input("Isar_Document.cancel_execution")
+  }
+
def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
-    name: String, perspective: Command.Perspective)
+    name: Document.Node.Name, perspective: Command.Perspective)
{
val ids =
{ import XML.Encode._
list(long)(perspective.commands.map(_.id)) }

-    input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
-      YXML.string_of_body(ids))
+    input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
+      name.node, YXML.string_of_body(ids))
}

def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
@@ -153,7 +177,7 @@
{ import XML.Encode._
def id: T[Command] = (cmd => long(cmd.id))
def encode: T[List[Document.Edit_Command]] =
-        list(pair(string,
+        list(pair((name => string(name.node)),
variant(List(
{ case Document.Node.Clear() => (Nil, Nil) },
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },```
```--- a/src/Pure/System/session.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/System/session.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -22,7 +22,7 @@
case object Global_Settings
case object Perspective
case object Assignment
-  case class Commands_Changed(set: Set[Command])
+  case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])

sealed abstract class Phase
case object Inactive extends Phase
@@ -63,7 +63,10 @@
private val (_, command_change_buffer) =
{
-    var changed: Set[Command] = Set()
+    var changed_nodes: Set[Document.Node.Name] = Set.empty
+    var changed_commands: Set[Command] = Set.empty
+    def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
+
var flush_time: Option[Long] = None

def flush_timeout: Long =
@@ -74,8 +77,10 @@

def flush()
{
-      if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
-      changed = Set()
+      if (changed)
+        commands_changed.event(Session.Commands_Changed(changed_nodes, changed_commands))
+      changed_nodes = Set.empty
+      changed_commands = Set.empty
flush_time = None
}

@@ -91,7 +96,10 @@
var finished = false
while (!finished) {
-        case command: Command => changed += command; invoke()
+        case command: Command =>
+          changed_nodes += command.node_name
+          changed_commands += command
+          invoke()
case TIMEOUT => flush()
case Stop => finished = true; reply(())
@@ -126,23 +134,21 @@
private val global_state = new Volatile(Document.State.init)
def current_state(): Document.State = global_state()

-  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
+  def snapshot(name: Document.Node.Name, pending_edits: List[Text.Edit]): Document.Snapshot =
global_state().snapshot(name, pending_edits)

/* theory files */

-  def header_edit(name: String, master_dir: String,
{
def norm_import(s: String): String =
{
}
-    def norm_use(s: String): String =
+    def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))

@@ -159,12 +165,12 @@

private case class Start(timeout: Time, args: List[String])
private case object Interrupt
-  private case class Init_Node(name: String, master_dir: String,
+  private case class Init_Node(name: Document.Node.Name,
-  private case class Edit_Node(name: String, master_dir: String,
+  private case class Edit_Node(name: Document.Node.Name,
private case class Change_Node(
-    name: String,
+    name: Document.Node.Name,
doc_edits: List[Document.Edit_Command],
previous: Document.Version,
version: Document.Version)
@@ -177,7 +183,7 @@

/* perspective */

-    def update_perspective(name: String, text_perspective: Text.Perspective)
+    def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
{
val previous = global_state().tip_version
val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
@@ -198,14 +204,16 @@

/* incoming edits */

-    def handle_edits(name: String, master_dir: String,
+    def handle_edits(name: Document.Node.Name,
//{{{
{
val syntax = current_syntax()
val previous = global_state().history.tip.version

-      val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
+      prover.get.cancel_execution()
+
val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
val change =
global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
@@ -344,20 +352,20 @@
case Interrupt if prover.isDefined =>
prover.get.interrupt

-        case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
+        case Init_Node(name, header, perspective, text) if prover.isDefined =>
// FIXME compare with existing node
List(Document.Node.Clear(),
Document.Node.Edits(List(Text.Edit.insert(0, text))),
Document.Node.Perspective(perspective)))

-        case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
+        case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
if (text_edits.isEmpty && global_state().tip_stable &&
perspective.range.stop <= global_state().last_exec_offset(name))
update_perspective(name, perspective)
else
List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))

@@ -386,13 +394,11 @@

def interrupt() { session_actor ! Interrupt }

-  // FIXME simplify signature
-  def init_node(name: String, master_dir: String,
+  def init_node(name: Document.Node.Name,
-  { session_actor !? Init_Node(name, master_dir, header, perspective, text) }
+  { session_actor !? Init_Node(name, header, perspective, text) }

-  // FIXME simplify signature
-    perspective: Text.Perspective, edits: List[Text.Edit])
-  { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) }
+  def edit_node(name: Document.Node.Name,
+  { session_actor !? Edit_Node(name, header, perspective, edits) }
}```
```--- a/src/Pure/Thy/thy_info.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -25,51 +25,55 @@
{
/* messages */

-  private def show_path(names: List[String]): String =
-    names.map(quote).mkString(" via ")
+  private def show_path(names: List[Document.Node.Name]): String =
+    names.map(name => quote(name.theory)).mkString(" via ")

-  private def cycle_msg(names: List[String]): String =
+  private def cycle_msg(names: List[Document.Node.Name]): String =
"Cyclic dependency of " + show_path(names)

-  private def required_by(s: String, initiators: List[String]): String =
+  private def required_by(initiators: List[Document.Node.Name]): String =
if (initiators.isEmpty) ""
-    else s + "(required by " + show_path(initiators.reverse) + ")"
+    else "\n(required by " + show_path(initiators.reverse) + ")"

/* dependencies */

-  type Deps = Map[String, Document.Node_Header]
-
-  private def require_thys(initiators: List[String],
-      deps: Deps, thys: List[(String, String)]): Deps =
-    (deps /: thys)(require_thy(initiators, _, _))
-
-  private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps =
+  def import_name(dir: String, str: String): Document.Node.Name =
{
-    val (dir, str) = thy
val path = Path.explode(str)
-    val thy_name = path.base.implode
+    val dir1 = thy_load.append(dir, path.dir)
+    val theory = path.base.implode
+    Document.Node.Name(node, dir1, theory)
+  }
+
+  type Deps = Map[Document.Node.Name, Document.Node_Header]

+  private def require_thys(initiators: List[Document.Node.Name],
+      deps: Deps, names: List[Document.Node.Name]): Deps =
+    (deps /: names)(require_thy(initiators, _, _))
+
+  private def require_thy(initiators: List[Document.Node.Name],
+      deps: Deps, name: Document.Node.Name): Deps =
+  {
else {
-      val dir1 = thy_load.append(dir, path.dir)
try {
-        if (initiators.contains(node_name)) error(cycle_msg(initiators))
+        if (initiators.contains(name)) error(cycle_msg(initiators))
catch {
case ERROR(msg) =>
-              cat_error(msg, "The error(s) above occurred while examining theory file " +
-                quote(node_name) + required_by("\n", initiators))
+              cat_error(msg, "The error(s) above occurred while examining theory " +
+                quote(name.theory) + required_by(initiators))
}
-        val thys = header.imports.map(str => (dir1, str))
-        require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys)
+        val imports = header.imports.map(import_name(name.dir, _))
+        require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports)
}
-      catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) }
+      catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
}
}

-  def dependencies(thys: List[(String, String)]): Deps =
-    require_thys(Nil, Map.empty, thys)
+  def dependencies(names: List[Document.Node.Name]): Deps =
+    require_thys(Nil, Map.empty, names)
}```
```--- a/src/Pure/Thy/thy_load.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/Thy/thy_load.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -10,7 +10,7 @@
{
def register_thy(thy_name: String)
-  def append(master_dir: String, path: Path): String
+  def append(dir: String, path: Path): String
}
```
```--- a/src/Pure/Thy/thy_syntax.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -27,12 +27,14 @@
def length: Int = command.length
}

-    def parse(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
+    def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence)
+      : Entry =
{
/* stack operations */

def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
-      var stack: List[(Int, String, mutable.ListBuffer[Entry])] = List((0, root_name, buffer()))
+      var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
+        List((0, "theory " + node_name.theory, buffer()))

@tailrec def close(level: Int => Boolean)
{
@@ -67,7 +69,7 @@
/* result structure */

val spans = parse_spans(syntax.scan(text))
result()
}
}
@@ -125,7 +127,8 @@
}
}

-  def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective)
+  def update_perspective(nodes: Document.Nodes,
+      name: Document.Node.Name, text_perspective: Text.Perspective)
: (Command.Perspective, Option[Document.Nodes]) =
{
val node = nodes(name)
@@ -136,7 +139,8 @@
(perspective, new_nodes)
}

-  def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective)
+  def edit_perspective(previous: Document.Version,
+      name: Document.Node.Name, text_perspective: Text.Perspective)
: (Command.Perspective, Document.Version) =
{
val nodes = previous.nodes
@@ -186,7 +190,8 @@

/* phase 2: recover command spans */

-    @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
+    @tailrec def recover_spans(node_name: Document.Node.Name, commands: Linear_Set[Command])
+      : Linear_Set[Command] =
{
commands.iterator.find(cmd => !cmd.is_defined) match {
case Some(first_unparsed) =>
@@ -212,10 +217,10 @@
(Some(last), spans1.take(spans1.length - 1))
else (commands.next(last), spans1)

-          val inserted = spans2.map(span => new Command(Document.new_id(), span))
+          val inserted = spans2.map(span => new Command(Document.new_id(), node_name, span))
val new_commands =
commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
-          recover_spans(new_commands)
+          recover_spans(node_name, new_commands)

case None => commands
}
@@ -237,7 +242,7 @@
val node = nodes(name)
val commands0 = node.commands
val commands1 = edit_text(text_edits, commands0)
-          val commands2 = recover_spans(commands1)   // FIXME somewhat slow
+          val commands2 = recover_spans(name, commands1)   // FIXME somewhat slow

val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList```
```--- a/src/Pure/library.ML	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/library.ML	Thu Sep 01 14:35:51 2011 +0200
@@ -959,7 +959,7 @@
fun sort_distinct ord = quicksort true ord;

val sort_strings = sort string_ord;
-fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
+fun sort_wrt key xs = sort (string_ord o pairself key) xs;

(* items tagged by integer index *)```
```--- a/src/Pure/library.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Pure/library.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -14,6 +14,8 @@
import scala.swing.ComboBox
import scala.swing.event.SelectionChanged
import scala.collection.mutable
+import scala.math.Ordering
+import scala.util.Sorting

object Library
@@ -61,6 +63,18 @@

def split_lines(str: String): List[String] = space_explode('\n', str)

+  def sort_wrt[A](key: A => String, args: Seq[A]): List[A] =
+  {
+    val ordering: Ordering[A] =
+      new Ordering[A] { def compare(x: A, y: A): Int = key(x) compare key(y) }
+    val a = (new Array[Any](args.length)).asInstanceOf[Array[A]]
+    for ((x, i) <- args.iterator zipWithIndex) a(i) = x
+    Sorting.quickSort[A](a)(ordering)
+    a.toList
+  }
+
+  def sort_strings(args: Seq[String]): List[String] = sort_wrt((x: String) => x, args)
+

/* iterate over chunks (cf. space_explode) */
```
```--- a/src/Tools/jEdit/src/document_model.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -45,11 +45,10 @@
}
}

-  def init(session: Session, buffer: Buffer,
-    master_dir: String, node_name: String, thy_name: String): Document_Model =
+  def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
{
exit(buffer)
-    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
+    val model = new Document_Model(session, buffer, name)
buffer.setProperty(key, model)
model.activate()
model
@@ -57,15 +56,14 @@
}

-class Document_Model(val session: Session, val buffer: Buffer,
-  val master_dir: String, val node_name: String, val thy_name: String)
+class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
{

{
-    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
+    Exn.capture { Thy_Header.check(name.theory, buffer.getSegment(0, buffer.getLength)) }
}

@@ -105,15 +103,14 @@
case edits =>
pending.clear
last_perspective = new_perspective
-          session.edit_node(node_name, master_dir, node_header(), new_perspective, edits)
}
}

def init()
{
flush()
-      session.init_node(node_name, master_dir,
}

private val delay_flush =
@@ -145,7 +142,7 @@
def snapshot(): Document.Snapshot =
{
-    session.snapshot(node_name, pending_edits.snapshot())
+    session.snapshot(name, pending_edits.snapshot())
}

```
```--- a/src/Tools/jEdit/src/document_view.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -442,27 +442,29 @@
private val main_actor = actor {
loop {
react {
-        case Session.Commands_Changed(changed) =>
+        case changed: Session.Commands_Changed =>
val buffer = model.buffer
Isabelle.swing_buffer_lock(buffer) {
val (updated, snapshot) = flush_snapshot()
val visible = visible_range()

-            if (updated || changed.exists(snapshot.node.commands.contains))
+            if (updated ||
+                (changed.nodes.contains(model.name) &&
+                 changed.commands.exists(snapshot.node.commands.contains)))
overview.repaint()

if (updated) invalidate_range(visible)
else {
val visible_cmds =
snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
-              if (visible_cmds.exists(changed)) {
+              if (visible_cmds.exists(changed.commands)) {
for {
line <- 0 until text_area.getVisibleLines
val start = text_area.getScreenLineStartOffset(line) if start >= 0
val end = text_area.getScreenLineEndOffset(line) if end >= 0
val range = proper_line_range(start, end)
val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
-                  if line_cmds.exists(changed)
+                  if line_cmds.exists(changed.commands)
} text_area.invalidateScreenLineRange(line, line)
}
}```
```--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -74,10 +74,10 @@
(props, props) match {
case (Position.Id(def_id), Position.Offset(def_offset)) =>
snapshot.state.find_command(snapshot.version, def_id) match {
-                          case Some((def_name, def_node, def_cmd)) =>
+                          case Some((def_node, def_cmd)) =>
def_node.command_start(def_cmd) match {
case Some(def_cmd_start) =>
-                                new Internal_Hyperlink(def_name, begin, end, line,
+                                new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
def_cmd_start + def_cmd.decode(def_offset))
case None => null
}```
```--- a/src/Tools/jEdit/src/isabelle_markup.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -24,7 +24,11 @@
def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)

val outdated_color = new Color(238, 227, 227)
-  val unfinished_color = new Color(255, 228, 225)
+  val outdated1_color = new Color(238, 227, 227, 50)
+  val running_color = new Color(97, 0, 97)
+  val running1_color = new Color(97, 0, 97, 100)
+  val unfinished_color = new Color(255, 160, 160)
+  val unfinished1_color = new Color(255, 160, 160, 50)

val light_color = new Color(240, 240, 240)
val regular_color = new Color(192, 192, 192)
@@ -53,11 +57,11 @@
def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
{
val state = snapshot.command_state(command)
-    if (snapshot.is_outdated) Some(outdated_color)
+    if (snapshot.is_outdated) Some(outdated1_color)
else
Isar_Document.command_status(state.status) match {
-        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
-        case Isar_Document.Unprocessed => Some(unfinished_color)
+        case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
+        case Isar_Document.Unprocessed => Some(unfinished1_color)
case _ => None
}
}
@@ -68,7 +72,7 @@
if (snapshot.is_outdated) None
else
Isar_Document.command_status(state.status) match {
-        case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
+        case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
case Isar_Document.Unprocessed => Some(unfinished_color)
case Isar_Document.Failed => Some(error_color)
case Isar_Document.Finished =>```
```--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -138,7 +138,7 @@
}

val text = Isabelle.buffer_text(model.buffer)
-    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
+    val structure = Structure.parse(syntax, model.name, text)

make_tree(0, structure) foreach (node => data.root.add(node))
}```
```--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -33,23 +33,23 @@

/* file-system operations */

-  override def append(master_dir: String, source_path: Path): String =
+  override def append(dir: String, source_path: Path): String =
{
val path = source_path.expand
if (path.is_absolute) Isabelle_System.platform_path(path)
else {
-      val vfs = VFSManager.getVFSForPath(master_dir)
+      val vfs = VFSManager.getVFSForPath(dir)
if (vfs.isInstanceOf[FileVFS])
-          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
-      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
+          vfs.constructPath(dir, Isabelle_System.platform_path(path)))
+      else vfs.constructPath(dir, Isabelle_System.standard_path(path))
}
}

-  override def check_thy(node_name: String): Thy_Header =
+  override def check_thy(name: Document.Node.Name): Thy_Header =
{
-      Isabelle.jedit_buffer(node_name) match {
+      Isabelle.jedit_buffer(name.node) match {
case Some(buffer) =>
Isabelle.buffer_lock(buffer) {
val text = new Segment
@@ -59,7 +59,7 @@
case None => None
}
} getOrElse {
-      val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
+      val file = new File(name.node)  // FIXME load URL via jEdit VFS (!?)
if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
}```
```--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -105,7 +105,7 @@
loop {
react {
case Session.Global_Settings => handle_resize()
-        case Session.Commands_Changed(changed) => handle_update(Some(changed))
+        case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
}```
```--- a/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -14,8 +14,7 @@
import javax.swing.JOptionPane

import scala.collection.mutable
-import scala.swing.ComboBox
-import scala.util.Sorting
+import scala.swing.{ComboBox, ListView, ScrollPane}

import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
Buffer, EditPane, ServiceManager, View}
@@ -169,9 +168,6 @@

def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath

-  def buffer_path(buffer: Buffer): (String, String) =
-    (buffer.getDirectory, buffer_name(buffer))
-

/* main jEdit components */

@@ -217,10 +213,11 @@
document_model(buffer) match {
case Some(model) => Some(model)
case None =>
-            val (master_dir, path) = buffer_path(buffer)
-              case Some(name) =>
-                Some(Document_Model.init(session, buffer, master_dir, path, name))
+            val name = buffer_name(buffer)
+              case Some(theory) =>
+                val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
+                Some(Document_Model.init(session, buffer, node_name))
case None => None
}
}
@@ -364,23 +361,25 @@

val thys =
for (buffer <- buffers; model <- Isabelle.document_model(buffer))
-          yield (model.master_dir, model.thy_name)
-      val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
+          yield model.name
+      val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _)

-      val do_load = !files.isEmpty &&
-        {
-          val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
-          val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
-          files_text.editable = false
+      if (!files.isEmpty) {
+        val files_list = new ListView(Library.sort_strings(files))
+        for (i <- 0 until files.length)
+          files_list.selection.indices += i
+
Library.confirm_dialog(jEdit.getActiveView(),
JOptionPane.YES_NO_OPTION,
-            "The following files are required to resolve theory imports.  Reload now?",
-            files_text) == 0
-        }
-        for (file <- files if !loaded_buffer(file))
-          jEdit.openFile(null: View, file)
+            "The following files are required to resolve theory imports.",
+            new ScrollPane(files_list))
+          files_list.selection.items foreach (file =>
+            if (!loaded_buffer(file)) jEdit.openFile(null: View, file))
+      }
}

```
```--- a/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 14:21:09 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 14:35:51 2011 +0200
@@ -10,11 +10,13 @@
import isabelle._

import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView,
+  ScrollPane, TabbedPane, Component, Swing}
import scala.swing.event.{ButtonClicked, SelectionChanged}

import java.lang.System
import java.awt.BorderLayout
+import javax.swing.JList
import javax.swing.border.{BevelBorder, SoftBevelBorder}

import org.gjt.sp.jedit.View
@@ -27,11 +29,16 @@
private val readme = new HTML_Panel("SansSerif", 14)

+  val status = new ListView(Nil: List[String])
+  status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
+  status.selection.intervalMode = ListView.IntervalMode.Single
+
private val syslog = new TextArea(Isabelle.session.syslog())

private val tabs = new TabbedPane {
-    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
+    pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
+    pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))

selection.index =
{
@@ -64,6 +71,36 @@

+  /* component state -- owned by Swing thread */
+
+  private var nodes_status: Map[Document.Node.Name, String] = Map.empty
+
+  private def handle_changed(changed_nodes: Set[Document.Node.Name])
+  {
+      // FIXME correlation to changed_nodes!?
+      val state = Isabelle.session.current_state()
+      state.recent_stable.map(change => change.version.get_finished) match {
+        case None =>
+        case Some(version) =>
+          var nodes_status1 = nodes_status
+          for {
+            name <- changed_nodes
+            node <- version.nodes.get(name)
+            val status = Isar_Document.node_status(state, version, node)
+          } nodes_status1 += (name -> status.toString)
+
+          if (nodes_status != nodes_status1) {
+            nodes_status = nodes_status1
+            val order =
+              Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
+            status.listData = order.map(name => name.theory + " " + nodes_status(name))
+          }
+      }
+    }
+  }
+
+
/* main actor */

private val main_actor = actor {
@@ -83,6 +120,8 @@
case phase: Session.Phase =>
Swing_Thread.now { session_phase.text = " " + phase.toString + " " }

+        case changed: Session.Commands_Changed => handle_changed(changed.nodes)
+
}
}
@@ -91,10 +130,12 @@
override def init() {
Isabelle.session.raw_messages += main_actor
Isabelle.session.phase_changed += main_actor
+    Isabelle.session.commands_changed += main_actor
}

override def exit() {
Isabelle.session.raw_messages -= main_actor
Isabelle.session.phase_changed -= main_actor
+    Isabelle.session.commands_changed -= main_actor
}
}```