# HG changeset patch
# User wenzelm
# Date 1750066554 -7200
# Node ID b49f65765c580bdc0519977bf7814356c290fbc1
# Parent  eb26ddc6b0639a1e6b76df203e13defaa6ff74f7
tuned errors;

diff -r eb26ddc6b063 -r b49f65765c58 src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Mon Jun 16 11:00:04 2025 +0200
+++ b/src/Pure/System/other_isabelle.scala	Mon Jun 16 11:35:54 2025 +0200
@@ -20,7 +20,9 @@
         case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix)
         case _ =>
           if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
-            error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT")
+            error(
+              "Cannot manage other Isabelle distribution: ISABELLE_SETTINGS_PRESENT " +
+                "-- consider using SSH")
           }
           (root.canonical, "")
       }
@@ -39,6 +41,7 @@
   other_isabelle =>
 
   override def toString: String = isabelle_home_url
+  def error_context: String = "\nThe error(s) above occurred for other Isabelle " + toString
 
 
   /* static system */
@@ -72,8 +75,7 @@
 
   def getenv_strict(name: String): String =
     proper_string(getenv(name)) getOrElse
-      error("Undefined Isabelle environment variable: " + quote(name) +
-        "\nISABELLE_HOME=" + isabelle_home)
+      error("Undefined Isabelle environment variable: " + quote(name) + error_context)
 
   val settings: Isabelle_System.Settings = (name: String) => getenv(name)
 
@@ -97,7 +99,7 @@
         getenv("POLYML_HOME") match {
           case "" =>
             try { expand_path(Path.variable("ML_HOME")).dir }
-            catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
+            catch { case ERROR(msg) => error("Bad ML_HOME: " + msg + error_context) }
           case s => Path.explode(s)
         }
 
@@ -112,7 +114,7 @@
             case Pattern(a) if result.ok => a
             case _ =>
               error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
-                if_proper(result.err, "\n" + result.err))
+                if_proper(result.err, "\n" + result.err) + error_context)
           }
         }
         else getenv("ML_PLATFORM")
@@ -174,7 +176,10 @@
         "export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" +
         "bin/isabelle jedit -b", echo = echo).check
     }
-    catch { case ERROR(msg) => cat_error("Failed to build Isabelle/Scala/Java modules:", msg) }
+    catch {
+      case ERROR(msg) =>
+        error("Failed to build Isabelle/Scala/Java modules:\n" + msg + error_context)
+    }
   }
 
 
@@ -196,7 +201,7 @@
         "#-*- shell-script -*- :mode=shellscript:\n" +
         settings.mkString("\n", "\n", "\n"))
     }
-    else error("Cannot proceed with existing user settings file: " + etc_settings)
+    else error("Cannot proceed with existing user settings file: " + etc_settings + error_context)
   }
 
   def debug_settings(): List[String] = {