src/Pure/Admin/build_fonts.scala
changeset 71726 a5fda30edae2
parent 71602 d5502ee7c141
child 72375 e48d93811ed7
equal deleted inserted replaced
71725:c255ed582095 71726:a5fda30edae2
   214     sources: List[Family] = default_sources,
   214     sources: List[Family] = default_sources,
   215     source_dirs: List[Path] = Nil,
   215     source_dirs: List[Path] = Nil,
   216     target_prefix: String = "Isabelle",
   216     target_prefix: String = "Isabelle",
   217     target_version: String = "",
   217     target_version: String = "",
   218     target_dir: Path = default_target_dir,
   218     target_dir: Path = default_target_dir,
   219     progress: Progress = No_Progress)
   219     progress: Progress = new Progress)
   220   {
   220   {
   221     progress.echo("Directory " + target_dir)
   221     progress.echo("Directory " + target_dir)
   222     hinting.foreach(hinted => Isabelle_System.mkdirs(target_dir + hinted_path(hinted)))
   222     hinting.foreach(hinted => Isabelle_System.mkdirs(target_dir + hinted_path(hinted)))
   223 
   223 
   224     val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts"))
   224     val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts"))