clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;

--- a/src/Doc/System/Sessions.thy	Sun Dec 27 14:08:35 2020 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Dec 27 15:11:06 2020 +0100
@@ -405,7 +405,9 @@
   \<^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}).
+  @{setting_ref ISABELLE_BROWSER_INFO_SYSTEM}). This applies only to
+  explicitly selected sessions; note that option \<open>-R\<close> allows to select all
+  requirements separately.
 
   \<^medskip>
   Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected

--- a/src/Pure/Tools/build.scala	Sun Dec 27 14:08:35 2020 +0100
+++ b/src/Pure/Tools/build.scala	Sun Dec 27 15:11:06 2020 +0100
@@ -215,6 +215,8 @@
     val full_sessions =
       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
 
+    val full_sessions_selection = full_sessions.imports_selection(selection)
+
     def sources_stamp(deps: Sessions.Deps, session_name: String): String =
     {
       val digests =
@@ -277,7 +279,7 @@
     store.prepare_output_dir()
 
     if (clean_build) {
-      for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) {
+      for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
         val (relevant, ok) = store.clean_output(name)
         if (relevant) {
           if (ok) progress.echo("Cleaned " + name)
@@ -492,11 +494,12 @@
     /* PDF/HTML presentation */
 
     if (!no_build && !progress.stopped && results.ok) {
+      val selected = full_sessions_selection.toSet
       val presentation_chapters =
         (for {
           session_name <- deps.sessions_structure.build_topological_order.iterator
           info = results.info(session_name)
-          if presentation.enabled(info) && results(session_name).ok }
+          if selected(session_name) && presentation.enabled(info) && results(session_name).ok }
         yield (info.chapter, (session_name, info.description))).toList
 
       if (presentation_chapters.nonEmpty) {