equal
deleted
inserted
replaced
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")) |