more robust Thy_Header.base_name, with minimal assumptions about path syntax;
Isabelle.buffer_path: keep platform syntax;

--- a/src/Pure/System/session.scala	Tue Aug 16 21:54:06 2011 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 16 22:48:31 2011 +0200
@@ -191,7 +191,7 @@
 
       def norm_import(s: String): String =
       {
-        val name = Thy_Info.base_name(s)
+        val name = Thy_Header.base_name(s)
         if (thy_load.is_loaded(name)) name
         else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
       }

--- a/src/Pure/Thy/thy_header.scala	Tue Aug 16 21:54:06 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Aug 16 22:48:31 2011 +0200
@@ -28,8 +28,12 @@
 
   /* theory file name */
 
+  private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
 
+  def base_name(s: String): String =
+    s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
+
   def thy_name(s: String): Option[String] =
     s match { case Thy_Name(name) => Some(name) case _ => None }
 

--- a/src/Pure/Thy/thy_info.ML	Tue Aug 16 21:54:06 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 16 22:48:31 2011 +0200
@@ -9,7 +9,6 @@
 sig
   datatype action = Update | Remove
   val add_hook: (action -> string -> unit) -> unit
-  val base_name: string -> string
   val get_names: unit -> string list
   val status: unit -> unit
   val lookup_theory: string -> theory option
@@ -46,11 +45,6 @@
 
 (** thy database **)
 
-(* base name *)
-
-fun base_name s = Path.implode (Path.base (Path.explode s));
-
-
 (* messages *)
 
 fun loader_msg txt [] = "Theory loader: " ^ txt
@@ -78,6 +72,7 @@
 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 21:54:06 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Aug 16 22:48:31 2011 +0200
@@ -9,11 +9,6 @@
 
 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 21:54:06 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 22:48:31 2011 +0200
@@ -190,9 +190,7 @@
   {
     val master_dir = buffer.getDirectory
     val path = buffer.getSymlinkPath
-    if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
-      (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
-    else (master_dir, path)
+    (master_dir, path)
   }