equal
deleted
inserted
replaced
44 def find_jars(start: String): List[String] = |
44 def find_jars(start: String): List[String] = |
45 if (start != null) |
45 if (start != null) |
46 find_files(new JFile(start), |
46 find_files(new JFile(start), |
47 entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath) |
47 entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath) |
48 else Nil |
48 else Nil |
49 val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome) |
49 val path = |
|
50 Main.class_path.map(Isabelle_System.platform_file(_)) ::: |
|
51 find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome) |
50 path.mkString(JFile.pathSeparator) |
52 path.mkString(JFile.pathSeparator) |
51 } |
53 } |
52 |
54 |
53 |
55 |
54 /* global state -- owned by Swing thread */ |
56 /* global state -- owned by Swing thread */ |