# HG changeset patch # User Fabian Huch # Date 1739552811 -3600 # Node ID 3f3769c50bf5d9ab5c8ca806ce89efff8521613f # Parent 2cc21c84232d6ba69fa6b5a143fa32e8812550b4 tuned; diff -r 2cc21c84232d -r 3f3769c50bf5 src/Tools/Find_Facts/src/find_facts.scala --- a/src/Tools/Find_Facts/src/find_facts.scala Fri Feb 14 17:40:21 2025 +0100 +++ b/src/Tools/Find_Facts/src/find_facts.scala Fri Feb 14 18:06:51 2025 +0100 @@ -629,10 +629,10 @@ val session = Session(options, Resources.bootstrap) val selection = Sessions.Selection(sessions = sessions) - val session_structure = + val sessions_structure = Sessions.load_structure(options, dirs = AFP.main_dirs(afp_root) ::: dirs).selection(selection) - val deps = Sessions.Deps.load(session_structure) - val context = Browser_Info.context(session_structure) + val deps = Sessions.Deps.load(sessions_structure) + val context = Browser_Info.context(sessions_structure) if (sessions.isEmpty) progress.echo("Nothing to index") else { @@ -644,7 +644,7 @@ using(Export.open_database_context(store)) { database_context => val document_info = Document_Info.read(database_context, deps, sessions) val context1 = - Browser_Info.context(session_structure, root_dir = root_dir, + Browser_Info.context(sessions_structure, root_dir = root_dir, document_info = document_info) if (browser_info) context1.update_root() @@ -653,7 +653,7 @@ if (browser_info) deps.background(session_name) else Sessions.background0(session_name) using(database_context.open_session(background)) { session_context => - val info = session_structure(session_name) + val info = sessions_structure(session_name) progress.echo("Session " + info.chapter + "/" + session_name + " ...") if (browser_info) Browser_Info.build_session(context1, session_context)