use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
more robust treatment of node dependencies;
misc tuning;

--- a/src/Pure/PIDE/document.ML	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 16 21:13:52 2011 +0200
@@ -142,21 +142,16 @@
       | Header header =>
           let
             val node = get_node nodes name;
-            val nodes' = Graph.new_node (name, node) (remove_node name nodes);
-            val parents =
-              (case header of Exn.Res (_, parents, _) => parents | _ => [])
-              |> filter (can (Graph.get_node nodes'));
-            val (header', nodes'') =
-              (header, Graph.add_deps_acyclic (name, parents) nodes')
-                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes')
-                  | Graph.UNDEF d => (Exn.Exn (ERROR ("Undefined theory entry: " ^ quote d)), nodes')
-          in
-            nodes''
-            |> Graph.map_node name (set_header header')
-          end));
+            val nodes1 = Graph.new_node (name, node) (remove_node name nodes);
+            val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
+            val nodes2 = fold default_node parents nodes1;
+            val (header', nodes3) =
+              (header, Graph.add_deps_acyclic (name, parents) nodes2)
+                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
+          in Graph.map_node name (set_header header') nodes3 end));
 
-fun def_node name (Version nodes) = Version (default_node name nodes);
-fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes);
+fun put_node (name, node) (Version nodes) =
+  Version (update_node name (K node) nodes);
 
 end;
 
@@ -331,10 +326,7 @@
   let
     val old_version = the_version state old_id;
     val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
-    val new_version =
-      old_version
-      |> fold (def_node o #1) edits
-      |> fold edit_nodes edits;
+    val new_version = fold edit_nodes edits old_version;
 
     val updates =
       nodes_of new_version |> Graph.schedule
@@ -352,11 +344,11 @@
 
                     val parents =
                       imports |> map (fn import =>
-                        (case AList.lookup (op =) deps import of
-                          SOME parent_future =>
-                            get_theory (Position.file_only (import ^ ".thy"))
-                              (#2 (Future.join parent_future))
-                        | NONE => Thy_Info.get_theory (Thy_Info.base_name import)));
+                        (case Thy_Info.lookup_theory import of
+                          SOME thy => thy
+                        | NONE =>
+                            get_theory (Position.file_only import)
+                              (#2 (Future.join (the (AList.lookup (op =) deps import))))));
                   in Thy_Load.begin_theory dir thy_name imports files parents end
                 fun get_command id =
                   (id, the_command state id |> Future.map (Toplevel.modify_init init));

--- a/src/Pure/PIDE/document.scala	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 16 21:13:52 2011 +0200
@@ -53,9 +53,9 @@
     case class Edits[A](edits: List[A]) extends Edit[A]
     case class Header[A](header: Node_Header) extends Edit[A]
 
-    def norm_header[A](f: String => String, header: Node_Header): Header[A] =
+    def norm_header[A](f: String => String, g: String => String, header: Node_Header): Header[A] =
       header match {
-        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) })
+        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f, g) })
         case exn => Header[A](exn)
       }
 

--- a/src/Pure/System/session.scala	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 16 21:13:52 2011 +0200
@@ -189,9 +189,15 @@
       val syntax = current_syntax()
       val previous = global_state().history.tip.version
 
-      val norm_header =
-        Document.Node.norm_header[Text.Edit](
-          name => file_store.append(master_dir, Path.explode(name)), header)
+      def norm_import(s: String): String =
+      {
+        val name = Thy_Info.base_name(s)
+        if (thy_load.is_loaded(name)) name
+        else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
+      }
+      def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s))
+      val norm_header = Document.Node.norm_header[Text.Edit](norm_import, norm_use, header)
+
       val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
       val change =

--- a/src/Pure/Thy/thy_header.scala	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Aug 16 21:13:52 2011 +0200
@@ -28,11 +28,12 @@
 
   /* theory file name */
 
-  private val Thy_Name = new Regex("""(.*?)([^/\\:]+)\.thy""")
+  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
 
-  def thy_name(s: String): Option[(String, String)] =
-    s match { case Thy_Name(prefix, name) => Some((prefix, name)) case _ => None }
+  def thy_name(s: String): Option[String] =
+    s match { case Thy_Name(name) => Some(name) case _ => None }
 
+  def thy_path(path: Path): Path = path.ext("thy")
   def thy_path(name: String): Path = Path.basic(name).ext("thy")
 
 
@@ -113,7 +114,7 @@
   def map(f: String => String): Thy_Header =
     Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
 
-  def norm_deps(f: String => String): Thy_Header =
-    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (f(p._1), p._2)))
+  def norm_deps(f: String => String, g: String => String): Thy_Header =
+    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
 }
 

--- a/src/Pure/Thy/thy_info.ML	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 16 21:13:52 2011 +0200
@@ -46,6 +46,11 @@
 
 (** thy database **)
 
+(* base name *)
+
+fun base_name s = Path.implode (Path.base (Path.explode s));
+
+
 (* messages *)
 
 fun loader_msg txt [] = "Theory loader: " ^ txt
@@ -73,7 +78,6 @@
 fun make_deps master imports : deps = {master = master, imports = imports};
 
 fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
-fun base_name s = Path.implode (Path.base (Path.explode s));
 
 local
   val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);

--- a/src/Pure/Thy/thy_info.scala	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Aug 16 21:13:52 2011 +0200
@@ -9,6 +9,11 @@
 
 object Thy_Info
 {
+  /* base name */
+
+  def base_name(s: String): String = Path.explode(s).base.implode
+
+
   /* protocol messages */
 
   object Loaded_Theory {

--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 21:13:52 2011 +0200
@@ -210,8 +210,8 @@
           case None =>
             val (master_dir, path) = buffer_path(buffer)
             Thy_Header.thy_name(path) match {
-              case Some((prefix, name)) =>
-                Some(Document_Model.init(session, buffer, master_dir, prefix + name, name))
+              case Some(name) =>
+                Some(Document_Model.init(session, buffer, master_dir, path, name))
               case None => None
             }
         }
@@ -334,8 +334,8 @@
       else {
         val vfs = VFSManager.getVFSForPath(master_dir)
         if (vfs.isInstanceOf[FileVFS])
-          vfs.constructPath(master_dir, Isabelle_System.platform_path(path))
-          // FIXME MiscUtilities.resolveSymlinks (!?)
+          MiscUtilities.resolveSymlinks(
+            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
         else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
       }
     }