# HG changeset patch
# User wenzelm
# Date 1262013859 -3600
# Node ID d58da36d1a30731d06d14a15fb49f08eb2c32cf7
# Parent  001321ca185c08942ef0ff6bad7555c79e55a7c1
isabelle_tool: apply platform_path only once;
tuned;

diff -r 001321ca185c -r d58da36d1a30 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Dec 28 14:51:03 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Dec 28 16:24:19 2009 +0100
@@ -267,7 +267,7 @@
     }) match {
       case Some(dir) =>
         Isabelle_System.process_output(
-          execute(true, (List(platform_path(dir + "/" + name)) ++ args): _*))
+          execute(true, (List(expand_path(dir + "/" + name)) ++ args): _*))
       case None => ("Unknown Isabelle tool: " + name, 2)
     }
   }
@@ -332,7 +332,7 @@
 
   private def read_symbols(path: String): List[String] =
   {
-    val file = new File(platform_path(path))
+    val file = platform_file(path)
     if (file.isFile) Source.fromFile(file).getLines.toList
     else Nil
   }