# HG changeset patch
# User clasohm
# Date 760184122 -3600
# Node ID ec0b34154a6e8dd5d0cfe627e79e9e01efa59d12
# Parent  0d0a6a17a02f6ca1f33375bf7626dcfe44f027bf
made error message "file not found" more informative

diff -r 0d0a6a17a02f -r ec0b34154a6e src/Pure/Thy/read.ML
--- a/src/Pure/Thy/read.ML	Wed Jan 26 22:07:06 1994 +0100
+++ b/src/Pure/Thy/read.ML	Wed Feb 02 11:15:22 1994 +0100
@@ -144,9 +144,13 @@
             val ml_file = if thy_file = "" then make_absolute found
                           else if file_exists (tack_on thy_path (thyl ^ ".ML"))
                           then tack_on thy_path (thyl ^ ".ML")
-                          else ""
+                          else "";
+            val searched_dirs = if path = "" then (!loadpath) else [path]
         in if thy_file = "" andalso ml_file = "" then
-             error ("Could find no .thy or .ML file for theory " ^ name)
+             error ("Could not find file \"" ^ (to_lower name) ^ ".thy\" or \""
+                    ^ (to_lower name) ^ ".ML\" for theory \"" ^ name ^ "\"\n"
+                    ^ "in the following directories: \"" ^
+                    (space_implode "\", \"" searched_dirs) ^ "\"")
            else ();
            (thy_file, ml_file) 
         end;