merged
authorwenzelm
Thu Sep 01 14:35:51 2011 +0200 (2011-09-01 ago)
changeset 4463874fb317aaeb5
parent 44637 13f86edf3db3
parent 44617 5db68864a967
child 44639 83dc04ccabd5
child 44646 a6047ddd9377
merged
     1.1 --- a/src/FOL/ex/Nat_Class.thy	Thu Sep 01 14:21:09 2011 +0200
     1.2 +++ b/src/FOL/ex/Nat_Class.thy	Thu Sep 01 14:35:51 2011 +0200
     1.3 @@ -26,9 +26,8 @@
     1.4      and rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 60) where
     1.9 -  "m + n = rec(m, n, \<lambda>x y. Suc(y))"
    1.10 +definition add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 60)
    1.11 +  where "m + n = rec(m, n, \<lambda>x y. Suc(y))"
    1.12  
    1.13  lemma Suc_n_not_n: "Suc(k) \<noteq> (k::'a)"
    1.14    apply (rule_tac n = k in induct)
     2.1 --- a/src/FOL/ex/Natural_Numbers.thy	Thu Sep 01 14:21:09 2011 +0200
     2.2 +++ b/src/FOL/ex/Natural_Numbers.thy	Thu Sep 01 14:35:51 2011 +0200
     2.3 @@ -46,9 +46,8 @@
     2.4  qed
     2.5  
     2.6  
     2.7 -definition
     2.8 -  add :: "[nat, nat] => nat"    (infixl "+" 60) where
     2.9 -  "m + n = rec(m, n, \<lambda>x y. Suc(y))"
    2.10 +definition add :: "nat => nat => nat"    (infixl "+" 60)
    2.11 +  where "m + n = rec(m, n, \<lambda>x y. Suc(y))"
    2.12  
    2.13  lemma add_0 [simp]: "0 + n = n"
    2.14    unfolding add_def by (rule rec_0)
     3.1 --- a/src/Pure/PIDE/command.scala	Thu Sep 01 14:21:09 2011 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Thu Sep 01 14:35:51 2011 +0200
     3.3 @@ -80,10 +80,11 @@
     3.4    /* dummy commands */
     3.5  
     3.6    def unparsed(source: String): Command =
     3.7 -    new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source)))
     3.8 +    new Command(Document.no_id, Document.Node.Name("", "", ""),
     3.9 +      List(Token(Token.Kind.UNPARSED, source)))
    3.10  
    3.11 -  def span(toks: List[Token]): Command =
    3.12 -    new Command(Document.no_id, toks)
    3.13 +  def span(node_name: Document.Node.Name, toks: List[Token]): Command =
    3.14 +    new Command(Document.no_id, node_name, toks)
    3.15  
    3.16  
    3.17    /* perspective */
    3.18 @@ -110,6 +111,7 @@
    3.19  
    3.20  class Command(
    3.21      val id: Document.Command_ID,
    3.22 +    val node_name: Document.Node.Name,
    3.23      val span: List[Token])
    3.24  {
    3.25    /* classification */
     4.1 --- a/src/Pure/PIDE/document.ML	Thu Sep 01 14:21:09 2011 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Thu Sep 01 14:35:51 2011 +0200
     4.3 @@ -25,7 +25,7 @@
     4.4    type state
     4.5    val init_state: state
     4.6    val define_command: command_id -> string -> state -> state
     4.7 -  val join_commands: state -> unit
     4.8 +  val join_commands: state -> state
     4.9    val cancel_execution: state -> Future.task list
    4.10    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
    4.11    val update: version_id -> version_id -> edit list -> state ->
    4.12 @@ -230,7 +230,9 @@
    4.13  
    4.14  abstype state = State of
    4.15   {versions: version Inttab.table,  (*version_id -> document content*)
    4.16 -  commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
    4.17 +  commands:
    4.18 +    Toplevel.transition future Inttab.table *  (*command_id -> transition (future parsing)*)
    4.19 +    Toplevel.transition future list,  (*recent commands to be joined*)
    4.20    execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
    4.21      (*exec_id -> command_id with eval/print process*)
    4.22    execution: Future.group}  (*global execution process*)
    4.23 @@ -244,7 +246,7 @@
    4.24  
    4.25  val init_state =
    4.26    make_state (Inttab.make [(no_id, empty_version)],
    4.27 -    Inttab.make [(no_id, Future.value Toplevel.empty)],
    4.28 +    (Inttab.make [(no_id, Future.value Toplevel.empty)], []),
    4.29      Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
    4.30      Future.new_group NONE);
    4.31  
    4.32 @@ -266,7 +268,7 @@
    4.33  (* commands *)
    4.34  
    4.35  fun define_command (id: command_id) text =
    4.36 -  map_state (fn (versions, commands, execs, execution) =>
    4.37 +  map_state (fn (versions, (commands, recent), execs, execution) =>
    4.38      let
    4.39        val id_string = print_id id;
    4.40        val tr =
    4.41 @@ -276,15 +278,16 @@
    4.42        val commands' =
    4.43          Inttab.update_new (id, tr) commands
    4.44            handle Inttab.DUP dup => err_dup "command" dup;
    4.45 -    in (versions, commands', execs, execution) end);
    4.46 +    in (versions, (commands', tr :: recent), execs, execution) end);
    4.47  
    4.48  fun the_command (State {commands, ...}) (id: command_id) =
    4.49 -  (case Inttab.lookup commands id of
    4.50 +  (case Inttab.lookup (#1 commands) id of
    4.51      NONE => err_undef "command" id
    4.52    | SOME tr => tr);
    4.53  
    4.54 -fun join_commands (State {commands, ...}) =
    4.55 -  Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands ();
    4.56 +val join_commands =
    4.57 +    map_state (fn (versions, (commands, recent), execs, execution) =>
    4.58 +      (Future.join_results recent; (versions, (commands, []), execs, execution)));
    4.59  
    4.60  
    4.61  (* command executions *)
    4.62 @@ -328,10 +331,7 @@
    4.63  fun run int tr st =
    4.64    (case Toplevel.transition int tr st of
    4.65      SOME (st', NONE) => ([], SOME st')
    4.66 -  | SOME (_, SOME (exn, _)) =>
    4.67 -      (case ML_Compiler.exn_messages exn of
    4.68 -        [] => Exn.interrupt ()
    4.69 -      | errs => (errs, NONE))
    4.70 +  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
    4.71    | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
    4.72  
    4.73  in
    4.74 @@ -342,15 +342,21 @@
    4.75      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    4.76      val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
    4.77  
    4.78 +    val _ = Multithreading.interrupted ();
    4.79 +    val _ = Toplevel.status tr Markup.forked;
    4.80      val start = Timing.start ();
    4.81      val (errs, result) =
    4.82        if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
    4.83        else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    4.84      val _ = timing tr (Timing.result start);
    4.85 +    val _ = Toplevel.status tr Markup.joined;
    4.86      val _ = List.app (Toplevel.error_msg tr) errs;
    4.87    in
    4.88      (case result of
    4.89 -      NONE => (Toplevel.status tr Markup.failed; (st, no_print))
    4.90 +      NONE =>
    4.91 +       (if null errs then Exn.interrupt () else ();
    4.92 +        Toplevel.status tr Markup.failed;
    4.93 +        (st, no_print))
    4.94      | SOME st' =>
    4.95         (Toplevel.status tr Markup.finished;
    4.96          proof_status tr st';
    4.97 @@ -526,7 +532,7 @@
    4.98            (fn deps => fn (name, node) =>
    4.99              (singleton o Future.forks)
   4.100                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
   4.101 -                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
   4.102 +                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
   4.103                (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
   4.104  
   4.105      in (versions, commands, execs, execution) end);
     5.1 --- a/src/Pure/PIDE/document.scala	Thu Sep 01 14:21:09 2011 +0200
     5.2 +++ b/src/Pure/PIDE/document.scala	Thu Sep 01 14:35:51 2011 +0200
     5.3 @@ -31,7 +31,7 @@
     5.4  
     5.5    /* named nodes -- development graph */
     5.6  
     5.7 -  type Edit[A, B] = (String, Node.Edit[A, B])
     5.8 +  type Edit[A, B] = (Node.Name, Node.Edit[A, B])
     5.9    type Edit_Text = Edit[Text.Edit, Text.Perspective]
    5.10    type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
    5.11  
    5.12 @@ -39,6 +39,16 @@
    5.13  
    5.14    object Node
    5.15    {
    5.16 +    sealed case class Name(node: String, dir: String, theory: String)
    5.17 +    {
    5.18 +      override def hashCode: Int = node.hashCode
    5.19 +      override def equals(that: Any): Boolean =
    5.20 +        that match {
    5.21 +          case other: Name => node == other.node
    5.22 +          case _ => false
    5.23 +        }
    5.24 +    }
    5.25 +
    5.26      sealed abstract class Edit[A, B]
    5.27      {
    5.28        def foreach(f: A => Unit)
    5.29 @@ -149,7 +159,7 @@
    5.30      val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
    5.31    }
    5.32  
    5.33 -  type Nodes = Map[String, Node]
    5.34 +  type Nodes = Map[Node.Name, Node]
    5.35    sealed case class Version(val id: Version_ID, val nodes: Nodes)
    5.36  
    5.37  
    5.38 @@ -271,13 +281,12 @@
    5.39  
    5.40      def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
    5.41  
    5.42 -    def find_command(version: Version, id: ID): Option[(String, Node, Command)] =
    5.43 +    def find_command(version: Version, id: ID): Option[(Node, Command)] =
    5.44        commands.get(id) orElse execs.get(id) match {
    5.45          case None => None
    5.46          case Some(st) =>
    5.47            val command = st.command
    5.48 -          version.nodes.find({ case (_, node) => node.commands(command) })
    5.49 -            .map({ case (name, node) => (name, node, command) })
    5.50 +          version.nodes.get(command.node_name).map((_, command))
    5.51        }
    5.52  
    5.53      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
    5.54 @@ -336,10 +345,10 @@
    5.55      def tip_stable: Boolean = is_stable(history.tip)
    5.56      def tip_version: Version = history.tip.version.get_finished
    5.57  
    5.58 -    def last_exec_offset(name: String): Text.Offset =
    5.59 +    def last_exec_offset(name: Node.Name): Text.Offset =
    5.60      {
    5.61        val version = tip_version
    5.62 -      the_assignment(version).last_execs.get(name) match {
    5.63 +      the_assignment(version).last_execs.get(name.node) match {
    5.64          case Some(Some(id)) =>
    5.65            val node = version.nodes(name)
    5.66            val cmd = the_command(id).command
    5.67 @@ -360,9 +369,19 @@
    5.68        (change, copy(history = history + change))
    5.69      }
    5.70  
    5.71 +    def command_state(version: Version, command: Command): Command.State =
    5.72 +    {
    5.73 +      require(is_assigned(version))
    5.74 +      try {
    5.75 +        the_exec(the_assignment(version).check_finished.command_execs
    5.76 +          .getOrElse(command.id, fail))
    5.77 +      }
    5.78 +      catch { case _: State.Fail => command.empty_state }
    5.79 +    }
    5.80 +
    5.81  
    5.82      // persistent user-view
    5.83 -    def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
    5.84 +    def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot =
    5.85      {
    5.86        val stable = recent_stable.get
    5.87        val latest = history.tip
    5.88 @@ -379,13 +398,7 @@
    5.89          val version = stable.version.get_finished
    5.90          val node = version.nodes(name)
    5.91          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    5.92 -
    5.93 -        def command_state(command: Command): Command.State =
    5.94 -          try {
    5.95 -            the_exec(the_assignment(version).check_finished.command_execs
    5.96 -              .getOrElse(command.id, fail))
    5.97 -          }
    5.98 -          catch { case _: State.Fail => command.empty_state }
    5.99 +        def command_state(command: Command): Command.State = state.command_state(version, command)
   5.100  
   5.101          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
   5.102          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
     6.1 --- a/src/Pure/PIDE/isar_document.ML	Thu Sep 01 14:21:09 2011 +0200
     6.2 +++ b/src/Pure/PIDE/isar_document.ML	Thu Sep 01 14:35:51 2011 +0200
     6.3 @@ -12,6 +12,10 @@
     6.4      (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
     6.5  
     6.6  val _ =
     6.7 +  Isabelle_Process.add_command "Isar_Document.cancel_execution"
     6.8 +    (fn [] => ignore (Document.cancel_execution (Document.state ())));
     6.9 +
    6.10 +val _ =
    6.11    Isabelle_Process.add_command "Isar_Document.update_perspective"
    6.12      (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
    6.13        let
    6.14 @@ -48,17 +52,17 @@
    6.15              end;
    6.16  
    6.17          val running = Document.cancel_execution state;
    6.18 -        val (assignment, state') = Document.update old_id new_id edits state;
    6.19 +        val (assignment, state1) = Document.update old_id new_id edits state;
    6.20          val _ = Future.join_tasks running;
    6.21 -        val _ = Document.join_commands state';
    6.22 +        val state2 = Document.join_commands state1;
    6.23          val _ =
    6.24            Output.status (Markup.markup (Markup.assign new_id)
    6.25              (assignment |>
    6.26                let open XML.Encode
    6.27                in pair (list (pair int (option int))) (list (pair string (option int))) end
    6.28                |> YXML.string_of_body));
    6.29 -        val state'' = Document.execute new_id state';
    6.30 -      in state'' end));
    6.31 +        val state3 = Document.execute new_id state2;
    6.32 +      in state3 end));
    6.33  
    6.34  val _ =
    6.35    Isabelle_Process.add_command "Isar_Document.invoke_scala"
     7.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Sep 01 14:21:09 2011 +0200
     7.2 +++ b/src/Pure/PIDE/isar_document.scala	Thu Sep 01 14:35:51 2011 +0200
     7.3 @@ -33,8 +33,8 @@
     7.4    /* toplevel transactions */
     7.5  
     7.6    sealed abstract class Status
     7.7 +  case object Unprocessed extends Status
     7.8    case class Forked(forks: Int) extends Status
     7.9 -  case object Unprocessed extends Status
    7.10    case object Finished extends Status
    7.11    case object Failed extends Status
    7.12  
    7.13 @@ -51,6 +51,25 @@
    7.14      else Unprocessed
    7.15    }
    7.16  
    7.17 +  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
    7.18 +
    7.19 +  def node_status(
    7.20 +    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
    7.21 +  {
    7.22 +    var unprocessed = 0
    7.23 +    var running = 0
    7.24 +    var finished = 0
    7.25 +    var failed = 0
    7.26 +    node.commands.foreach(command =>
    7.27 +      command_status(state.command_state(version, command).status) match {
    7.28 +        case Unprocessed => unprocessed += 1
    7.29 +        case Forked(_) => running += 1
    7.30 +        case Finished => finished += 1
    7.31 +        case Failed => failed += 1
    7.32 +      })
    7.33 +    Node_Status(unprocessed, running, finished, failed)
    7.34 +  }
    7.35 +
    7.36  
    7.37    /* result messages */
    7.38  
    7.39 @@ -135,15 +154,20 @@
    7.40  
    7.41    /* document versions */
    7.42  
    7.43 +  def cancel_execution()
    7.44 +  {
    7.45 +    input("Isar_Document.cancel_execution")
    7.46 +  }
    7.47 +
    7.48    def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
    7.49 -    name: String, perspective: Command.Perspective)
    7.50 +    name: Document.Node.Name, perspective: Command.Perspective)
    7.51    {
    7.52      val ids =
    7.53      { import XML.Encode._
    7.54        list(long)(perspective.commands.map(_.id)) }
    7.55  
    7.56 -    input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
    7.57 -      YXML.string_of_body(ids))
    7.58 +    input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
    7.59 +      name.node, YXML.string_of_body(ids))
    7.60    }
    7.61  
    7.62    def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
    7.63 @@ -153,7 +177,7 @@
    7.64      { import XML.Encode._
    7.65        def id: T[Command] = (cmd => long(cmd.id))
    7.66        def encode: T[List[Document.Edit_Command]] =
    7.67 -        list(pair(string,
    7.68 +        list(pair((name => string(name.node)),
    7.69            variant(List(
    7.70              { case Document.Node.Clear() => (Nil, Nil) },
    7.71              { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
     8.1 --- a/src/Pure/System/session.scala	Thu Sep 01 14:21:09 2011 +0200
     8.2 +++ b/src/Pure/System/session.scala	Thu Sep 01 14:35:51 2011 +0200
     8.3 @@ -22,7 +22,7 @@
     8.4    case object Global_Settings
     8.5    case object Perspective
     8.6    case object Assignment
     8.7 -  case class Commands_Changed(set: Set[Command])
     8.8 +  case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
     8.9  
    8.10    sealed abstract class Phase
    8.11    case object Inactive extends Phase
    8.12 @@ -63,7 +63,10 @@
    8.13    private val (_, command_change_buffer) =
    8.14      Simple_Thread.actor("command_change_buffer", daemon = true)
    8.15    {
    8.16 -    var changed: Set[Command] = Set()
    8.17 +    var changed_nodes: Set[Document.Node.Name] = Set.empty
    8.18 +    var changed_commands: Set[Command] = Set.empty
    8.19 +    def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
    8.20 +
    8.21      var flush_time: Option[Long] = None
    8.22  
    8.23      def flush_timeout: Long =
    8.24 @@ -74,8 +77,10 @@
    8.25  
    8.26      def flush()
    8.27      {
    8.28 -      if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
    8.29 -      changed = Set()
    8.30 +      if (changed)
    8.31 +        commands_changed.event(Session.Commands_Changed(changed_nodes, changed_commands))
    8.32 +      changed_nodes = Set.empty
    8.33 +      changed_commands = Set.empty
    8.34        flush_time = None
    8.35      }
    8.36  
    8.37 @@ -91,7 +96,10 @@
    8.38      var finished = false
    8.39      while (!finished) {
    8.40        receiveWithin(flush_timeout) {
    8.41 -        case command: Command => changed += command; invoke()
    8.42 +        case command: Command =>
    8.43 +          changed_nodes += command.node_name
    8.44 +          changed_commands += command
    8.45 +          invoke()
    8.46          case TIMEOUT => flush()
    8.47          case Stop => finished = true; reply(())
    8.48          case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
    8.49 @@ -126,23 +134,21 @@
    8.50    private val global_state = new Volatile(Document.State.init)
    8.51    def current_state(): Document.State = global_state()
    8.52  
    8.53 -  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
    8.54 +  def snapshot(name: Document.Node.Name, pending_edits: List[Text.Edit]): Document.Snapshot =
    8.55      global_state().snapshot(name, pending_edits)
    8.56  
    8.57  
    8.58    /* theory files */
    8.59  
    8.60 -  def header_edit(name: String, master_dir: String,
    8.61 -    header: Document.Node_Header): Document.Edit_Text =
    8.62 +  def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
    8.63    {
    8.64      def norm_import(s: String): String =
    8.65      {
    8.66        val thy_name = Thy_Header.base_name(s)
    8.67        if (thy_load.is_loaded(thy_name)) thy_name
    8.68 -      else thy_load.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
    8.69 +      else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
    8.70      }
    8.71 -    def norm_use(s: String): String =
    8.72 -      thy_load.append(master_dir, Path.explode(s))
    8.73 +    def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
    8.74  
    8.75      val header1: Document.Node_Header =
    8.76        header match {
    8.77 @@ -159,12 +165,12 @@
    8.78  
    8.79    private case class Start(timeout: Time, args: List[String])
    8.80    private case object Interrupt
    8.81 -  private case class Init_Node(name: String, master_dir: String,
    8.82 +  private case class Init_Node(name: Document.Node.Name,
    8.83      header: Document.Node_Header, perspective: Text.Perspective, text: String)
    8.84 -  private case class Edit_Node(name: String, master_dir: String,
    8.85 +  private case class Edit_Node(name: Document.Node.Name,
    8.86      header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
    8.87    private case class Change_Node(
    8.88 -    name: String,
    8.89 +    name: Document.Node.Name,
    8.90      doc_edits: List[Document.Edit_Command],
    8.91      previous: Document.Version,
    8.92      version: Document.Version)
    8.93 @@ -177,7 +183,7 @@
    8.94  
    8.95      /* perspective */
    8.96  
    8.97 -    def update_perspective(name: String, text_perspective: Text.Perspective)
    8.98 +    def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
    8.99      {
   8.100        val previous = global_state().tip_version
   8.101        val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
   8.102 @@ -198,14 +204,16 @@
   8.103  
   8.104      /* incoming edits */
   8.105  
   8.106 -    def handle_edits(name: String, master_dir: String,
   8.107 +    def handle_edits(name: Document.Node.Name,
   8.108          header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
   8.109      //{{{
   8.110      {
   8.111        val syntax = current_syntax()
   8.112        val previous = global_state().history.tip.version
   8.113  
   8.114 -      val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
   8.115 +      prover.get.cancel_execution()
   8.116 +
   8.117 +      val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
   8.118        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
   8.119        val change =
   8.120          global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
   8.121 @@ -344,20 +352,20 @@
   8.122          case Interrupt if prover.isDefined =>
   8.123            prover.get.interrupt
   8.124  
   8.125 -        case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
   8.126 +        case Init_Node(name, header, perspective, text) if prover.isDefined =>
   8.127            // FIXME compare with existing node
   8.128 -          handle_edits(name, master_dir, header,
   8.129 +          handle_edits(name, header,
   8.130              List(Document.Node.Clear(),
   8.131                Document.Node.Edits(List(Text.Edit.insert(0, text))),
   8.132                Document.Node.Perspective(perspective)))
   8.133            reply(())
   8.134  
   8.135 -        case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
   8.136 +        case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
   8.137            if (text_edits.isEmpty && global_state().tip_stable &&
   8.138                perspective.range.stop <= global_state().last_exec_offset(name))
   8.139              update_perspective(name, perspective)
   8.140            else
   8.141 -            handle_edits(name, master_dir, header,
   8.142 +            handle_edits(name, header,
   8.143                List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
   8.144            reply(())
   8.145  
   8.146 @@ -386,13 +394,11 @@
   8.147  
   8.148    def interrupt() { session_actor ! Interrupt }
   8.149  
   8.150 -  // FIXME simplify signature
   8.151 -  def init_node(name: String, master_dir: String,
   8.152 +  def init_node(name: Document.Node.Name,
   8.153      header: Document.Node_Header, perspective: Text.Perspective, text: String)
   8.154 -  { session_actor !? Init_Node(name, master_dir, header, perspective, text) }
   8.155 +  { session_actor !? Init_Node(name, header, perspective, text) }
   8.156  
   8.157 -  // FIXME simplify signature
   8.158 -  def edit_node(name: String, master_dir: String, header: Document.Node_Header,
   8.159 -    perspective: Text.Perspective, edits: List[Text.Edit])
   8.160 -  { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) }
   8.161 +  def edit_node(name: Document.Node.Name,
   8.162 +    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
   8.163 +  { session_actor !? Edit_Node(name, header, perspective, edits) }
   8.164  }
     9.1 --- a/src/Pure/Thy/thy_info.scala	Thu Sep 01 14:21:09 2011 +0200
     9.2 +++ b/src/Pure/Thy/thy_info.scala	Thu Sep 01 14:35:51 2011 +0200
     9.3 @@ -25,51 +25,55 @@
     9.4  {
     9.5    /* messages */
     9.6  
     9.7 -  private def show_path(names: List[String]): String =
     9.8 -    names.map(quote).mkString(" via ")
     9.9 +  private def show_path(names: List[Document.Node.Name]): String =
    9.10 +    names.map(name => quote(name.theory)).mkString(" via ")
    9.11  
    9.12 -  private def cycle_msg(names: List[String]): String =
    9.13 +  private def cycle_msg(names: List[Document.Node.Name]): String =
    9.14      "Cyclic dependency of " + show_path(names)
    9.15  
    9.16 -  private def required_by(s: String, initiators: List[String]): String =
    9.17 +  private def required_by(initiators: List[Document.Node.Name]): String =
    9.18      if (initiators.isEmpty) ""
    9.19 -    else s + "(required by " + show_path(initiators.reverse) + ")"
    9.20 +    else "\n(required by " + show_path(initiators.reverse) + ")"
    9.21  
    9.22  
    9.23    /* dependencies */
    9.24  
    9.25 -  type Deps = Map[String, Document.Node_Header]
    9.26 -
    9.27 -  private def require_thys(initiators: List[String],
    9.28 -      deps: Deps, thys: List[(String, String)]): Deps =
    9.29 -    (deps /: thys)(require_thy(initiators, _, _))
    9.30 -
    9.31 -  private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps =
    9.32 +  def import_name(dir: String, str: String): Document.Node.Name =
    9.33    {
    9.34 -    val (dir, str) = thy
    9.35      val path = Path.explode(str)
    9.36 -    val thy_name = path.base.implode
    9.37 -    val node_name = thy_load.append(dir, Thy_Header.thy_path(path))
    9.38 +    val node = thy_load.append(dir, Thy_Header.thy_path(path))
    9.39 +    val dir1 = thy_load.append(dir, path.dir)
    9.40 +    val theory = path.base.implode
    9.41 +    Document.Node.Name(node, dir1, theory)
    9.42 +  }
    9.43 +
    9.44 +  type Deps = Map[Document.Node.Name, Document.Node_Header]
    9.45  
    9.46 -    if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps
    9.47 +  private def require_thys(initiators: List[Document.Node.Name],
    9.48 +      deps: Deps, names: List[Document.Node.Name]): Deps =
    9.49 +    (deps /: names)(require_thy(initiators, _, _))
    9.50 +
    9.51 +  private def require_thy(initiators: List[Document.Node.Name],
    9.52 +      deps: Deps, name: Document.Node.Name): Deps =
    9.53 +  {
    9.54 +    if (deps.isDefinedAt(name) || thy_load.is_loaded(name.theory)) deps
    9.55      else {
    9.56 -      val dir1 = thy_load.append(dir, path.dir)
    9.57        try {
    9.58 -        if (initiators.contains(node_name)) error(cycle_msg(initiators))
    9.59 +        if (initiators.contains(name)) error(cycle_msg(initiators))
    9.60          val header =
    9.61 -          try { thy_load.check_thy(node_name) }
    9.62 +          try { thy_load.check_thy(name) }
    9.63            catch {
    9.64              case ERROR(msg) =>
    9.65 -              cat_error(msg, "The error(s) above occurred while examining theory file " +
    9.66 -                quote(node_name) + required_by("\n", initiators))
    9.67 +              cat_error(msg, "The error(s) above occurred while examining theory " +
    9.68 +                quote(name.theory) + required_by(initiators))
    9.69            }
    9.70 -        val thys = header.imports.map(str => (dir1, str))
    9.71 -        require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys)
    9.72 +        val imports = header.imports.map(import_name(name.dir, _))
    9.73 +        require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports)
    9.74        }
    9.75 -      catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) }
    9.76 +      catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    9.77      }
    9.78    }
    9.79  
    9.80 -  def dependencies(thys: List[(String, String)]): Deps =
    9.81 -    require_thys(Nil, Map.empty, thys)
    9.82 +  def dependencies(names: List[Document.Node.Name]): Deps =
    9.83 +    require_thys(Nil, Map.empty, names)
    9.84  }
    10.1 --- a/src/Pure/Thy/thy_load.scala	Thu Sep 01 14:21:09 2011 +0200
    10.2 +++ b/src/Pure/Thy/thy_load.scala	Thu Sep 01 14:35:51 2011 +0200
    10.3 @@ -10,7 +10,7 @@
    10.4  {
    10.5    def register_thy(thy_name: String)
    10.6    def is_loaded(thy_name: String): Boolean
    10.7 -  def append(master_dir: String, path: Path): String
    10.8 -  def check_thy(node_name: String): Thy_Header
    10.9 +  def append(dir: String, path: Path): String
   10.10 +  def check_thy(node_name: Document.Node.Name): Thy_Header
   10.11  }
   10.12  
    11.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Sep 01 14:21:09 2011 +0200
    11.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Sep 01 14:35:51 2011 +0200
    11.3 @@ -27,12 +27,14 @@
    11.4        def length: Int = command.length
    11.5      }
    11.6  
    11.7 -    def parse(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
    11.8 +    def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence)
    11.9 +      : Entry =
   11.10      {
   11.11        /* stack operations */
   11.12  
   11.13        def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
   11.14 -      var stack: List[(Int, String, mutable.ListBuffer[Entry])] = List((0, root_name, buffer()))
   11.15 +      var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
   11.16 +        List((0, "theory " + node_name.theory, buffer()))
   11.17  
   11.18        @tailrec def close(level: Int => Boolean)
   11.19        {
   11.20 @@ -67,7 +69,7 @@
   11.21        /* result structure */
   11.22  
   11.23        val spans = parse_spans(syntax.scan(text))
   11.24 -      spans.foreach(span => add(Command.span(span)))
   11.25 +      spans.foreach(span => add(Command.span(node_name, span)))
   11.26        result()
   11.27      }
   11.28    }
   11.29 @@ -125,7 +127,8 @@
   11.30      }
   11.31    }
   11.32  
   11.33 -  def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective)
   11.34 +  def update_perspective(nodes: Document.Nodes,
   11.35 +      name: Document.Node.Name, text_perspective: Text.Perspective)
   11.36      : (Command.Perspective, Option[Document.Nodes]) =
   11.37    {
   11.38      val node = nodes(name)
   11.39 @@ -136,7 +139,8 @@
   11.40      (perspective, new_nodes)
   11.41    }
   11.42  
   11.43 -  def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective)
   11.44 +  def edit_perspective(previous: Document.Version,
   11.45 +      name: Document.Node.Name, text_perspective: Text.Perspective)
   11.46      : (Command.Perspective, Document.Version) =
   11.47    {
   11.48      val nodes = previous.nodes
   11.49 @@ -186,7 +190,8 @@
   11.50  
   11.51      /* phase 2: recover command spans */
   11.52  
   11.53 -    @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
   11.54 +    @tailrec def recover_spans(node_name: Document.Node.Name, commands: Linear_Set[Command])
   11.55 +      : Linear_Set[Command] =
   11.56      {
   11.57        commands.iterator.find(cmd => !cmd.is_defined) match {
   11.58          case Some(first_unparsed) =>
   11.59 @@ -212,10 +217,10 @@
   11.60                (Some(last), spans1.take(spans1.length - 1))
   11.61              else (commands.next(last), spans1)
   11.62  
   11.63 -          val inserted = spans2.map(span => new Command(Document.new_id(), span))
   11.64 +          val inserted = spans2.map(span => new Command(Document.new_id(), node_name, span))
   11.65            val new_commands =
   11.66              commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
   11.67 -          recover_spans(new_commands)
   11.68 +          recover_spans(node_name, new_commands)
   11.69  
   11.70          case None => commands
   11.71        }
   11.72 @@ -237,7 +242,7 @@
   11.73            val node = nodes(name)
   11.74            val commands0 = node.commands
   11.75            val commands1 = edit_text(text_edits, commands0)
   11.76 -          val commands2 = recover_spans(commands1)   // FIXME somewhat slow
   11.77 +          val commands2 = recover_spans(name, commands1)   // FIXME somewhat slow
   11.78  
   11.79            val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
   11.80            val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
    12.1 --- a/src/Pure/library.ML	Thu Sep 01 14:21:09 2011 +0200
    12.2 +++ b/src/Pure/library.ML	Thu Sep 01 14:35:51 2011 +0200
    12.3 @@ -959,7 +959,7 @@
    12.4  fun sort_distinct ord = quicksort true ord;
    12.5  
    12.6  val sort_strings = sort string_ord;
    12.7 -fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
    12.8 +fun sort_wrt key xs = sort (string_ord o pairself key) xs;
    12.9  
   12.10  
   12.11  (* items tagged by integer index *)
    13.1 --- a/src/Pure/library.scala	Thu Sep 01 14:21:09 2011 +0200
    13.2 +++ b/src/Pure/library.scala	Thu Sep 01 14:35:51 2011 +0200
    13.3 @@ -14,6 +14,8 @@
    13.4  import scala.swing.ComboBox
    13.5  import scala.swing.event.SelectionChanged
    13.6  import scala.collection.mutable
    13.7 +import scala.math.Ordering
    13.8 +import scala.util.Sorting
    13.9  
   13.10  
   13.11  object Library
   13.12 @@ -61,6 +63,18 @@
   13.13  
   13.14    def split_lines(str: String): List[String] = space_explode('\n', str)
   13.15  
   13.16 +  def sort_wrt[A](key: A => String, args: Seq[A]): List[A] =
   13.17 +  {
   13.18 +    val ordering: Ordering[A] =
   13.19 +      new Ordering[A] { def compare(x: A, y: A): Int = key(x) compare key(y) }
   13.20 +    val a = (new Array[Any](args.length)).asInstanceOf[Array[A]]
   13.21 +    for ((x, i) <- args.iterator zipWithIndex) a(i) = x
   13.22 +    Sorting.quickSort[A](a)(ordering)
   13.23 +    a.toList
   13.24 +  }
   13.25 +
   13.26 +  def sort_strings(args: Seq[String]): List[String] = sort_wrt((x: String) => x, args)
   13.27 +
   13.28  
   13.29    /* iterate over chunks (cf. space_explode) */
   13.30  
    14.1 --- a/src/Tools/jEdit/src/document_model.scala	Thu Sep 01 14:21:09 2011 +0200
    14.2 +++ b/src/Tools/jEdit/src/document_model.scala	Thu Sep 01 14:35:51 2011 +0200
    14.3 @@ -45,11 +45,10 @@
    14.4      }
    14.5    }
    14.6  
    14.7 -  def init(session: Session, buffer: Buffer,
    14.8 -    master_dir: String, node_name: String, thy_name: String): Document_Model =
    14.9 +  def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
   14.10    {
   14.11      exit(buffer)
   14.12 -    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
   14.13 +    val model = new Document_Model(session, buffer, name)
   14.14      buffer.setProperty(key, model)
   14.15      model.activate()
   14.16      model
   14.17 @@ -57,15 +56,14 @@
   14.18  }
   14.19  
   14.20  
   14.21 -class Document_Model(val session: Session, val buffer: Buffer,
   14.22 -  val master_dir: String, val node_name: String, val thy_name: String)
   14.23 +class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
   14.24  {
   14.25    /* header */
   14.26  
   14.27    def node_header(): Exn.Result[Thy_Header] =
   14.28    {
   14.29      Swing_Thread.require()
   14.30 -    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
   14.31 +    Exn.capture { Thy_Header.check(name.theory, buffer.getSegment(0, buffer.getLength)) }
   14.32    }
   14.33  
   14.34  
   14.35 @@ -105,15 +103,14 @@
   14.36          case edits =>
   14.37            pending.clear
   14.38            last_perspective = new_perspective
   14.39 -          session.edit_node(node_name, master_dir, node_header(), new_perspective, edits)
   14.40 +          session.edit_node(name, node_header(), new_perspective, edits)
   14.41        }
   14.42      }
   14.43  
   14.44      def init()
   14.45      {
   14.46        flush()
   14.47 -      session.init_node(node_name, master_dir,
   14.48 -        node_header(), perspective(), Isabelle.buffer_text(buffer))
   14.49 +      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
   14.50      }
   14.51  
   14.52      private val delay_flush =
   14.53 @@ -145,7 +142,7 @@
   14.54    def snapshot(): Document.Snapshot =
   14.55    {
   14.56      Swing_Thread.require()
   14.57 -    session.snapshot(node_name, pending_edits.snapshot())
   14.58 +    session.snapshot(name, pending_edits.snapshot())
   14.59    }
   14.60  
   14.61  
    15.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Sep 01 14:21:09 2011 +0200
    15.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Sep 01 14:35:51 2011 +0200
    15.3 @@ -442,27 +442,29 @@
    15.4    private val main_actor = actor {
    15.5      loop {
    15.6        react {
    15.7 -        case Session.Commands_Changed(changed) =>
    15.8 +        case changed: Session.Commands_Changed =>
    15.9            val buffer = model.buffer
   15.10            Isabelle.swing_buffer_lock(buffer) {
   15.11              val (updated, snapshot) = flush_snapshot()
   15.12              val visible = visible_range()
   15.13  
   15.14 -            if (updated || changed.exists(snapshot.node.commands.contains))
   15.15 +            if (updated ||
   15.16 +                (changed.nodes.contains(model.name) &&
   15.17 +                 changed.commands.exists(snapshot.node.commands.contains)))
   15.18                overview.repaint()
   15.19  
   15.20              if (updated) invalidate_range(visible)
   15.21              else {
   15.22                val visible_cmds =
   15.23                  snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
   15.24 -              if (visible_cmds.exists(changed)) {
   15.25 +              if (visible_cmds.exists(changed.commands)) {
   15.26                  for {
   15.27                    line <- 0 until text_area.getVisibleLines
   15.28                    val start = text_area.getScreenLineStartOffset(line) if start >= 0
   15.29                    val end = text_area.getScreenLineEndOffset(line) if end >= 0
   15.30                    val range = proper_line_range(start, end)
   15.31                    val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   15.32 -                  if line_cmds.exists(changed)
   15.33 +                  if line_cmds.exists(changed.commands)
   15.34                  } text_area.invalidateScreenLineRange(line, line)
   15.35                }
   15.36              }
    16.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 14:21:09 2011 +0200
    16.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 14:35:51 2011 +0200
    16.3 @@ -74,10 +74,10 @@
    16.4                      (props, props) match {
    16.5                        case (Position.Id(def_id), Position.Offset(def_offset)) =>
    16.6                          snapshot.state.find_command(snapshot.version, def_id) match {
    16.7 -                          case Some((def_name, def_node, def_cmd)) =>
    16.8 +                          case Some((def_node, def_cmd)) =>
    16.9                              def_node.command_start(def_cmd) match {
   16.10                                case Some(def_cmd_start) =>
   16.11 -                                new Internal_Hyperlink(def_name, begin, end, line,
   16.12 +                                new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
   16.13                                    def_cmd_start + def_cmd.decode(def_offset))
   16.14                                case None => null
   16.15                              }
    17.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Thu Sep 01 14:21:09 2011 +0200
    17.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Thu Sep 01 14:35:51 2011 +0200
    17.3 @@ -24,7 +24,11 @@
    17.4    def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
    17.5  
    17.6    val outdated_color = new Color(238, 227, 227)
    17.7 -  val unfinished_color = new Color(255, 228, 225)
    17.8 +  val outdated1_color = new Color(238, 227, 227, 50)
    17.9 +  val running_color = new Color(97, 0, 97)
   17.10 +  val running1_color = new Color(97, 0, 97, 100)
   17.11 +  val unfinished_color = new Color(255, 160, 160)
   17.12 +  val unfinished1_color = new Color(255, 160, 160, 50)
   17.13  
   17.14    val light_color = new Color(240, 240, 240)
   17.15    val regular_color = new Color(192, 192, 192)
   17.16 @@ -53,11 +57,11 @@
   17.17    def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   17.18    {
   17.19      val state = snapshot.command_state(command)
   17.20 -    if (snapshot.is_outdated) Some(outdated_color)
   17.21 +    if (snapshot.is_outdated) Some(outdated1_color)
   17.22      else
   17.23        Isar_Document.command_status(state.status) match {
   17.24 -        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
   17.25 -        case Isar_Document.Unprocessed => Some(unfinished_color)
   17.26 +        case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
   17.27 +        case Isar_Document.Unprocessed => Some(unfinished1_color)
   17.28          case _ => None
   17.29        }
   17.30    }
   17.31 @@ -68,7 +72,7 @@
   17.32      if (snapshot.is_outdated) None
   17.33      else
   17.34        Isar_Document.command_status(state.status) match {
   17.35 -        case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
   17.36 +        case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
   17.37          case Isar_Document.Unprocessed => Some(unfinished_color)
   17.38          case Isar_Document.Failed => Some(error_color)
   17.39          case Isar_Document.Finished =>
    18.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 01 14:21:09 2011 +0200
    18.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 01 14:35:51 2011 +0200
    18.3 @@ -138,7 +138,7 @@
    18.4        }
    18.5  
    18.6      val text = Isabelle.buffer_text(model.buffer)
    18.7 -    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
    18.8 +    val structure = Structure.parse(syntax, model.name, text)
    18.9  
   18.10      make_tree(0, structure) foreach (node => data.root.add(node))
   18.11    }
    19.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Sep 01 14:21:09 2011 +0200
    19.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Sep 01 14:35:51 2011 +0200
    19.3 @@ -33,23 +33,23 @@
    19.4  
    19.5    /* file-system operations */
    19.6  
    19.7 -  override def append(master_dir: String, source_path: Path): String =
    19.8 +  override def append(dir: String, source_path: Path): String =
    19.9    {
   19.10      val path = source_path.expand
   19.11      if (path.is_absolute) Isabelle_System.platform_path(path)
   19.12      else {
   19.13 -      val vfs = VFSManager.getVFSForPath(master_dir)
   19.14 +      val vfs = VFSManager.getVFSForPath(dir)
   19.15        if (vfs.isInstanceOf[FileVFS])
   19.16          MiscUtilities.resolveSymlinks(
   19.17 -          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
   19.18 -      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
   19.19 +          vfs.constructPath(dir, Isabelle_System.platform_path(path)))
   19.20 +      else vfs.constructPath(dir, Isabelle_System.standard_path(path))
   19.21      }
   19.22    }
   19.23  
   19.24 -  override def check_thy(node_name: String): Thy_Header =
   19.25 +  override def check_thy(name: Document.Node.Name): Thy_Header =
   19.26    {
   19.27      Swing_Thread.now {
   19.28 -      Isabelle.jedit_buffer(node_name) match {
   19.29 +      Isabelle.jedit_buffer(name.node) match {
   19.30          case Some(buffer) =>
   19.31            Isabelle.buffer_lock(buffer) {
   19.32              val text = new Segment
   19.33 @@ -59,7 +59,7 @@
   19.34          case None => None
   19.35        }
   19.36      } getOrElse {
   19.37 -      val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
   19.38 +      val file = new File(name.node)  // FIXME load URL via jEdit VFS (!?)
   19.39        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
   19.40        Thy_Header.read(file)
   19.41      }
    20.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Thu Sep 01 14:21:09 2011 +0200
    20.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Sep 01 14:35:51 2011 +0200
    20.3 @@ -105,7 +105,7 @@
    20.4      loop {
    20.5        react {
    20.6          case Session.Global_Settings => handle_resize()
    20.7 -        case Session.Commands_Changed(changed) => handle_update(Some(changed))
    20.8 +        case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
    20.9          case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
   20.10          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
   20.11        }
    21.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 14:21:09 2011 +0200
    21.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 14:35:51 2011 +0200
    21.3 @@ -14,8 +14,7 @@
    21.4  import javax.swing.JOptionPane
    21.5  
    21.6  import scala.collection.mutable
    21.7 -import scala.swing.ComboBox
    21.8 -import scala.util.Sorting
    21.9 +import scala.swing.{ComboBox, ListView, ScrollPane}
   21.10  
   21.11  import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
   21.12    Buffer, EditPane, ServiceManager, View}
   21.13 @@ -169,9 +168,6 @@
   21.14  
   21.15    def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
   21.16  
   21.17 -  def buffer_path(buffer: Buffer): (String, String) =
   21.18 -    (buffer.getDirectory, buffer_name(buffer))
   21.19 -
   21.20  
   21.21    /* main jEdit components */
   21.22  
   21.23 @@ -217,10 +213,11 @@
   21.24          document_model(buffer) match {
   21.25            case Some(model) => Some(model)
   21.26            case None =>
   21.27 -            val (master_dir, path) = buffer_path(buffer)
   21.28 -            Thy_Header.thy_name(path) match {
   21.29 -              case Some(name) =>
   21.30 -                Some(Document_Model.init(session, buffer, master_dir, path, name))
   21.31 +            val name = buffer_name(buffer)
   21.32 +            Thy_Header.thy_name(name) match {
   21.33 +              case Some(theory) =>
   21.34 +                val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
   21.35 +                Some(Document_Model.init(session, buffer, node_name))
   21.36                case None => None
   21.37              }
   21.38          }
   21.39 @@ -364,23 +361,25 @@
   21.40  
   21.41        val thys =
   21.42          for (buffer <- buffers; model <- Isabelle.document_model(buffer))
   21.43 -          yield (model.master_dir, model.thy_name)
   21.44 -      val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
   21.45 +          yield model.name
   21.46 +      val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _)
   21.47  
   21.48 -      val do_load = !files.isEmpty &&
   21.49 -        {
   21.50 -          val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
   21.51 -          val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
   21.52 -          files_text.editable = false
   21.53 +      if (!files.isEmpty) {
   21.54 +        val files_list = new ListView(Library.sort_strings(files))
   21.55 +        for (i <- 0 until files.length)
   21.56 +          files_list.selection.indices += i
   21.57 +
   21.58 +        val answer =
   21.59            Library.confirm_dialog(jEdit.getActiveView(),
   21.60              "Auto loading of required files",
   21.61              JOptionPane.YES_NO_OPTION,
   21.62 -            "The following files are required to resolve theory imports.  Reload now?",
   21.63 -            files_text) == 0
   21.64 -        }
   21.65 -      if (do_load)
   21.66 -        for (file <- files if !loaded_buffer(file))
   21.67 -          jEdit.openFile(null: View, file)
   21.68 +            "The following files are required to resolve theory imports.",
   21.69 +            "Reload selected files now?",
   21.70 +            new ScrollPane(files_list))
   21.71 +        if (answer == 0)
   21.72 +          files_list.selection.items foreach (file =>
   21.73 +            if (!loaded_buffer(file)) jEdit.openFile(null: View, file))
   21.74 +      }
   21.75      }
   21.76  
   21.77  
    22.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 14:21:09 2011 +0200
    22.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 14:35:51 2011 +0200
    22.3 @@ -10,11 +10,13 @@
    22.4  import isabelle._
    22.5  
    22.6  import scala.actors.Actor._
    22.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
    22.8 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView,
    22.9 +  ScrollPane, TabbedPane, Component, Swing}
   22.10  import scala.swing.event.{ButtonClicked, SelectionChanged}
   22.11  
   22.12  import java.lang.System
   22.13  import java.awt.BorderLayout
   22.14 +import javax.swing.JList
   22.15  import javax.swing.border.{BevelBorder, SoftBevelBorder}
   22.16  
   22.17  import org.gjt.sp.jedit.View
   22.18 @@ -27,11 +29,16 @@
   22.19    private val readme = new HTML_Panel("SansSerif", 14)
   22.20    readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
   22.21  
   22.22 +  val status = new ListView(Nil: List[String])
   22.23 +  status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
   22.24 +  status.selection.intervalMode = ListView.IntervalMode.Single
   22.25 +
   22.26    private val syslog = new TextArea(Isabelle.session.syslog())
   22.27  
   22.28    private val tabs = new TabbedPane {
   22.29      pages += new TabbedPane.Page("README", Component.wrap(readme))
   22.30 -    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
   22.31 +    pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
   22.32 +    pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
   22.33  
   22.34      selection.index =
   22.35      {
   22.36 @@ -64,6 +71,36 @@
   22.37    add(controls.peer, BorderLayout.NORTH)
   22.38  
   22.39  
   22.40 +  /* component state -- owned by Swing thread */
   22.41 +
   22.42 +  private var nodes_status: Map[Document.Node.Name, String] = Map.empty
   22.43 +
   22.44 +  private def handle_changed(changed_nodes: Set[Document.Node.Name])
   22.45 +  {
   22.46 +    Swing_Thread.now {
   22.47 +      // FIXME correlation to changed_nodes!?
   22.48 +      val state = Isabelle.session.current_state()
   22.49 +      state.recent_stable.map(change => change.version.get_finished) match {
   22.50 +        case None =>
   22.51 +        case Some(version) =>
   22.52 +          var nodes_status1 = nodes_status
   22.53 +          for {
   22.54 +            name <- changed_nodes
   22.55 +            node <- version.nodes.get(name)
   22.56 +            val status = Isar_Document.node_status(state, version, node)
   22.57 +          } nodes_status1 += (name -> status.toString)
   22.58 +
   22.59 +          if (nodes_status != nodes_status1) {
   22.60 +            nodes_status = nodes_status1
   22.61 +            val order =
   22.62 +              Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
   22.63 +            status.listData = order.map(name => name.theory + " " + nodes_status(name))
   22.64 +          }
   22.65 +      }
   22.66 +    }
   22.67 +  }
   22.68 +
   22.69 +
   22.70    /* main actor */
   22.71  
   22.72    private val main_actor = actor {
   22.73 @@ -83,6 +120,8 @@
   22.74          case phase: Session.Phase =>
   22.75            Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
   22.76  
   22.77 +        case changed: Session.Commands_Changed => handle_changed(changed.nodes)
   22.78 +
   22.79          case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
   22.80        }
   22.81      }
   22.82 @@ -91,10 +130,12 @@
   22.83    override def init() {
   22.84      Isabelle.session.raw_messages += main_actor
   22.85      Isabelle.session.phase_changed += main_actor
   22.86 +    Isabelle.session.commands_changed += main_actor
   22.87    }
   22.88  
   22.89    override def exit() {
   22.90      Isabelle.session.raw_messages -= main_actor
   22.91      Isabelle.session.phase_changed -= main_actor
   22.92 +    Isabelle.session.commands_changed -= main_actor
   22.93    }
   22.94  }