equal
deleted
inserted
replaced
366 " src: url('" + make_url(entry.path.file_name) + "') format('truetype');") ::: |
366 " src: url('" + make_url(entry.path.file_name) + "') format('truetype');") ::: |
367 (if (entry.is_bold) List(" font-weight: bold;") else Nil) ::: |
367 (if (entry.is_bold) List(" font-weight: bold;") else Nil) ::: |
368 (if (entry.is_italic) List(" font-style: italic;") else Nil) ::: |
368 (if (entry.is_italic) List(" font-style: italic;") else Nil) ::: |
369 List("}")) |
369 List("}")) |
370 |
370 |
371 ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face(_))) |
371 ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face)) |
372 .mkString("", "\n\n", "\n") |
372 .mkString("", "\n\n", "\n") |
373 } |
373 } |
374 |
374 |
375 |
375 |
376 /* document directory */ |
376 /* document directory */ |