# HG changeset patch
# User wenzelm
# Date 1231540476 -3600
# Node ID d584715a3ebb2eb0a423822e5af9a437dd72dd8c
# Parent  779ff118732788d271bcdf04880c058522b8b726
added split_thy_path;

diff -r 779ff1187327 -r d584715a3ebb src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Jan 09 23:33:59 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Jan 09 23:34:36 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/thy_load.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Theory loader primitives, including load path.
@@ -22,6 +21,7 @@
   val ml_exts: string list
   val ml_path: string -> Path.T
   val thy_path: string -> Path.T
+  val split_thy_path: Path.T -> Path.T * string
   val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_thy: Path.T -> string -> Path.T * File.ident
@@ -62,6 +62,11 @@
 val ml_path = Path.ext "ML" o Path.basic;
 val thy_path = Path.ext "thy" o Path.basic;
 
+fun split_thy_path path =
+  (case Path.split_ext path of
+    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
+  | _ => error ("Bad theory file specification " ^ Path.implode path));
+
 
 (* check files *)