discontinued special treatment of ML files -- no longer complete extensions on demand;
simplified Thy_Load.check_file, with uniform error reporting;
added Thy_Load.test_file for non-strict checking;
misc tuning and simplification;

--- a/NEWS	Thu Jul 22 20:46:45 2010 +0200
+++ b/NEWS	Thu Jul 22 22:31:20 2010 +0200
@@ -14,6 +14,11 @@
 consistent view on symbols, while raw explode (or String.explode)
 merely give a byte-oriented representation.
 
+* Special treatment of ML file names has been discontinued.
+Historically, optional extensions .ML or .sml were added on demand --
+at the cost of clarity of file dependencies.  Recall that Isabelle/ML
+files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
+
 
 *** HOL ***
 

--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Thu Jul 22 20:46:45 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Thu Jul 22 22:31:20 2010 +0200
@@ -80,7 +80,7 @@
                NONE => (NONE, NONE)
              | SOME fname =>
                let val path = Path.explode fname in
-                 case Thy_Load.check_file Path.current path of
+                 case Thy_Load.test_file Path.current path of
                    SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
                  | NONE => (NONE, SOME fname)
                end);

--- a/src/Pure/Thy/present.ML	Thu Jul 22 20:46:45 2010 +0200
+++ b/src/Pure/Thy/present.ML	Thu Jul 22 22:31:20 2010 +0200
@@ -460,18 +460,14 @@
     val parents = Theory.parents_of thy;
     val parent_specs = map (parent_link remote_path path) parents;
 
-    fun prep_file (raw_path, loadit) =
-      (case Thy_Load.check_ml dir raw_path of
-        SOME (path, _) =>
-          let
-            val base = Path.base path;
-            val base_html = html_ext base;
-            val _ = add_file (Path.append html_prefix base_html,
-              HTML.ml_file (Url.File base) (File.read path));
-            in (Url.File base_html, Url.File raw_path, loadit) end
-      | NONE => error ("Browser info: expected to find ML file " ^ quote (Path.implode raw_path)));
-
-    val files_html = map prep_file files;
+    val files_html = files |> map (fn (raw_path, loadit) =>
+      let
+        val path = #1 (Thy_Load.check_file dir raw_path);
+        val base = Path.base path;
+        val base_html = html_ext base;
+        val _ = add_file (Path.append html_prefix base_html,
+          HTML.ml_file (Url.File base) (File.read path));
+      in (Url.File base_html, Url.File raw_path, loadit) end);
 
     fun prep_html_source (tex_source, html_source, html) =
       let

--- a/src/Pure/Thy/thy_info.ML	Thu Jul 22 20:46:45 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Jul 22 22:31:20 2010 +0200
@@ -296,11 +296,7 @@
   let
     val dir = master_directory name;
     val _ = check_unfinished error name;
-  in
-    (case Thy_Load.check_file dir path of
-      SOME path_info => change_deps name (provide path name path_info)
-    | NONE => error ("Could not find file " ^ quote (Path.implode path)))
-  end;
+  in change_deps name (provide path name (Thy_Load.check_file dir path)) end;
 
 fun load_file path =
   if ! Output.timing then
@@ -417,12 +413,12 @@
 
 local
 
-fun check_ml master (src_path, info) =
+fun check_file master (src_path, info) =
   let val info' =
     (case info of
       NONE => NONE
     | SOME (_, id) =>
-        (case Thy_Load.check_ml (master_dir master) src_path of
+        (case Thy_Load.test_file (master_dir master) src_path of
           NONE => NONE
         | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
   in (src_path, info') end;
@@ -444,7 +440,7 @@
           in (false, init_deps master' text' parents' files', parents') end
         else
           let
-            val files' = map (check_ml master') files;
+            val files' = map (check_file master') files;
             val current = update_time >= 0 andalso can get_theory name
               andalso forall (is_some o snd) files';
             val update_time' = if current then update_time else ~1;

--- a/src/Pure/Thy/thy_load.ML	Thu Jul 22 20:46:45 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Jul 22 22:31:20 2010 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/Thy/thy_load.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Theory loader primitives, including load path.
+Loading files that contribute to a theory, including global load path
+management.
 *)
 
 signature BASIC_THY_LOAD =
@@ -16,13 +17,12 @@
 signature THY_LOAD =
 sig
   include BASIC_THY_LOAD
-  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 consistent_name: string -> string -> unit
-  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 test_file: Path.T -> Path.T -> (Path.T * File.ident) option
+  val check_file: Path.T -> Path.T -> Path.T * File.ident
   val check_thy: Path.T -> string -> Path.T * File.ident
   val deps_thy: Path.T -> string ->
    {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
@@ -58,7 +58,6 @@
 
 (* file formats *)
 
-val ml_exts = ["ML", "sml"];
 val ml_path = Path.ext "ML" o Path.basic;
 val thy_path = Path.ext "thy" o Path.basic;
 
@@ -75,30 +74,38 @@
 
 (* check files *)
 
-fun check_ext exts paths src_path =
+local
+
+exception NOT_FOUND of Path.T list * Path.T;
+
+fun try_file dir src_path =
   let
+    val prfxs = search_path dir src_path;
     val path = Path.expand src_path;
     val _ = Path.is_current path andalso error "Bad file specification";
+    val result =
+      prfxs |> get_first (fn prfx =>
+        let val full_path = File.full_path (Path.append prfx path)
+        in Option.map (pair full_path) (File.ident full_path) end);
+  in
+    (case result of
+      SOME res => res
+    | NONE => raise NOT_FOUND (prfxs, path))
+  end;
 
-    fun try_ext rel_path ext =
-      let val ext_path = Path.expand (Path.ext ext rel_path)
-      in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
-    fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
-  in get_first try_prfx paths end;
-
-fun check_file dir path = check_ext [] (search_path dir path) path;
-fun check_ml dir path = check_ext ml_exts (search_path dir path) path;
+in
 
-fun check_thy dir name =
-  let
-    val thy_file = thy_path name;
-    val paths = search_path dir thy_file;
-  in
-    (case check_ext [] paths thy_file of
-      NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
-        " in " ^ commas_quote (map Path.implode paths))
-    | SOME thy_id => thy_id)
-  end;
+fun test_file dir file =
+  SOME (try_file dir file) handle NOT_FOUND _ => NONE;
+
+fun check_file dir file =
+  try_file dir file handle NOT_FOUND (prfxs, path) =>
+    error ("Could not find file " ^ quote (Path.implode path) ^
+      " in " ^ commas_quote (map Path.implode prfxs));
+
+fun check_thy dir name = check_file dir (thy_path name);
+
+end;
 
 
 (* theory deps *)
@@ -114,12 +121,13 @@
   in {master = master, text = text, imports = imports, uses = uses} end;
 
 
-(* load files *)
+(* ML files *)
 
 fun load_ml dir raw_path =
-  (case check_ml dir raw_path of
-    NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
-  | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
+  let
+    val (path, id) = check_file dir raw_path;
+    val _ = ML_Context.eval_file path;
+  in (path, id) end;
 
 end;