proper HTML title;
authorwenzelm
Fri, 22 Dec 2017 13:51:20 +0100
changeset 67252 c7f859868b7c
parent 67251 573077aa2826
child 67253 93b4333f33bb
proper HTML title;
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)))
     }
   }