more robust Thy_Header.base_name, with minimal assumptions about path syntax;
authorwenzelm
Tue Aug 16 22:48:31 2011 +0200 (2011-08-16)
changeset 44225a8f921e6484f
parent 44224 4040d0ffac7b
child 44226 1ea760da0f2d
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
Isabelle.buffer_path: keep platform syntax;
src/Pure/System/session.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_info.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/System/session.scala	Tue Aug 16 21:54:06 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Tue Aug 16 22:48:31 2011 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4  
     1.5        def norm_import(s: String): String =
     1.6        {
     1.7 -        val name = Thy_Info.base_name(s)
     1.8 +        val name = Thy_Header.base_name(s)
     1.9          if (thy_load.is_loaded(name)) name
    1.10          else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
    1.11        }
     2.1 --- a/src/Pure/Thy/thy_header.scala	Tue Aug 16 21:54:06 2011 +0200
     2.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Aug 16 22:48:31 2011 +0200
     2.3 @@ -28,8 +28,12 @@
     2.4  
     2.5    /* theory file name */
     2.6  
     2.7 +  private val Base_Name = new Regex(""".*?([^/\\:]+)""")
     2.8    private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
     2.9  
    2.10 +  def base_name(s: String): String =
    2.11 +    s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    2.12 +
    2.13    def thy_name(s: String): Option[String] =
    2.14      s match { case Thy_Name(name) => Some(name) case _ => None }
    2.15  
     3.1 --- a/src/Pure/Thy/thy_info.ML	Tue Aug 16 21:54:06 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Aug 16 22:48:31 2011 +0200
     3.3 @@ -9,7 +9,6 @@
     3.4  sig
     3.5    datatype action = Update | Remove
     3.6    val add_hook: (action -> string -> unit) -> unit
     3.7 -  val base_name: string -> string
     3.8    val get_names: unit -> string list
     3.9    val status: unit -> unit
    3.10    val lookup_theory: string -> theory option
    3.11 @@ -46,11 +45,6 @@
    3.12  
    3.13  (** thy database **)
    3.14  
    3.15 -(* base name *)
    3.16 -
    3.17 -fun base_name s = Path.implode (Path.base (Path.explode s));
    3.18 -
    3.19 -
    3.20  (* messages *)
    3.21  
    3.22  fun loader_msg txt [] = "Theory loader: " ^ txt
    3.23 @@ -78,6 +72,7 @@
    3.24  fun make_deps master imports : deps = {master = master, imports = imports};
    3.25  
    3.26  fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
    3.27 +fun base_name s = Path.implode (Path.base (Path.explode s));
    3.28  
    3.29  local
    3.30    val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
     4.1 --- a/src/Pure/Thy/thy_info.scala	Tue Aug 16 21:54:06 2011 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Aug 16 22:48:31 2011 +0200
     4.3 @@ -9,11 +9,6 @@
     4.4  
     4.5  object Thy_Info
     4.6  {
     4.7 -  /* base name */
     4.8 -
     4.9 -  def base_name(s: String): String = Path.explode(s).base.implode
    4.10 -
    4.11 -
    4.12    /* protocol messages */
    4.13  
    4.14    object Loaded_Theory {
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 21:54:06 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 22:48:31 2011 +0200
     5.3 @@ -190,9 +190,7 @@
     5.4    {
     5.5      val master_dir = buffer.getDirectory
     5.6      val path = buffer.getSymlinkPath
     5.7 -    if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
     5.8 -      (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
     5.9 -    else (master_dir, path)
    5.10 +    (master_dir, path)
    5.11    }
    5.12  
    5.13