--- a/src/Doc/System/Presentation.thy Wed Nov 18 13:14:01 2020 +0100
+++ b/src/Doc/System/Presentation.thy Wed Nov 18 13:16:08 2020 +0100
@@ -130,6 +130,7 @@
Options are:
-O set option "document_output", relative to current directory
+ -P DIR enable HTML/PDF presentation in directory (":" for default)
-V verbose latex
-d DIR include session directory
-n no build of session
@@ -144,7 +145,8 @@
notably essential Isabelle style files, and \<^verbatim>\<open>session.tex\<close> to input all
theory sources from the session (excluding imports from other sessions).
- \<^medskip> Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool build}.
+ \<^medskip> Options \<^verbatim>\<open>-P\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool
+ build}.
\<^medskip> Option \<^verbatim>\<open>-V\<close> prints full output of {\LaTeX} tools.
--- a/src/Doc/System/Sessions.thy Wed Nov 18 13:14:01 2020 +0100
+++ b/src/Doc/System/Sessions.thy Wed Nov 18 13:16:08 2020 +0100
@@ -317,6 +317,7 @@
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
+ -P DIR enable HTML/PDF presentation in directory (":" for default)
-R refer to requirements of selected sessions
-S soft build: only observe changes of sources, not heap images
-X NAME exclude sessions from group NAME and all descendants
@@ -402,6 +403,11 @@
the command-line are applied in the given order.
\<^medskip>
+ Option \<^verbatim>\<open>-P\<close> enables PDF/HTML presentation in the given directory, where
+ ``\<^verbatim>\<open>-P:\<close>'' refers to the default @{setting_ref ISABELLE_BROWSER_INFO} (or
+ @{setting_ref ISABELLE_BROWSER_INFO_SYSTEM}).
+
+ \<^medskip>
Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
sessions. By default, images are only saved for inner nodes of the hierarchy
of sessions, as required for other sessions to continue later on.
--- 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)
}
})
}
--- a/src/Pure/Thy/sessions.scala Wed Nov 18 13:14:01 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Nov 18 13:16:08 2020 +0100
@@ -463,8 +463,6 @@
export_files: List[(Path, Int, List[String])],
meta_digest: SHA1.Digest)
{
- def chapter_session: Path = Path.basic(chapter) + Path.basic(name)
-
def deps: List[String] = parent.toList ::: imports
def deps_base(session_bases: String => Base): Base =
@@ -517,6 +515,8 @@
case s => Some(dir + Path.explode(s))
}
+ def browser_info: Boolean = options.bool("browser_info")
+
lazy val bibtex_entries: List[Text.Info[String]] =
(for {
(document_dir, file) <- document_files.iterator
@@ -1197,7 +1197,7 @@
if (system_heaps) List(system_output_dir)
else List(user_output_dir, system_output_dir)
- val browser_info: Path =
+ def presentation_dir: Path =
if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
else Path.explode("$ISABELLE_BROWSER_INFO")
--- a/src/Pure/Tools/build.scala Wed Nov 18 13:14:01 2020 +0100
+++ b/src/Pure/Tools/build.scala Wed Nov 18 13:16:08 2020 +0100
@@ -158,6 +158,7 @@
deps: Sessions.Deps,
store: Sessions.Store,
do_store: Boolean,
+ presentation: Present.Context,
verbose: Boolean,
val numa_node: Option[Int],
command_timings0: List[Properties.T])
@@ -370,8 +371,8 @@
Present.build_documents(session_name, deps, store, verbose = verbose,
verbose_latex = true, progress = document_progress)
}
- if (info.options.bool("browser_info")) {
- val dir = Present.session_html(session_name, deps, store)
+ if (presentation.enabled(info)) {
+ val dir = Present.session_html(session_name, deps, store, presentation)
if (verbose) progress.echo("Browser info at " + dir.absolute)
}
}
@@ -481,6 +482,7 @@
def build(
options: Options,
selection: Sessions.Selection = Sessions.Selection.empty,
+ presentation: Present.Context = Present.Context.none,
progress: Progress = new Progress,
check_unknown_files: Boolean = false,
build_heap: Boolean = false,
@@ -729,8 +731,8 @@
val numa_node = numa_nodes.next(used_node)
val job =
- new Job(progress, session_name, info, deps, store, do_store, verbose,
- numa_node, queue.command_timings(session_name))
+ new Job(progress, session_name, info, deps, store, do_store, presentation,
+ verbose, numa_node, queue.command_timings(session_name))
loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
}
else {
@@ -794,14 +796,16 @@
(name, result) <- results0.iterator
if result.ok
info = full_sessions(name)
- if info.options.bool("browser_info")
+ if presentation.enabled(info)
} yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
+ val dir = presentation.dir(store)
+
for ((chapter, entries) <- browser_chapters)
- Present.update_chapter_index(store.browser_info, chapter, entries)
+ Present.update_chapter_index(dir, chapter, entries)
- if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
+ if (browser_chapters.nonEmpty) Present.make_global_index(dir)
}
results
@@ -817,6 +821,7 @@
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var numa_shuffling = false
+ var presentation = Present.Context.none
var requirements = false
var soft_build = false
var exclude_session_groups: List[String] = Nil
@@ -842,6 +847,7 @@
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
+ -P DIR enable HTML/PDF presentation in directory (":" for default)
-R refer to requirements of selected sessions
-S soft build: only observe changes of sources, not heap images
-X NAME exclude sessions from group NAME and all descendants
@@ -866,6 +872,7 @@
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"N" -> (_ => numa_shuffling = true),
+ "P:" -> (arg => presentation = Present.Context.make(arg)),
"R" -> (_ => requirements = true),
"S" -> (_ => soft_build = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
@@ -908,6 +915,7 @@
exclude_sessions = exclude_sessions,
session_groups = session_groups,
sessions = sessions),
+ presentation = presentation,
progress = progress,
check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
build_heap = build_heap,