# HG changeset patch
# User wenzelm
# Date 1244145714 -7200
# Node ID dde1b4d1c95b2a10910e0f8461f9fb19383278ba
# Parent  d24ef3ff34bc3c78461ea43b4a82b22c10a6f499
retrieve ML source files;

diff -r d24ef3ff34bc -r dde1b4d1c95b etc/settings
--- a/etc/settings	Thu Jun 04 19:15:57 2009 +0200
+++ b/etc/settings	Thu Jun 04 22:01:54 2009 +0200
@@ -27,7 +27,7 @@
   $POLY_HOME)
 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
 ML_OPTIONS="-H 200"
-ML_DBASE=""
+ML_SOURCES="$ML_HOME/../src"
 
 # Poly/ML 5.2.1
 #ML_PLATFORM=x86-linux
diff -r d24ef3ff34bc -r dde1b4d1c95b src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Jun 04 19:15:57 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Jun 04 22:01:54 2009 +0200
@@ -80,7 +80,25 @@
     new File(platform_path(path))
 
 
-  /* processes */
+  /* source files */
+
+  private def try_file(file: File) = if (file.isFile) Some(file) else None
+
+  def source_file(path: String): Option[File] = {
+    if (path == "ML") None
+    else if (path.startsWith("/") || path == "")
+      try_file(platform_file(path))
+    else {
+      val pure_file = platform_file("~~/src/Pure/" + path)
+      if (pure_file.isFile) Some(pure_file)
+      else if (getenv("ML_SOURCES") != "")
+        try_file(platform_file("$ML_SOURCES/" + path))
+      else None
+    }
+  }
+
+
+  /* shell processes */
 
   def execute(redirect: Boolean, args: String*): Process = {
     val cmdline = new java.util.LinkedList[String]
@@ -149,7 +167,7 @@
 
   private def read_symbols(path: String) = {
     val file = new File(platform_path(path))
-    if (file.canRead) Source.fromFile(file).getLines
+    if (file.isFile) Source.fromFile(file).getLines
     else Iterator.empty
   }
   val symbols = new Symbol.Interpretation(