# HG changeset patch
# User wenzelm
# Date 1672429109 -3600
# Node ID f2a8ba0b8c96bfdf36074ac150560505d138fae7
# Parent  a5ff9cf61551aca687f8fb2b367dd65ba36842a4
more robust: avoid detour via somewhat fragile Node.Name.path;

diff -r a5ff9cf61551 -r f2a8ba0b8c96 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 30 20:26:28 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 30 20:38:29 2022 +0100
@@ -114,6 +114,8 @@
           case _ => false
         }
 
+      def file_name: String = Url.get_base_name(node).getOrElse("")
+
       def path: Path = Path.explode(File.standard_path(node))
       def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
 
diff -r a5ff9cf61551 -r f2a8ba0b8c96 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Dec 30 20:26:28 2022 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Dec 30 20:38:29 2022 +0100
@@ -32,7 +32,7 @@
     override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
       val name = snapshot.node_name
       if (detect(name.node)) {
-        val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
+        val title = "Bibliography " + quote(snapshot.node_name.file_name)
         val content =
           Isabelle_System.with_tmp_file("bib", "bib") { bib =>
             File.write(bib, snapshot.source)
diff -r a5ff9cf61551 -r f2a8ba0b8c96 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Fri Dec 30 20:26:28 2022 +0100
+++ b/src/Pure/Thy/browser_info.scala	Fri Dec 30 20:38:29 2022 +0100
@@ -264,7 +264,7 @@
 
       val name = snapshot.node_name
       if (plain_text) {
-        val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
+        val title = "File " + Symbol.cartouche_decoded(name.file_name)
         val body = HTML.text(snapshot.source)
         html_document(title, body, fonts_css)
       }
@@ -272,7 +272,7 @@
         Resources.html_document(snapshot) getOrElse {
           val title =
             if (name.is_theory) "Theory " + quote(name.theory_base_name)
-            else "File " + Symbol.cartouche_decoded(name.path.file_name)
+            else "File " + Symbol.cartouche_decoded(name.file_name)
           val xml = snapshot.xml_markup(elements = elements.html)
           val body = Node_Context.empty.make_html(elements, xml)
           html_document(title, body, fonts_css)
diff -r a5ff9cf61551 -r f2a8ba0b8c96 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Dec 30 20:26:28 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Dec 30 20:38:29 2022 +0100
@@ -426,8 +426,10 @@
                   name <- proper_session_theories.iterator
                   name1 <- resources.find_theory_node(name.theory)
                   if name.node != name1.node
-                } yield "Incoherent theory file import:\n  " + name.path + " vs. \n  " + name1.path)
-                .toList
+                } yield {
+                  "Incoherent theory file import:\n  " + quote(name.node) +
+                    " vs. \n  " + quote(name1.node)
+                }).toList
 
               errs1 ::: errs2 ::: errs3 ::: errs4
             }