# HG changeset patch # User wenzelm # Date 1661077178 -7200 # Node ID 603852abed8f2469b7da2bd525f501f6feb3f6bc # Parent 4bbbbaa656f1c65f17f615cb9e4e2b627975faed clarified names: Browser_Info.Config vs. Browser_Info.Context; diff -r 4bbbbaa656f1 -r 603852abed8f src/Pure/Thy/browser_info.scala --- 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)) } } diff -r 4bbbbaa656f1 -r 603852abed8f src/Pure/Tools/build.scala --- 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, diff -r 4bbbbaa656f1 -r 603852abed8f src/Tools/VSCode/src/preview_panel.scala --- 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 } diff -r 4bbbbaa656f1 -r 603852abed8f src/Tools/jEdit/src/document_model.scala --- 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)