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 |
|
50 val initial_class_path = |
|
51 System.getProperty("java.class.path") match { |
|
52 case null => Nil |
|
53 case class_path => Library.space_explode(JFile.pathSeparatorChar, class_path) |
|
54 } |
|
55 |
49 val path = |
56 val path = |
50 Main.class_path.map(Isabelle_System.platform_file(_)) ::: |
57 initial_class_path ::: |
51 find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome) |
58 find_jars(jEdit.getSettingsDirectory) ::: |
|
59 find_jars(jEdit.getJEditHome) |
52 path.mkString(JFile.pathSeparator) |
60 path.mkString(JFile.pathSeparator) |
53 } |
61 } |
54 |
62 |
55 |
63 |
56 /* global state -- owned by Swing thread */ |
64 /* global state -- owned by Swing thread */ |