# HG changeset patch
# User wenzelm
# Date 1496351568 -7200
# Node ID 58aa6749ff36ef1a16f2889414750fbf5f8b4197
# Parent  ee4cf96a9406983d4be2961ef4aecc95f3681ac6
generate CSS for Isabelle fonts;

diff -r ee4cf96a9406 -r 58aa6749ff36 etc/isabelle.css
--- a/etc/isabelle.css	Thu Jun 01 21:43:36 2017 +0200
+++ b/etc/isabelle.css	Thu Jun 01 23:12:48 2017 +0200
@@ -1,22 +1,3 @@
-/* style file for Isabelle XHTML/XML output */
-
-@font-face {
-  font-family: 'IsabelleText';
-  src: url('fonts/IsabelleText.ttf') format('truetype');
-}
-
-@font-face {
-  font-family: 'IsabelleText';
-  src: url('fonts/IsabelleTextBold.ttf') format('truetype');
-  font-weight: bold;
-}
-
-@font-face {
-  font-family: 'Vacuous';
-  src: url('fonts/Vacuous.ttf') format('truetype');
-}
-
-
 /* standard document markup */
 
 dt {
diff -r ee4cf96a9406 -r 58aa6749ff36 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Thu Jun 01 21:43:36 2017 +0200
+++ b/src/Pure/Thy/html.scala	Thu Jun 01 23:12:48 2017 +0200
@@ -174,6 +174,9 @@
 
   def style(s: String): XML.Elem = XML.elem("style", text(s))
 
+  def style_file(href: String): XML.Elem =
+    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
+
 
   /* messages */
 
@@ -208,29 +211,60 @@
     XML.Elem(Markup("meta",
       List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
 
-  def head_css(css: String): XML.Elem =
-    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil)
-
   def output_document(head: XML.Body, body: XML.Body,
     css: String = "isabelle.css", hidden: Boolean = true): String =
   {
     cat_lines(
       List(header,
         output(
-          XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head),
+          XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head),
           hidden = hidden),
         output(XML.elem("body", body), hidden = hidden)))
   }
 
 
+  /* fonts */
+
+  def fonts_url(): String => String =
+    (for (font <- Isabelle_System.fonts(html = true))
+     yield (font.base_name -> Url.print_file(font.file))).toMap
+
+  def fonts_dir(prefix: String)(ttf_name: String): String =
+    prefix + "/" + ttf_name
+
+  def fonts_css(make_url: String => String = fonts_url()): String =
+  {
+    def font_face(name: String, ttf_name: String, bold: Boolean = false): String =
+      cat_lines(
+        List(
+          "@font-face {",
+          "  font-family: '" + name + "';",
+          "  src: url('" + make_url(ttf_name) + "') format('truetype');") :::
+        (if (bold) List("  font-weight: bold;") else Nil) :::
+        List("}"))
+
+    List(
+      "/* Isabelle fonts */",
+      font_face("IsabelleText", "IsabelleText.ttf"),
+      font_face("IsabelleText", "IsabelleTextBold.ttf", bold = true),
+      font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n")
+  }
+
+
   /* document directory */
 
   def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
 
+  def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts"))
+  {
+    File.write(dir + isabelle_css.base,
+      fonts_css(make_url) + "\n\n\n" + File.read(isabelle_css))
+  }
+
   def init_dir(dir: Path)
   {
     Isabelle_System.mkdirs(dir)
-    File.copy(isabelle_css, dir)
+    write_isabelle_css(dir)
   }
 
   def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
diff -r ee4cf96a9406 -r 58aa6749ff36 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Jun 01 21:43:36 2017 +0200
+++ b/src/Pure/Thy/present.scala	Thu Jun 01 23:12:48 2017 +0200
@@ -93,7 +93,7 @@
       File.copy(graph_file, session_graph.file)
       Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
 
-      File.copy(HTML.isabelle_css, session_prefix)
+      HTML.write_isabelle_css(session_prefix)
 
       for (font <- Isabelle_System.fonts(html = true))
         File.copy(font, session_fonts)
diff -r ee4cf96a9406 -r 58aa6749ff36 src/Tools/VSCode/src/preview.scala
--- a/src/Tools/VSCode/src/preview.scala	Thu Jun 01 21:43:36 2017 +0200
+++ b/src/Tools/VSCode/src/preview.scala	Thu Jun 01 23:12:48 2017 +0200
@@ -45,11 +45,12 @@
   {
     val label = "Preview " + quote(model.node_name.toString)
     val content =
-      HTML.output_document(Nil,
+      HTML.output_document(
+        List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
         List(
           HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
           HTML.source(Symbol.decode(snapshot.node.commands.iterator.map(_.source).mkString))),
-        css = Url.print_file(HTML.isabelle_css.file))
+        css = "")
     (label, content)
   }
 }