--- a/Admin/components/components.sha1 Thu Nov 29 15:07:18 2018 +0100
+++ b/Admin/components/components.sha1 Thu Nov 29 15:17:51 2018 +0100
@@ -71,6 +71,7 @@
c17c482e411bbaf992498041a3e1dea80336aaa6 isabelle_fonts-20171230.tar.gz
3affbb306baff37c360319b21cbaa2cc96ebb282 isabelle_fonts-20180113.tar.gz
bee32019e5d7cf096ef2ea1d836c732e9a7628cc isabelle_fonts-20181124.tar.gz
+f249bc2c85bd2af9eee509de17187a766b74ab86 isabelle_fonts-20181129.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
71d19df63816e9be1c4c5eb44aea7a44cfadb319 jdk-11.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
--- a/Admin/components/main Thu Nov 29 15:07:18 2018 +0100
+++ b/Admin/components/main Thu Nov 29 15:17:51 2018 +0100
@@ -4,7 +4,7 @@
csdp-6.x
cvc4-1.5-4
e-2.0-2
-isabelle_fonts-20181124
+isabelle_fonts-20181129
jdk-11+28
jedit_build-20181026
jfreechart-1.5.0
--- a/lib/scripts/getfunctions Thu Nov 29 15:07:18 2018 +0100
+++ b/lib/scripts/getfunctions Thu Nov 29 15:17:51 2018 +0100
@@ -141,6 +141,21 @@
}
export -f isabelle_fonts
+function isabelle_fonts_hidden ()
+{
+ local X=""
+ for X in "$@"
+ do
+ if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then
+ ISABELLE_FONTS_HIDDEN="$X"
+ else
+ ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X"
+ fi
+ done
+ export ISABELLE_FONTS_HIDDEN
+}
+export -f isabelle_fonts_hidden
+
#file formats
function isabelle_file_format ()
{
--- a/src/Pure/Admin/build_fonts.scala Thu Nov 29 15:07:18 2018 +0100
+++ b/src/Pure/Admin/build_fonts.scala Thu Nov 29 15:17:51 2018 +0100
@@ -276,12 +276,7 @@
yield """ "$COMPONENT/""" + path.file_name + "\"").mkString(" \\\n") +
"""
-if [ -z "$ISABELLE_FONTS_HTML" ]
-then
- ISABELLE_FONTS_HTML="$COMPONENT/Vacuous.ttf"
-else
- ISABELLE_FONTS_HTML="$ISABELLE_FONTS_HTML:$COMPONENT/Vacuous.ttf"
-fi
+isabelle_fonts_hidden "$COMPONENT/Vacuous.ttf"
""")
--- a/src/Pure/Admin/other_isabelle.scala Thu Nov 29 15:07:18 2018 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Thu Nov 29 15:17:51 2018 +0100
@@ -62,7 +62,7 @@
val etc_preferences: Path = etc + Path.explode("preferences")
def copy_fonts(target_dir: Path): Unit =
- Isabelle_Fonts.make_entries(getenv = getenv(_), html = true).
+ Isabelle_Fonts.make_entries(getenv = getenv(_), hidden = true).
foreach(entry => File.copy(entry.path, target_dir))
--- a/src/Pure/General/http.scala Thu Nov 29 15:07:18 2018 +0100
+++ b/src/Pure/General/http.scala Thu Nov 29 15:17:51 2018 +0100
@@ -154,7 +154,8 @@
/* fonts */
- private lazy val html_fonts: List[Isabelle_Fonts.Entry] = Isabelle_Fonts.fonts(html = true)
+ private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
+ Isabelle_Fonts.fonts(hidden = true)
def fonts(root: String = "/fonts"): Handler =
get(root, arg =>
--- a/src/Pure/System/isabelle_fonts.scala Thu Nov 29 15:07:18 2018 +0100
+++ b/src/Pure/System/isabelle_fonts.scala Thu Nov 29 15:17:51 2018 +0100
@@ -34,7 +34,7 @@
}
}
- sealed case class Entry(path: Path, html: Boolean = false)
+ sealed case class Entry(path: Path, hidden: Boolean = false)
{
lazy val bytes: Bytes = Bytes.read(path)
lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file)
@@ -56,17 +56,17 @@
def make_entries(
getenv: String => String = Isabelle_System.getenv_strict(_),
- html: Boolean = false): List[Entry] =
+ hidden: Boolean = false): List[Entry] =
{
Path.split(getenv("ISABELLE_FONTS")).map(Entry(_)) :::
- (if (html) Path.split(getenv("ISABELLE_FONTS_HTML")).map(Entry(_, html = true)) else Nil)
+ (if (hidden) Path.split(getenv("ISABELLE_FONTS_HIDDEN")).map(Entry(_, hidden = true)) else Nil)
}
private lazy val all_fonts: List[Entry] =
- make_entries(html = true).sorted(Entry.Ordering)
+ make_entries(hidden = true).sorted(Entry.Ordering)
- def fonts(html: Boolean = false): List[Entry] =
- if (html) all_fonts else all_fonts.filter(entry => !entry.html)
+ def fonts(hidden: Boolean = false): List[Entry] =
+ if (hidden) all_fonts else all_fonts.filter(entry => !entry.hidden)
/* system init */
--- a/src/Pure/Thy/html.scala Thu Nov 29 15:07:18 2018 +0100
+++ b/src/Pure/Thy/html.scala Thu Nov 29 15:17:51 2018 +0100
@@ -350,7 +350,7 @@
/* fonts */
def fonts_url(): String => String =
- (for (entry <- Isabelle_Fonts.fonts(html = true))
+ (for (entry <- Isabelle_Fonts.fonts(hidden = true))
yield (entry.name -> Url.print_file(entry.path.file))).toMap
def fonts_dir(prefix: String)(ttf_name: String): String =
@@ -368,7 +368,7 @@
(if (entry.is_italic) List(" font-style: italic;") else Nil) :::
List("}"))
- ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(html = true).map(font_face(_)))
+ ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face(_)))
.mkString("", "\n\n", "\n")
}
--- a/src/Pure/Thy/present.scala Thu Nov 29 15:07:18 2018 +0100
+++ b/src/Pure/Thy/present.scala Thu Nov 29 15:17:51 2018 +0100
@@ -96,7 +96,7 @@
HTML.write_isabelle_css(session_prefix)
- for (entry <- Isabelle_Fonts.fonts(html = true))
+ for (entry <- Isabelle_Fonts.fonts(hidden = true))
File.copy(entry.path, session_fonts)
}
}