# HG changeset patch
# User wenzelm
# Date 1313527711 -7200
# Node ID a8f921e6484fb99f6bd22395c5a76dba15098317
# Parent  4040d0ffac7b0500f900616feb8688eeb988e848
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
Isabelle.buffer_path: keep platform syntax;

diff -r 4040d0ffac7b -r a8f921e6484f src/Pure/System/session.scala
--- 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)))
       }
diff -r 4040d0ffac7b -r a8f921e6484f src/Pure/Thy/thy_header.scala
--- 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 }
 
diff -r 4040d0ffac7b -r a8f921e6484f src/Pure/Thy/thy_info.ML
--- 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);
diff -r 4040d0ffac7b -r a8f921e6484f src/Pure/Thy/thy_info.scala
--- 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 {
diff -r 4040d0ffac7b -r a8f921e6484f src/Tools/jEdit/src/plugin.scala
--- 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)
   }