# HG changeset patch
# User wenzelm
# Date 1739366912 -3600
# Node ID 3f7c8e6d348109eb0c5d4cf1103b01228d2ce846
# Parent  143ff9527bac9c858502cb5e3fdbac90fa34d539
tuned signature: more explicit operations;

diff -r 143ff9527bac -r 3f7c8e6d3481 src/Pure/Build/browser_info.scala
--- a/src/Pure/Build/browser_info.scala	Wed Feb 12 14:26:43 2025 +0100
+++ b/src/Pure/Build/browser_info.scala	Wed Feb 12 14:28:32 2025 +0100
@@ -638,7 +638,7 @@
           val html = context.source(node_context(file, file_dir).make_html(thy_elements, xml))
 
           val path = Path.explode(file)
-          val src_path = File.relative_path(master_dir, path).getOrElse(path)
+          val src_path = File.perhaps_relative_path(master_dir, path)
 
           val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
           HTML.write_document(file_dir, file_html.file_name,
diff -r 143ff9527bac -r 3f7c8e6d3481 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Wed Feb 12 14:26:43 2025 +0100
+++ b/src/Pure/Build/build.scala	Wed Feb 12 14:28:32 2025 +0100
@@ -728,7 +728,7 @@
       val blobs =
         blobs_files.map { name =>
           val path = Path.explode(name)
-          val src_path = File.relative_path(master_dir, path).getOrElse(path)
+          val src_path = File.perhaps_relative_path(master_dir, path)
 
           val file = read_source_file(name)
           val bytes = file.bytes
diff -r 143ff9527bac -r 3f7c8e6d3481 src/Pure/Build/sessions.scala
--- a/src/Pure/Build/sessions.scala	Wed Feb 12 14:26:43 2025 +0100
+++ b/src/Pure/Build/sessions.scala	Wed Feb 12 14:28:32 2025 +0100
@@ -418,7 +418,7 @@
                     name <- proper_session_theories.iterator
                     path = Path.explode(name.master_dir)
                     if !ok(path.canonical_file)
-                    path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
+                    path1 = File.perhaps_relative_path(info.dir.canonical, path)
                   } yield (path1, name)).toList
                 val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
 
diff -r 143ff9527bac -r 3f7c8e6d3481 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Wed Feb 12 14:26:43 2025 +0100
+++ b/src/Pure/General/file.scala	Wed Feb 12 14:28:32 2025 +0100
@@ -123,6 +123,9 @@
     else None
   }
 
+  def perhaps_relative_path(base: Path, other: Path): Path =
+    relative_path(base, other).getOrElse(other)
+
 
   /* bash path */