diff -r fd6dc1a4b9ca -r 1cbac4ae934d src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Wed Nov 18 13:14:01 2020 +0100 +++ b/src/Pure/Thy/present.scala Wed Nov 18 13:16:08 2020 +0100 @@ -12,6 +12,33 @@ object Present { + /* presentation context */ + + object Context + { + val none: Context = new Context { def enabled: Boolean = false } + val standard: Context = new Context { def enabled: Boolean = true } + + def dir(path: Path): Context = + new Context { + def enabled: Boolean = true + override def dir(store: Sessions.Store): Path = path + } + + def make(s: String): Context = + if (s == ":") standard else dir(Path.explode(s)) + } + + abstract class Context private + { + def enabled: Boolean + def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info + def dir(store: Sessions.Store): Path = store.presentation_dir + def dir(store: Sessions.Store, info: Sessions.Info): Path = + dir(store) + Path.basic(info.chapter) + Path.basic(info.name) + } + + /* maintain chapter index -- NOT thread-safe */ private val sessions_path = Path.basic(".sessions") @@ -83,13 +110,17 @@ def theory_link(name: Document.Node.Name): XML.Tree = HTML.link(html_name(name), HTML.text(name.theory_base_name)) - def session_html(session: String, deps: Sessions.Deps, store: Sessions.Store): Path = + def session_html( + session: String, + deps: Sessions.Deps, + store: Sessions.Store, + presentation: Context): Path = { val info = deps.sessions_structure(session) val options = info.options val base = deps(session) - val session_dir = store.browser_info + info.chapter_session + val session_dir = presentation.dir(store, info) val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts")) for (entry <- Isabelle_Fonts.fonts(hidden = true)) File.copy(entry.path, session_fonts) @@ -255,6 +286,7 @@ deps: Sessions.Deps, store: Sessions.Store, progress: Progress = new Progress, + presentation: Context = Context.none, verbose: Boolean = false, verbose_latex: Boolean = false): List[(String, Bytes)] = { @@ -369,8 +401,8 @@ } } - if (info.options.bool("browser_info") || doc_output.isEmpty) { - output(store.browser_info + info.chapter_session) + if (presentation.enabled(info) || doc_output.isEmpty) { + output(presentation.dir(store, info)) } doc_output.foreach(output) @@ -384,6 +416,7 @@ val isabelle_tool = Isabelle_Tool("document", "prepare session theory document", args => { + var presentation = Present.Context.none var verbose_latex = false var dirs: List[Path] = Nil var no_build = false @@ -395,6 +428,7 @@ Usage: isabelle document [OPTIONS] SESSION Options are: + -P DIR enable HTML/PDF presentation in directory (":" for default) -O set option "document_output", relative to current directory -V verbose latex -d DIR include session directory @@ -404,6 +438,7 @@ Prepare the theory document of a session. """, + "P:" -> (arg => presentation = Context.make(arg)), "O:" -> (arg => options += ("document_output=" + Path.explode(arg).absolute.implode)), "V" -> (_ => verbose_latex = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), @@ -434,7 +469,7 @@ selection_deps(Sessions.Selection.session(session)) build_documents(session, deps, store, progress = progress, - verbose = true, verbose_latex = verbose_latex) + presentation = presentation, verbose = true, verbose_latex = verbose_latex) } }) }