# HG changeset patch
# User wenzelm
# Date 1543501071 -3600
# Node ID ab66951166f34c08ea79be35f52f92f295cb62e1
# Parent  2c0af1c2e7235f706f4c057079f8c331205c0538
clarified "hidden" terminology;
updated component;

diff -r 2c0af1c2e723 -r ab66951166f3 Admin/components/components.sha1
--- 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
diff -r 2c0af1c2e723 -r ab66951166f3 Admin/components/main
--- 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
diff -r 2c0af1c2e723 -r ab66951166f3 lib/scripts/getfunctions
--- 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 ()
 {
diff -r 2c0af1c2e723 -r ab66951166f3 src/Pure/Admin/build_fonts.scala
--- 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"
 """)
 
 
diff -r 2c0af1c2e723 -r ab66951166f3 src/Pure/Admin/other_isabelle.scala
--- 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))
 
 
diff -r 2c0af1c2e723 -r ab66951166f3 src/Pure/General/http.scala
--- 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 =>
diff -r 2c0af1c2e723 -r ab66951166f3 src/Pure/System/isabelle_fonts.scala
--- 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 */
diff -r 2c0af1c2e723 -r ab66951166f3 src/Pure/Thy/html.scala
--- 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")
   }
 
diff -r 2c0af1c2e723 -r ab66951166f3 src/Pure/Thy/present.scala
--- 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)
     }
   }