--- 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))
--- 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)
--- 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)
--- 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
}