equal
deleted
inserted
replaced
381 { |
381 { |
382 File.write(dir + isabelle_css.base, |
382 File.write(dir + isabelle_css.base, |
383 fonts_css(make_url) + "\n\n" + File.read(isabelle_css)) |
383 fonts_css(make_url) + "\n\n" + File.read(isabelle_css)) |
384 } |
384 } |
385 |
385 |
386 def init_dir(dir: Path) |
386 def init_dir(dir: Path): Unit = |
387 { |
387 write_isabelle_css(Isabelle_System.make_directory(dir)) |
388 Isabelle_System.make_directory(dir) |
|
389 write_isabelle_css(dir) |
|
390 } |
|
391 |
388 |
392 def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, |
389 def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, |
393 css: String = isabelle_css.file_name, |
390 css: String = isabelle_css.file_name, |
394 hidden: Boolean = true, |
391 hidden: Boolean = true, |
395 structural: Boolean = true) |
392 structural: Boolean = true) |