# HG changeset patch # User Fabian Huch # Date 1739529265 -3600 # Node ID c9f845dca3504586841884453f5319d6e7fdbad7 # Parent f3a5a7c64412d7064768bd07b6481683c6e2d82c tuned; diff -r f3a5a7c64412 -r c9f845dca350 src/Tools/Find_Facts/src/find_facts.scala --- a/src/Tools/Find_Facts/src/find_facts.scala Thu Feb 13 16:36:57 2025 +0100 +++ b/src/Tools/Find_Facts/src/find_facts.scala Fri Feb 14 11:34:25 2025 +0100 @@ -473,7 +473,7 @@ def make_thy_blocks( options: Options, session: Session, - browser_info_context: Browser_Info.Context, + context: Browser_Info.Context, document_info: Document_Info, theory_context: Export.Theory_Context, snapshot: Document.Snapshot, @@ -486,7 +486,7 @@ val theory_info = document_info.theory_by_name(session_name, theory).getOrElse( error("No info for theory " + theory)) - val thy_dir = browser_info_context.theory_dir(theory_info) + val thy_dir = context.theory_dir(theory_info) def make_node_blocks( snapshot: Document.Snapshot, @@ -494,7 +494,7 @@ ): List[Block] = { val version = snapshot.version.id val file = Path.explode(snapshot.node_name.node).squash.implode - val url_path = thy_dir + browser_info_context.smart_html(theory_info, snapshot.node_name.node) + val url_path = thy_dir + context.smart_html(theory_info, snapshot.node_name.node) val elements = Browser_Info.Elements(html = Browser_Info.default_elements.html - Markup.ENTITY) @@ -615,7 +615,7 @@ val session_structure = Sessions.load_structure(options, dirs = AFP.main_dirs(afp_root) ::: dirs).selection(selection) val deps = Sessions.Deps.load(session_structure) - val browser_info_context = Browser_Info.context(session_structure) + val context = Browser_Info.context(session_structure) if (sessions.isEmpty) progress.echo("Nothing to index") else { @@ -638,8 +638,8 @@ case Some(snapshot) => progress.echo("Indexing theory " + quote(name.theory), verbose = true) val blocks = - make_thy_blocks(options, session, browser_info_context, document_info, - theory_context, snapshot, info.chapter) + make_thy_blocks(options, session, context, document_info, theory_context, + snapshot, info.chapter) Find_Facts.private_data.update_theory(db, theory_context.theory, blocks) } }