# HG changeset patch
# User wenzelm
# Date 1314876885 -7200
# Node ID a4ff8a7872025a18633cca7fe7a3cbe1b6c58ba0
# Parent  466ea227e00dbf65d9604bfac9ffc7b2b9661da3
more abstract Document.Node.Name;
tuned signature;

diff -r 466ea227e00d -r a4ff8a787202 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -80,9 +80,10 @@
   /* 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(node_name: String, toks: List[Token]): Command =
+  def span(node_name: Document.Node.Name, toks: List[Token]): Command =
     new Command(Document.no_id, node_name, toks)
 
 
@@ -110,7 +111,7 @@
 
 class Command(
     val id: Document.Command_ID,
-    val node_name: String,
+    val node_name: Document.Node.Name,
     val span: List[Token])
 {
   /* classification */
diff -r 466ea227e00d -r a4ff8a787202 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Sep 01 13:34:45 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, master_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)
 
 
@@ -335,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
@@ -371,7 +381,7 @@
 
 
     // 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
diff -r 466ea227e00d -r a4ff8a787202 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -160,14 +160,14 @@
   }
 
   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,
@@ -177,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)) },
diff -r 466ea227e00d -r a4ff8a787202 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Pure/System/session.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -22,7 +22,7 @@
   case object Global_Settings
   case object Perspective
   case object Assignment
