equal
deleted
inserted
replaced
24 |
24 |
25 private val environment: Map[String, String] = |
25 private val environment: Map[String, String] = |
26 { |
26 { |
27 import scala.collection.JavaConversions._ |
27 import scala.collection.JavaConversions._ |
28 |
28 |
29 val env0 = Map(java.lang.System.getenv.toList: _*) |
29 val env0 = Map(java.lang.System.getenv.toList: _*) + |
|
30 ("THIS_JAVA" -> this_java()) |
30 |
31 |
31 val isabelle_home = |
32 val isabelle_home = |
32 env0.get("ISABELLE_HOME") match { |
33 env0.get("ISABELLE_HOME") match { |
33 case None | Some("") => |
34 case None | Some("") => |
34 val path = java.lang.System.getProperty("isabelle.home") |
35 val path = java.lang.System.getProperty("isabelle.home") |