# HG changeset patch
# User wenzelm
# Date 1673024329 -3600
# Node ID 099486b09c0ee5f6b79809714ce3a209029cee79
# Parent  ee785742c6943f2bca58621ec379757c6657b7c1
prefer relative src_path (if possible) -- in contrast to 9ce0aa145d21:

diff -r ee785742c694 -r 099486b09c0e src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Fri Jan 06 17:20:53 2023 +0100
+++ b/src/Pure/Thy/browser_info.scala	Fri Jan 06 17:58:49 2023 +0100
@@ -614,6 +614,8 @@
           node_context(theory.thy_file, session_dir).
             make_html(thy_elements, snapshot.xml_markup(elements = thy_elements.html)))
 
+      val master_dir = Path.explode(snapshot.node_name.master_dir)
+
       val files =
         for {
           blob_name <- snapshot.node_files.tail
@@ -623,15 +625,18 @@
         yield {
           progress.expose_interrupt()
 
-          val file_name = blob_name.node
-          if (verbose) progress.echo("Presenting file " + quote(file_name))
+          val file = blob_name.node
+          if (verbose) progress.echo("Presenting file " + quote(file))
 
-          val file_html = session_dir + context.file_html(file_name)
+          val file_html = session_dir + context.file_html(file)
           val file_dir = file_html.dir
           val html_link = HTML.relative_href(file_html, base = Some(session_dir))
-          val html = context.source(node_context(file_name, file_dir).make_html(thy_elements, xml))
+          val html = context.source(node_context(file, file_dir).make_html(thy_elements, xml))
 
-          val file_title = "File " + Symbol.cartouche_decoded(file_name)
+          val path = Path.explode(file)
+          val src_path = File.relative_path(master_dir, path).getOrElse(path)
+
+          val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
           HTML.write_document(file_dir, file_html.file_name,
             List(HTML.title(file_title)), List(context.head(file_title), html),
             root = Some(context.root_dir))