-  case class Commands_Changed(nodes: Set[String], commands: 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,7 @@
   private val (_, command_change_buffer) =
     Simple_Thread.actor("command_change_buffer", daemon = true)
   {
-    var changed_nodes: Set[String] = Set.empty
+    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
 
@@ -134,23 +134,22 @@
   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,
-    header: Document.Node_Header): Document.Edit_Text =
+  def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
   {
     def norm_import(s: String): String =
     {
       val thy_name = Thy_Header.base_name(s)
       if (thy_load.is_loaded(thy_name)) thy_name
-      else thy_load.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
+      else thy_load.append(name.master_dir, Thy_Header.thy_path(Path.explode(s)))
     }
     def norm_use(s: String): String =
-      thy_load.append(master_dir, Path.explode(s))
+      thy_load.append(name.master_dir, Path.explode(s))
 
     val header1: Document.Node_Header =
       header match {
@@ -167,12 +166,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,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)
-  private case class Edit_Node(name: String, master_dir: String,
+  private case class Edit_Node(name: Document.Node.Name,
     header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
   private case class Change_Node(
-    name: String,
+    name: Document.Node.Name,
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
     version: Document.Version)
@@ -185,7 +184,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)
@@ -206,7 +205,7 @@
 
     /* incoming edits */
 
-    def handle_edits(name: String, master_dir: String,
+    def handle_edits(name: Document.Node.Name,
         header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
     //{{{
     {
@@ -215,7 +214,7 @@
 
       prover.get.cancel_execution()
 
-      val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
+      val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
       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)))
@@ -354,20 +353,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
-          handle_edits(name, master_dir, header,
+          handle_edits(name, header,
             List(Document.Node.Clear(),
               Document.Node.Edits(List(Text.Edit.insert(0, text))),
               Document.Node.Perspective(perspective)))
           reply(())
 
-        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
-            handle_edits(name, master_dir, header,
+            handle_edits(name, header,
               List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
           reply(())
 
@@ -396,13 +395,11 @@
 
   def interrupt() { session_actor ! Interrupt }
 
-  // FIXME simplify signature
-  def init_node(name: String, master_dir: String,
+  def init_node(name: Document.Node.Name,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)
-  { session_actor !? Init_Node(name, master_dir, header, perspective, text) }
+  { session_actor !? Init_Node(name, header, perspective, text) }
 
-  // FIXME simplify signature
-  def edit_node(name: String, master_dir: String, header: Document.Node_Header,
-    perspective: Text.Perspective, edits: List[Text.Edit])
-  { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) }
+  def edit_node(name: Document.Node.Name,
+    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
+  { session_actor !? Edit_Node(name, header, perspective, edits) }
 }
diff -r 466ea227e00d -r a4ff8a787202 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -25,51 +25,54 @@
 {
   /* 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(master_dir: String, str: String): Document.Node.Name =
   {
-    val (dir, str) = thy
     val path = Path.explode(str)
-    val thy_name = path.base.implode
-    val node_name = thy_load.append(dir, Thy_Header.thy_path(path))
+    val node_name = thy_load.append(master_dir, Thy_Header.thy_path(path))
+    val master_dir1 = thy_load.append(master_dir, path.dir)
+    Document.Node.Name(node_name, master_dir1, path.base.implode)
+  }
+
+  type Deps = Map[Document.Node.Name, Document.Node_Header]
 
-    if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps
+  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 =
+  {
+    if (deps.isDefinedAt(name) || thy_load.is_loaded(name.theory)) 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))
         val header =
-          try { thy_load.check_thy(node_name) }
+          try { thy_load.check_thy(name) }
           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.master_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)
 }
diff -r 466ea227e00d -r a4ff8a787202 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Pure/Thy/thy_load.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -11,6 +11,6 @@
   def register_thy(thy_name: String)
   def is_loaded(thy_name: String): Boolean
   def append(master_dir: String, path: Path): String
-  def check_thy(node_name: String): Thy_Header
+  def check_thy(node_name: Document.Node.Name): Thy_Header
 }
 
diff -r 466ea227e00d -r a4ff8a787202 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -27,13 +27,14 @@
       def length: Int = command.length
     }
 
-    def parse(syntax: Outer_Syntax, node_name: String, root_name: String, text: CharSequence)
+    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)
       {
@@ -126,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)
@@ -137,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
@@ -187,7 +190,7 @@
 
     /* phase 2: recover command spans */
 
-    @tailrec def recover_spans(node_name: String, commands: 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 {
diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Sep 01 13:34:45 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)
 {
   /* header */
 
   def node_header(): Exn.Result[Thy_Header] =
   {
     Swing_Thread.require()
-    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)
+          session.edit_node(name, node_header(), new_perspective, edits)
       }
     }
 
     def init()
     {
       flush()
-      session.init_node(node_name, master_dir,
-        node_header(), perspective(), Isabelle.buffer_text(buffer))
+      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
     }
 
     private val delay_flush =
@@ -145,7 +142,7 @@
   def snapshot(): Document.Snapshot =
   {
     Swing_Thread.require()
-    session.snapshot(node_name, pending_edits.snapshot())
+    session.snapshot(name, pending_edits.snapshot())
   }
 
 
diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -449,7 +449,7 @@
             val visible = visible_range()
 
             if (updated ||
-                (changed.nodes.contains(model.node_name) &&
+                (changed.nodes.contains(model.name) &&
                  changed.commands.exists(snapshot.node.commands.contains)))
               overview.repaint()
 
diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -77,7 +77,7 @@
                           case Some((def_node, def_cmd)) =>
                             def_node.command_start(def_cmd) match {
                               case Some(def_cmd_start) =>
-                                new Internal_Hyperlink(def_cmd.node_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
                             }
diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -138,7 +138,7 @@
       }
 
     val text = Isabelle.buffer_text(model.buffer)
-    val structure = Structure.parse(syntax, model.node_name, "theory " + model.thy_name, text)
+    val structure = Structure.parse(syntax, model.name, text)
 
     make_tree(0, structure) foreach (node => data.root.add(node))
   }
diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Sep 01 13:34:45 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])
         MiscUtilities.resolveSymlinks(
-          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 =
   {
     Swing_Thread.now {
-      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))
       Thy_Header.read(file)
     }
diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -168,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 */
 
@@ -216,10 +213,11 @@
         document_model(buffer) match {
           case Some(model) => Some(model)
           case None =>
-            val (master_dir, path) = buffer_path(buffer)
-            Thy_Header.thy_name(path) match {
-              case Some(name) =>
-                Some(Document_Model.init(session, buffer, master_dir, path, name))
+            val name = buffer_name(buffer)
+            Thy_Header.thy_name(name) match {
+              case Some(theory) =>
+                val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
+                Some(Document_Model.init(session, buffer, node_name))
               case None => None
             }
         }
@@ -363,8 +361,8 @@
 
       val thys =
         for (buffer <- buffers; model <- Isabelle.document_model(buffer))
-          yield (model.master_dir, model.thy_name)
-      val files = thy_info.dependencies(thys).toList.map(_._1).filterNot(loaded_buffer _)
+          yield model.name
+      val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _)
 
       if (!files.isEmpty) {
         val files_list = new ListView(Library.sort_strings(files))
diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 11:33:44 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 13:34:45 2011 +0200
@@ -75,7 +75,7 @@
 
   private var nodes_status: Map[String, String] = Map.empty
 
-  private def handle_changed(changed_nodes: Set[String])
+  private def handle_changed(changed_nodes: Set[Document.Node.Name])
   {
     Swing_Thread.now {
       // FIXME correlation to changed_nodes!?
@@ -88,7 +88,7 @@
             name <- changed_nodes
             node <- version.nodes.get(name)
             val status = Isar_Document.node_status(state, version, node)
-          } nodes_status1 += (name -> status.toString)
+          } nodes_status1 += (name.node -> status.toString)
 
           if (nodes_status != nodes_status1) {
             nodes_status = nodes_status1