# HG changeset patch
# User wenzelm
# Date 1343238580 -7200
# Node ID f26b6b364c2c801805e78ab4bdacfa2d631683bb
# Parent  fd03877ad5bcce3f2ac5254a0cefb3b683c9e206
tuned;

diff -r fd03877ad5bc -r f26b6b364c2c src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Jul 25 18:05:07 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Jul 25 19:49:40 2012 +0200
@@ -292,19 +292,18 @@
 
   /* find logics */
 
-  def find_logics(): List[String] =
+  def find_logics_dirs(): List[Path] =
   {
-    val ml_ident = getenv_strict("ML_IDENTIFIER")
-    val logics = new mutable.ListBuffer[String]
-    for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
-      val files = (dir + Path.explode(ml_ident)).file.listFiles()
-      if (files != null) {
-        for (file <- files if file.isFile) logics += file.getName
-      }
-    }
-    logics.toList.sorted
+    val ml_ident = Path.explode("$ML_IDENTIFIER").expand
+    Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
   }
 
+  def find_logics(): List[String] =
+    (for {
+      dir <- find_logics_dirs()
+      files = dir.file.listFiles() if files != null
+      file <- files.toList if file.isFile } yield file.getName).sorted
+
 
   /* fonts */