src/Pure/Thy/html.scala
changeset 69343 395c4fb15ea2
parent 67337 4254cfd15b00
child 69355 cdc2de88d657
equal deleted inserted replaced
69342:fa981730b964 69343:395c4fb15ea2
   356   def fonts_dir(prefix: String)(ttf_name: String): String =
   356   def fonts_dir(prefix: String)(ttf_name: String): String =
   357     prefix + "/" + ttf_name
   357     prefix + "/" + ttf_name
   358 
   358 
   359   def fonts_css(make_url: String => String = fonts_url()): String =
   359   def fonts_css(make_url: String => String = fonts_url()): String =
   360   {
   360   {
   361     def font_face(name: String, ttf_name: String, bold: Boolean = false): String =
   361     def font_face(
       
   362         name: String, ttf_name: String, bold: Boolean = false, italic: Boolean = false): String =
   362       cat_lines(
   363       cat_lines(
   363         List(
   364         List(
   364           "@font-face {",
   365           "@font-face {",
   365           "  font-family: '" + name + "';",
   366           "  font-family: '" + name + "';",
   366           "  src: url('" + make_url(ttf_name) + "') format('truetype');") :::
   367           "  src: url('" + make_url(ttf_name) + "') format('truetype');") :::
   367         (if (bold) List("  font-weight: bold;") else Nil) :::
   368         (if (bold) List("  font-weight: bold;") else Nil) :::
       
   369         (if (italic) List("  font-style: italic;") else Nil) :::
   368         List("}"))
   370         List("}"))
   369 
   371 
   370     List(
   372     List(
   371       "/* Isabelle fonts */",
   373       "/* Isabelle fonts */",
   372       font_face("IsabelleText", "IsabelleText.ttf"),
   374       font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono.ttf"),
   373       font_face("IsabelleText", "IsabelleTextBold.ttf", bold = true),
   375       font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Bold.ttf", bold = true),
       
   376       font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Oblique.ttf", italic = true),
       
   377       font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-BoldOblique.ttf", bold = true, italic = true),
       
   378       font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans.ttf"),
       
   379       font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Bold.ttf", bold = true),
       
   380       font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Oblique.ttf", italic = true),
       
   381       font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-BoldOblique.ttf", bold = true, italic = true),
       
   382       font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif.ttf"),
       
   383       font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Bold.ttf", bold = true),
       
   384       font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Oblique.ttf", italic = true),
       
   385       font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-BoldOblique.ttf", bold = true, italic = true),
   374       font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n")
   386       font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n")
   375   }
   387   }
   376 
   388 
   377 
   389 
   378   /* document directory */
   390   /* document directory */