clarified signature;
clarified version of locally changed repository;

--- a/src/Pure/General/mercurial.scala	Wed Jun 01 10:10:42 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Jun 04 16:54:24 2022 +0200
@@ -121,6 +121,9 @@
     ssh.is_dir(root + Path.explode(".hg")) &&
     new Repository(root, ssh).command("root").ok
 
+  def id_repository(root: Path, ssh: SSH.System = SSH.Local, rev: String = "tip"): Option[String] =
+    if (is_repository(root, ssh = ssh)) Some(repository(root, ssh = ssh).id(rev = rev)) else None
+
   def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = {
     val hg = new Repository(root, ssh)
     hg.command("root").check

--- a/src/Pure/System/isabelle_system.scala	Wed Jun 01 10:10:42 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jun 04 16:54:24 2022 +0200
@@ -102,10 +102,10 @@
   /* Isabelle distribution identification */
 
   def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
-    getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse {
-      if (Mercurial.is_repository(root)) Mercurial.repository(root).parent()
-      else error("Failed to identify Isabelle distribution " + root.expand)
-    }
+    getetc("ISABELLE_ID", root = root) orElse
+    Mercurial.archive_id(root) orElse
+    Mercurial.id_repository(root, rev = "") getOrElse
+    error("Failed to identify Isabelle distribution " + root.expand)
 
   object Isabelle_Id extends Scala.Fun_String("isabelle_id") {
     val here = Scala_Project.here