clarified modules;
authorwenzelm
Wed Nov 28 11:28:02 2018 +0100 (19 months ago)
changeset 69355cdc2de88d657
parent 69354 600727ff6889
child 69356 32f886aaf9c0
clarified modules;
src/Pure/Admin/other_isabelle.scala
src/Pure/GUI/gui.scala
src/Pure/General/graphics_file.scala
src/Pure/General/http.scala
src/Pure/System/isabelle_fonts.scala
src/Pure/System/isabelle_system.scala
src/Pure/Thy/html.scala
src/Pure/Thy/present.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Admin/other_isabelle.scala	Wed Nov 28 11:06:58 2018 +0100
     1.2 +++ b/src/Pure/Admin/other_isabelle.scala	Wed Nov 28 11:28:02 2018 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4    val etc_preferences: Path = etc + Path.explode("preferences")
     1.5  
     1.6    def fonts(html: Boolean = false): List[Path] =
     1.7 -    Isabelle_System.fonts(html = html, get = getenv(_))
     1.8 +    Isabelle_Fonts.files(html = html, getenv = getenv(_))
     1.9  
    1.10  
    1.11    /* settings */
     2.1 --- a/src/Pure/GUI/gui.scala	Wed Nov 28 11:06:58 2018 +0100
     2.2 +++ b/src/Pure/GUI/gui.scala	Wed Nov 28 11:28:02 2018 +0100
     2.3 @@ -242,8 +242,8 @@
     2.4    def install_fonts()
     2.5    {
     2.6      val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
     2.7 -    for (font <- Isabelle_System.fonts())
     2.8 -      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
     2.9 +    for (path <- Isabelle_Fonts.files())
    2.10 +      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, path.file))
    2.11    }
    2.12  }
    2.13  
     3.1 --- a/src/Pure/General/graphics_file.scala	Wed Nov 28 11:06:58 2018 +0100
     3.2 +++ b/src/Pure/General/graphics_file.scala	Wed Nov 28 11:28:02 2018 +0100
     3.3 @@ -45,7 +45,7 @@
     3.4    {
     3.5      val mapper = new DefaultFontMapper
     3.6      for {
     3.7 -      font <- Isabelle_System.fonts()
     3.8 +      font <- Isabelle_Fonts.files()
     3.9        name <- Library.try_unsuffix(".ttf", font.base_name)
    3.10      } {
    3.11        val parameters = new DefaultFontMapper.BaseFontParameters(File.platform_path(font))
     4.1 --- a/src/Pure/General/http.scala	Wed Nov 28 11:06:58 2018 +0100
     4.2 +++ b/src/Pure/General/http.scala	Wed Nov 28 11:28:02 2018 +0100
     4.3 @@ -156,7 +156,7 @@
     4.4  
     4.5    private lazy val html_fonts: SortedMap[String, Bytes] =
     4.6      SortedMap(
     4.7 -      Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
     4.8 +      Isabelle_Fonts.files(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
     4.9  
    4.10    def fonts(root: String = "/fonts"): Handler =
    4.11      get(root, arg =>
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/System/isabelle_fonts.scala	Wed Nov 28 11:28:02 2018 +0100
     5.3 @@ -0,0 +1,27 @@
     5.4 +/*  Title:      Pure/System/isabelle_system.scala
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Fonts from the Isabelle system environment, notably the "Isabelle DejaVu"
     5.8 +collection.
     5.9 +*/
    5.10 +
    5.11 +package isabelle
    5.12 +
    5.13 +
    5.14 +object Isabelle_Fonts
    5.15 +{
    5.16 +  /* Isabelle system environment */
    5.17 +
    5.18 +  def variables(html: Boolean = false): List[String] =
    5.19 +    if (html) List("ISABELLE_FONTS", "ISABELLE_FONTS_HTML") else List("ISABELLE_FONTS")
    5.20 +
    5.21 +  def files(
    5.22 +    html: Boolean = false,
    5.23 +    getenv: String => String = Isabelle_System.getenv_strict(_)): List[Path] =
    5.24 +  {
    5.25 +    for {
    5.26 +      variable <- variables(html = html)
    5.27 +      path <- Path.split(getenv(variable))
    5.28 +    } yield path
    5.29 +  }
    5.30 +}
     6.1 --- a/src/Pure/System/isabelle_system.scala	Wed Nov 28 11:06:58 2018 +0100
     6.2 +++ b/src/Pure/System/isabelle_system.scala	Wed Nov 28 11:28:02 2018 +0100
     6.3 @@ -365,19 +365,6 @@
     6.4    }
     6.5  
     6.6  
     6.7 -  /* fonts */
     6.8 -
     6.9 -  def fonts(html: Boolean = false, get: String => String = getenv_strict(_)): List[Path] =
    6.10 -  {
    6.11 -    val variables =
    6.12 -      if (html) List("ISABELLE_FONTS", "ISABELLE_FONTS_HTML") else List("ISABELLE_FONTS")
    6.13 -    for {
    6.14 -      variable <- variables
    6.15 -      path <- Path.split(get(variable))
    6.16 -    } yield path
    6.17 -  }
    6.18 -
    6.19 -
    6.20    /* default logic */
    6.21  
    6.22    def default_logic(args: String*): String =
     7.1 --- a/src/Pure/Thy/html.scala	Wed Nov 28 11:06:58 2018 +0100
     7.2 +++ b/src/Pure/Thy/html.scala	Wed Nov 28 11:28:02 2018 +0100
     7.3 @@ -350,8 +350,8 @@
     7.4    /* fonts */
     7.5  
     7.6    def fonts_url(): String => String =
     7.7 -    (for (font <- Isabelle_System.fonts(html = true))
     7.8 -     yield (font.base_name -> Url.print_file(font.file))).toMap
     7.9 +    (for (path <- Isabelle_Fonts.files(html = true))
    7.10 +     yield (path.base_name -> Url.print_file(path.file))).toMap
    7.11  
    7.12    def fonts_dir(prefix: String)(ttf_name: String): String =
    7.13      prefix + "/" + ttf_name
     8.1 --- a/src/Pure/Thy/present.scala	Wed Nov 28 11:06:58 2018 +0100
     8.2 +++ b/src/Pure/Thy/present.scala	Wed Nov 28 11:28:02 2018 +0100
     8.3 @@ -96,8 +96,8 @@
     8.4  
     8.5        HTML.write_isabelle_css(session_prefix)
     8.6  
     8.7 -      for (font <- Isabelle_System.fonts(html = true))
     8.8 -        File.copy(font, session_fonts)
     8.9 +      for (path <- Isabelle_Fonts.files(html = true))
    8.10 +        File.copy(path, session_fonts)
    8.11      }
    8.12    }
    8.13  
     9.1 --- a/src/Pure/build-jars	Wed Nov 28 11:06:58 2018 +0100
     9.2 +++ b/src/Pure/build-jars	Wed Nov 28 11:28:02 2018 +0100
     9.3 @@ -118,6 +118,7 @@
     9.4    System/getopts.scala
     9.5    System/invoke_scala.scala
     9.6    System/isabelle_charset.scala
     9.7 +  System/isabelle_fonts.scala
     9.8    System/isabelle_process.scala
     9.9    System/isabelle_system.scala
    9.10    System/isabelle_tool.scala