equal
deleted
inserted
replaced
109 /* Isabelle distribution identification */ |
109 /* Isabelle distribution identification */ |
110 |
110 |
111 def isabelle_id(root: Path = Path.ISABELLE_HOME): String = |
111 def isabelle_id(root: Path = Path.ISABELLE_HOME): String = |
112 getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse { |
112 getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse { |
113 if (Mercurial.is_repository(root)) Mercurial.repository(root).parent() |
113 if (Mercurial.is_repository(root)) Mercurial.repository(root).parent() |
114 else error("Failed to identify Isabelle distribution " + root) |
114 else error("Failed to identify Isabelle distribution " + root.expand) |
115 } |
115 } |
116 |
116 |
117 object Isabelle_Id extends Scala.Fun_String("isabelle_id") |
117 object Isabelle_Id extends Scala.Fun_String("isabelle_id") |
118 { |
118 { |
119 val here = Scala_Project.here |
119 val here = Scala_Project.here |