# HG changeset patch
# User wenzelm
# Date 1513947080 -3600
# Node ID c7f859868b7cbff3f5af51778cd227040c085c98
# Parent  573077aa2826d9e1e2a213488aec1543e8889e40
proper HTML title;

diff -r 573077aa2826 -r c7f859868b7c src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 11:39:49 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 13:51:20 2017 +0100
@@ -331,16 +331,15 @@
 
     if (is_bibtex) Bibtex.present(snapshot)
     else {
+      val (heading, body) =
+        if (is_theory)
+          ("Theory " + quote(node_name.theory_base_name), Present.theory_document(snapshot))
+        else ("File " + quote(node_name.path.base_name), Present.text_document(snapshot))
+
       HTML.output_document(
-        List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))),
-          css = "",
-          body =
-            if (is_theory)
-              List(HTML.chapter("Theory " + quote(node_name.theory_base_name)),
-                HTML.source(Present.theory_document(snapshot)))
-            else
-              List(HTML.chapter("File " + quote(node_name.node)),
-                HTML.source(Present.text_document(snapshot))))
+        List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css)),
+          HTML.title(heading)),
+          List(HTML.chapter(heading), HTML.source(body)))
     }
   }