1.1 --- a/etc/settings	Thu Jun 04 19:15:57 2009 +0200
     1.2 +++ b/etc/settings	Thu Jun 04 22:01:54 2009 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    $POLY_HOME)
     1.5  ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
     1.6  ML_OPTIONS="-H 200"
     1.7 -ML_DBASE=""
     1.8 +ML_SOURCES="$ML_HOME/../src"
     1.9  
    1.10  # Poly/ML 5.2.1
    1.11  #ML_PLATFORM=x86-linux

     2.1 --- a/src/Pure/System/isabelle_system.scala	Thu Jun 04 19:15:57 2009 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Jun 04 22:01:54 2009 +0200
     2.3 @@ -80,7 +80,25 @@
     2.4      new File(platform_path(path))
     2.5  
     2.6  
     2.7 -  /* processes */
     2.8 +  /* source files */
     2.9 +
    2.10 +  private def try_file(file: File) = if (file.isFile) Some(file) else None
    2.11 +
    2.12 +  def source_file(path: String): Option[File] = {
    2.13 +    if (path == "ML") None
    2.14 +    else if (path.startsWith("/") || path == "")
    2.15 +      try_file(platform_file(path))
    2.16 +    else {
    2.17 +      val pure_file = platform_file("~~/src/Pure/" + path)
    2.18 +      if (pure_file.isFile) Some(pure_file)
    2.19 +      else if (getenv("ML_SOURCES") != "")
    2.20 +        try_file(platform_file("$ML_SOURCES/" + path))
    2.21 +      else None
    2.22 +    }
    2.23 +  }
    2.24 +
    2.25 +
    2.26 +  /* shell processes */
    2.27  
    2.28    def execute(redirect: Boolean, args: String*): Process = {
    2.29      val cmdline = new java.util.LinkedList[String]
    2.30 @@ -149,7 +167,7 @@
    2.31  
    2.32    private def read_symbols(path: String) = {
    2.33      val file = new File(platform_path(path))
    2.34 -    if (file.canRead) Source.fromFile(file).getLines
    2.35 +    if (file.isFile) Source.fromFile(file).getLines
    2.36      else Iterator.empty
    2.37    }
    2.38    val symbols = new Symbol.Interpretation(