equal
deleted
inserted
replaced
78 |
78 |
79 |
79 |
80 /** compiler **/ |
80 /** compiler **/ |
81 |
81 |
82 def class_path(): List[String] = |
82 def class_path(): List[String] = |
83 Library.distinct( |
83 for { |
84 for { |
84 prop <- List("isabelle.scala.classpath", "java.class.path") |
85 prop <- List("isabelle.scala.classpath", "java.class.path") |
85 elems = System.getProperty(prop, "") if elems.nonEmpty |
86 elems = System.getProperty(prop, "") if elems.nonEmpty |
86 elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty |
87 elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty |
87 } yield elem |
88 } yield elem) |
|
89 |
88 |
90 object Compiler |
89 object Compiler |
91 { |
90 { |
92 def context( |
91 def context( |
93 error: String => Unit = Exn.error, |
92 error: String => Unit = Exn.error, |