equal
deleted
inserted
replaced
98 |
98 |
99 |
99 |
100 |
100 |
101 /** compiler **/ |
101 /** compiler **/ |
102 |
102 |
103 def get_classpath(): List[String] = |
103 def get_classpath(): List[Path] = |
104 space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", "")) |
104 for { |
105 .filter(_.nonEmpty) |
105 s <- space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", "")) |
|
106 if s.nonEmpty |
|
107 } yield Path.explode(File.standard_path(s)) |
106 |
108 |
107 object Compiler { |
109 object Compiler { |
108 object Message { |
110 object Message { |
109 object Kind extends Enumeration { |
111 object Kind extends Enumeration { |
110 val error, warning, info, other = Value |
112 val error, warning, info, other = Value |