equal
deleted
inserted
replaced
60 val etc: Path = isabelle_home_user + Path.explode("etc") |
60 val etc: Path = isabelle_home_user + Path.explode("etc") |
61 val etc_settings: Path = etc + Path.explode("settings") |
61 val etc_settings: Path = etc + Path.explode("settings") |
62 val etc_preferences: Path = etc + Path.explode("preferences") |
62 val etc_preferences: Path = etc + Path.explode("preferences") |
63 |
63 |
64 def fonts(html: Boolean = false): List[Path] = |
64 def fonts(html: Boolean = false): List[Path] = |
65 Isabelle_System.fonts(html = html, get = getenv(_)) |
65 Isabelle_Fonts.files(html = html, getenv = getenv(_)) |
66 |
66 |
67 |
67 |
68 /* settings */ |
68 /* settings */ |
69 |
69 |
70 def clean_settings(): Boolean = |
70 def clean_settings(): Boolean = |