clarified names: Browser_Info.Config vs. Browser_Info.Context;

--- a/src/Pure/Thy/browser_info.scala	Sun Aug 21 11:59:25 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Sun Aug 21 12:19:38 2022 +0200
@@ -15,16 +15,16 @@
 object Browser_Info {
   /** HTML documents **/
 
-  /* HTML context */
+  /* PDF/HTML presentation context */
 
-  def html_context(
+  def context(
     sessions_structure: Sessions.Structure,
     elements: Elements,
     root_dir: Path = Path.current,
     document_info: Document_Info = Document_Info.empty
-  ): HTML_Context = new HTML_Context(sessions_structure, elements, root_dir, document_info)
+  ): Context = new Context(sessions_structure, elements, root_dir, document_info)
 
-  class HTML_Context private[Browser_Info](
+  class Context private[Browser_Info](
     sessions_structure: Sessions.Structure,
     val elements: Elements,
     val root_dir: Path,
@@ -135,14 +135,14 @@
     val empty: Node_Context = new Node_Context
 
     def make(
-      html_context: HTML_Context,
+      context: Context,
       session_name: String,
       theory_name: String,
       file_name: String,
       node_dir: Path,
     ): Node_Context =
       new Node_Context {
-        private val session_dir = html_context.session_dir(session_name)
+        private val session_dir = context.session_dir(session_name)
 
         private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
 
@@ -150,7 +150,7 @@
           body match {
             case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
             case _ =>
-              for (theory <- html_context.theory_by_name(session_name, theory_name))
+              for (theory <- context.theory_by_name(session_name, theory_name))
               yield {
                 val body1 =
                   if (seen_ranges.contains(range)) {
@@ -170,9 +170,9 @@
         override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = {
           props match {
             case Theory_Ref(thy_name) =>
-              for (theory <- html_context.theory_by_name(session_name, thy_name))
+              for (theory <- context.theory_by_name(session_name, thy_name))
               yield {
-                val html_path = session_dir + html_context.theory_html(theory)
+                val html_path = session_dir + context.theory_html(theory)
                 val html_link = HTML.relative_href(html_path, base = Some(node_dir))
                 HTML.link(html_link, body)
               }
@@ -189,11 +189,11 @@
                 }
 
               for {
-                theory <- html_context.theory_by_file(session_name, def_file)
+                theory <- context.theory_by_file(session_name, def_file)
                 html_ref <- logical_ref(theory) orElse physical_ref(theory)
               }
               yield {
-                val html_path = session_dir + html_context.smart_html(theory, def_file)
+                val html_path = session_dir + context.smart_html(theory, def_file)
                 val html_link = HTML.relative_href(html_path, base = Some(node_dir))
                 HTML.entity_ref(HTML.link(html_link + "#" + html_ref, body))
               }
@@ -289,7 +289,7 @@
 
   def html_document(
     snapshot: Document.Snapshot,
-    html_context: HTML_Context,
+    context: Context,
     plain_text: Boolean = false,
     fonts_css: String = HTML.fonts_css()
   ): HTML_Document = {
@@ -299,16 +299,16 @@
     if (plain_text) {
       val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
       val body = HTML.text(snapshot.node.source)
-      html_context.html_document(title, body, fonts_css)
+      context.html_document(title, body, fonts_css)
     }
     else {
       Resources.html_document(snapshot) getOrElse {
         val title =
           if (name.is_theory) "Theory " + quote(name.theory_base_name)
           else "File " + Symbol.cartouche_decoded(name.path.file_name)
-        val xml = snapshot.xml_markup(elements = html_context.elements.html)
-        val body = Node_Context.empty.make_html(html_context.elements, xml)
-        html_context.html_document(title, body, fonts_css)
+        val xml = snapshot.xml_markup(elements = context.elements.html)
+        val body = Node_Context.empty.make_html(context.elements, xml)
+        context.html_document(title, body, fonts_css)
       }
     }
   }
@@ -317,23 +317,23 @@
 
   /** HTML presentation **/
 
-  /* presentation context */
+  /* browser_info store configuration */
 
-  object Context {
-    val none: Context = new Context { def enabled: Boolean = false }
-    val standard: Context = new Context { def enabled: Boolean = true }
+  object Config {
+    val none: Config = new Config { def enabled: Boolean = false }
+    val standard: Config = new Config { def enabled: Boolean = true }
 
-    def dir(path: Path): Context =
-      new Context {
+    def dir(path: Path): Config =
+      new Config {
         def enabled: Boolean = true
         override def dir(store: Sessions.Store): Path = path
       }
 
-    def make(s: String): Context =
+    def make(s: String): Config =
       if (s == ":") standard else dir(Path.explode(s))
   }
 
-  abstract class Context private {
+  abstract class Config private {
     def enabled: Boolean
     def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
     def dir(store: Sessions.Store): Path = store.presentation_dir
@@ -430,7 +430,7 @@
   val session_graph_path: Path = Path.explode("session_graph.pdf")
 
   def session_html(
-    html_context: HTML_Context,
+    context: Context,
     session_context: Export.Session_Context,
     progress: Progress = new Progress,
     verbose: Boolean = false,
@@ -439,11 +439,11 @@
     val session_info = session_context.sessions_structure(session_name)
 
     val session_dir =
-      Isabelle_System.make_directory(html_context.session_dir(session_name)).expand
+      Isabelle_System.make_directory(context.session_dir(session_name)).expand
 
     progress.echo("Presenting " + session_name + " in " + session_dir + " ...")
 
-    val session = html_context.document_info.the_session(session_name)
+    val session = context.document_info.the_session(session_name)
 
     Bytes.write(session_dir + session_graph_path,
       graphview.Graph_File.make_pdf(session_info.options,
@@ -481,18 +481,18 @@
         error("Missing document information for theory: " + quote(theory_name))
 
       val command = Build_Job.read_theory(session_context.theory(theory_name)) getOrElse err()
-      val theory = html_context.theory_by_name(session_name, theory_name) getOrElse err()
+      val theory = context.theory_by_name(session_name, theory_name) getOrElse err()
 
       if (verbose) progress.echo("Presenting theory " + quote(theory_name))
       val snapshot = Document.State.init.snippet(command)
 
-      val thy_elements = theory.elements(html_context.elements)
+      val thy_elements = theory.elements(context.elements)
 
       def node_context(file_name: String, node_dir: Path): Node_Context =
-        Node_Context.make(html_context, session_name, theory_name, file_name, node_dir)
+        Node_Context.make(context, session_name, theory_name, file_name, node_dir)
 
       val thy_html =
-        html_context.source(
+        context.source(
           node_context(theory.thy_file, session_dir).
             make_html(thy_elements, snapshot.xml_markup(elements = thy_elements.html)))
 
@@ -506,26 +506,24 @@
           val file_name = blob.name.node
           if (verbose) progress.echo("Presenting file " + quote(file_name))
 
-          val file_html = session_dir + html_context.file_html(file_name)
+          val file_html = session_dir + context.file_html(file_name)
           val file_dir = file_html.dir
           val html_link = HTML.relative_href(file_html, base = Some(session_dir))
-          val html =
-            html_context.source(
-              node_context(file_name, file_dir).make_html(thy_elements, xml))
+          val html = context.source(node_context(file_name, file_dir).make_html(thy_elements, xml))
 
           val file_title = "File " + Symbol.cartouche_decoded(blob.src_path.implode_short)
           HTML.write_document(file_dir, file_html.file_name,
-            List(HTML.title(file_title)), List(html_context.head(file_title), html),
-            root = Some(html_context.root_dir))
+            List(HTML.title(file_title)), List(context.head(file_title), html),
+            root = Some(context.root_dir))
           List(HTML.link(html_link, HTML.text(file_title)))
         }
 
       val thy_title = "Theory " + theory.print_short
-      HTML.write_document(session_dir, html_context.theory_html(theory).implode,
-        List(HTML.title(thy_title)), List(html_context.head(thy_title), thy_html),
-        root = Some(html_context.root_dir))
+      HTML.write_document(session_dir, context.theory_html(theory).implode,
+        List(HTML.title(thy_title)), List(context.head(thy_title), thy_html),
+        root = Some(context.root_dir))
 
-      List(HTML.link(html_context.theory_html(theory),
+      List(HTML.link(context.theory_html(theory),
         HTML.text(theory.print_short) :::
         (if (files.isEmpty) Nil else List(HTML.itemize(files)))))
     }
@@ -535,8 +533,8 @@
     val title = "Session " + session_name
       HTML.write_document(session_dir, "index.html",
         List(HTML.title(title + Isabelle_System.isabelle_heading())),
-        html_context.head(title, List(HTML.par(document_links))) ::
-          html_context.contents("Theories", theories),
-        root = Some(html_context.root_dir))
+        context.head(title, List(HTML.par(document_links))) ::
+          context.contents("Theories", theories),
+        root = Some(context.root_dir))
   }
 }

--- a/src/Pure/Tools/build.scala	Sun Aug 21 11:59:25 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sun Aug 21 12:19:38 2022 +0200
@@ -163,7 +163,7 @@
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
-    presentation: Browser_Info.Context = Browser_Info.Context.none,
+    browser_info: Browser_Info.Config = Browser_Info.Config.none,
     progress: Progress = new Progress,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
@@ -238,7 +238,7 @@
       (for {
         session_name <- deps.sessions_structure.build_topological_order.iterator
         info <- deps.sessions_structure.get(session_name)
-        if full_sessions_selected(session_name) && presentation.enabled(info) }
+        if full_sessions_selected(session_name) && browser_info.enabled(info) }
       yield info).toList
 
 
@@ -486,7 +486,7 @@
 
     if (!no_build && !progress.stopped && results.ok) {
       if (presentation_sessions.nonEmpty) {
-        val presentation_dir = presentation.dir(store)
+        val presentation_dir = browser_info.dir(store)
         progress.echo("Presentation in " + presentation_dir.absolute)
         Browser_Info.update_root(presentation_dir)
 
@@ -502,12 +502,12 @@
           Par_List.map({ (session: String) =>
             progress.expose_interrupt()
 
-            val html_context =
-              Browser_Info.html_context(deps.sessions_structure, Browser_Info.elements1,
+            val context =
+              Browser_Info.context(deps.sessions_structure, Browser_Info.elements1,
                 root_dir = presentation_dir, document_info = document_info)
 
             using(database_context.open_session(deps.base_info(session))) { session_context =>
-              Browser_Info.session_html(html_context, session_context,
+              Browser_Info.session_html(context, session_context,
                 progress = progress, verbose = verbose)
             }
           }, presentation_sessions.map(_.name))
@@ -529,7 +529,7 @@
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
       var numa_shuffling = false
-      var presentation = Browser_Info.Context.none
+      var browser_info = Browser_Info.Config.none
       var requirements = false
       var soft_build = false
       var exclude_session_groups: List[String] = Nil
@@ -580,7 +580,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 = Browser_Info.Context.make(arg)),
+        "P:" -> (arg => browser_info = Browser_Info.Config.make(arg)),
         "R" -> (_ => requirements = true),
         "S" -> (_ => soft_build = true),
         "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
@@ -623,7 +623,7 @@
               exclude_sessions = exclude_sessions,
               session_groups = session_groups,
               sessions = sessions),
-            presentation = presentation,
+            browser_info = browser_info,
             progress = progress,
             check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
             build_heap = build_heap,

--- a/src/Tools/VSCode/src/preview_panel.scala	Sun Aug 21 11:59:25 2022 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala	Sun Aug 21 12:19:38 2022 +0200
@@ -28,9 +28,9 @@
                 val snapshot = model.snapshot()
                 if (snapshot.is_outdated) m
                 else {
-                  val html_context =
-                    Browser_Info.html_context(resources.sessions_structure, Browser_Info.elements2)
-                  val document = Browser_Info.html_document(snapshot, html_context)
+                  val context =
+                    Browser_Info.context(resources.sessions_structure, Browser_Info.elements2)
+                  val document = Browser_Info.html_document(snapshot, context)
                   channel.write(LSP.Preview_Response(file, column, document.title, document.content))
                   m - file
                 }

--- a/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 11:59:25 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 12:19:38 2022 +0200
@@ -313,10 +313,10 @@
       }
       yield {
         val snapshot = model.await_stable_snapshot()
-        val html_context =
-          Browser_Info.html_context(PIDE.resources.sessions_structure, Browser_Info.elements2)
+        val context =
+          Browser_Info.context(PIDE.resources.sessions_structure, Browser_Info.elements2)
         val document =
-          Browser_Info.html_document(snapshot, html_context,
+          Browser_Info.html_document(snapshot, context,
             plain_text = query.startsWith(plain_text_prefix),
             fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name)))
         HTTP.Response.html(document.content)