tuned signature -- more explicit types;

--- a/src/Pure/Admin/build_history.scala	Wed Mar 31 21:44:29 2021 +0200
+++ b/src/Pure/Admin/build_history.scala	Wed Mar 31 22:10:56 2021 +0200
@@ -91,7 +91,7 @@
 
   /** build_history **/
 
-  private val default_user_home = Path.explode("$USER_HOME")
+  private val default_user_home = Path.USER_HOME
   private val default_rev = "tip"
   private val default_multicore = (1, 1)
   private val default_heap = 1500
@@ -125,8 +125,8 @@
   {
     /* sanity checks */
 
-    if (File.eq(Path.explode("~~"), root))
-      error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
+    if (File.eq(Path.ISABELLE_HOME, root))
+      error("Repository coincides with ISABELLE_HOME=" + Path.ISABELLE_HOME.expand)
 
     for ((threads, _) <- multicore_list if threads < 1)
       error("Bad threads value < 1: " + threads)
@@ -556,7 +556,7 @@
         strict = strict).check
 
     if (self_update) {
-      val hg = Mercurial.repository(Path.explode("~~"))
+      val hg = Mercurial.repository(Path.ISABELLE_HOME)
       hg.push(self_hg.root_url, force = true)
       self_hg.update(rev = hg.parent(), clean = true)
 

--- a/src/Pure/Admin/build_release.scala	Wed Mar 31 21:44:29 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Mar 31 22:10:56 2021 +0200
@@ -388,7 +388,7 @@
     build_library: Boolean = false,
     parallel_jobs: Int = 1): Release =
   {
-    val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
+    val hg = Mercurial.repository(Path.ISABELLE_HOME)
 
     val release =
     {

--- a/src/Pure/Admin/other_isabelle.scala	Wed Mar 31 21:44:29 2021 +0200
+++ b/src/Pure/Admin/other_isabelle.scala	Wed Mar 31 22:10:56 2021 +0200
@@ -11,7 +11,7 @@
 {
   def apply(isabelle_home: Path,
       isabelle_identifier: String = "",
-      user_home: Path = Path.explode("$USER_HOME"),
+      user_home: Path = Path.USER_HOME,
       progress: Progress = new Progress): Other_Isabelle =
     new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
 }

--- a/src/Pure/General/path.scala	Wed Mar 31 21:44:29 2021 +0200
+++ b/src/Pure/General/path.scala	Wed Mar 31 22:10:56 2021 +0200
@@ -87,6 +87,9 @@
   def variable(s: String): Path = new Path(List(variable_elem(s)))
   val parent: Path = new Path(List(Parent))
 
+  val USER_HOME: Path = variable("USER_HOME")
+  val ISABELLE_HOME: Path = variable("ISABELLE_HOME")
+
 
   /* explode */
 

--- a/src/Pure/ML/ml_statistics.scala	Wed Mar 31 21:44:29 2021 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed Mar 31 22:10:56 2021 +0200
@@ -73,7 +73,7 @@
     Bash.process(env_prefix + "exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
         Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
           ML_Syntax.print_double(delay.seconds)),
-        cwd = Path.explode("~~").file)
+        cwd = Path.ISABELLE_HOME.file)
       .result(progress_stdout = progress_stdout, strict = false).check
   }
 

--- a/src/Pure/System/isabelle_system.scala	Wed Mar 31 21:44:29 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Mar 31 22:10:56 2021 +0200
@@ -173,7 +173,7 @@
 
   /* getetc -- static distribution parameters */
 
-  def getetc(name: String, root: Path = Path.explode("~~")): Option[String] =
+  def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] =
   {
     val path = root + Path.basic("etc") + Path.basic(name)
     if (path.is_file) {
@@ -189,13 +189,13 @@
 
   /* Isabelle distribution identification */
 
-  def isabelle_id(root: Path = Path.explode("~~")): Option[String] =
+  def isabelle_id(root: Path = Path.ISABELLE_HOME): Option[String] =
     getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) orElse {
       if (Mercurial.is_repository(root)) Some(Mercurial.repository(root).parent())
       else None
     }
 
-  def isabelle_tags(root: Path = Path.explode("~~")): String =
+  def isabelle_tags(root: Path = Path.ISABELLE_HOME): String =
     getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse {
       if (Mercurial.is_repository(root)) {
         val hg = Mercurial.repository(root)

--- a/src/Pure/Tools/build.scala	Wed Mar 31 21:44:29 2021 +0200
+++ b/src/Pure/Tools/build.scala	Wed Mar 31 22:10:56 2021 +0200
@@ -625,7 +625,7 @@
             sessions = sessions),
           presentation = presentation,
           progress = progress,
-          check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
+          check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
           build_heap = build_heap,
           clean_build = clean_build,
           dirs = dirs,

--- a/src/Pure/Tools/scala_project.scala	Wed Mar 31 21:44:29 2021 +0200
+++ b/src/Pure/Tools/scala_project.scala	Wed Mar 31 22:10:56 2021 +0200
@@ -27,7 +27,7 @@
   {
     val files1 =
     {
-      val isabelle_home = Path.explode("~~").canonical
+      val isabelle_home = Path.ISABELLE_HOME.canonical
       Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH")).
         map(path => File.relative_path(isabelle_home, path).getOrElse(path).implode)
     }
@@ -126,7 +126,7 @@
       val (path, target) =
         isabelle_dirs.collectFirst({
           case (prfx, p) if file.startsWith(prfx) =>
-            (Path.explode("~~") + Path.explode(file), scala_src_dir + p)
+            (Path.ISABELLE_HOME + Path.explode(file), scala_src_dir + p)
         }).getOrElse(error("Unknown directory prefix for " + quote(file)))
 
       Isabelle_System.make_directory(target)