--- a/src/Tools/Find_Facts/src/find_facts.scala Fri Feb 14 15:24:42 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala Fri Feb 14 17:40:21 2025 +0100
@@ -115,6 +115,11 @@
val solr_data_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/solr")
object private_data extends Solr.Data("find_facts") {
+ /* meta info */
+
+ val browser_info_database = new Properties.String("browser_info_database")
+
+
/* types */
val symbol_codes =
@@ -447,6 +452,18 @@
}
}
+ def meta_info(browser_info_database: Option[Path] = None): Properties.T =
+ browser_info_database match {
+ case Some(path) => Find_Facts.private_data.browser_info_database(path.implode)
+ case None => Nil
+ }
+
+ def browser_info_database(db: Solr.Database): Path =
+ db.props match {
+ case Find_Facts.private_data.browser_info_database(file) => db.dir + Path.explode(file)
+ case _ => Browser_Info.default_database
+ }
+
def query_block(db: Solr.Database, id: String): Option[Block] = {
val q = Solr.filter(Find_Facts.private_data.Fields.id, Solr.phrase(id))
Find_Facts.private_data.read_blocks(db, q, Nil).blocks.headOption
@@ -473,7 +490,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 +503,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 +511,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)
@@ -585,13 +602,13 @@
isabelle_home: Path = Path.current,
options: List[Options.Spec] = Nil,
dirs: List[Path] = Nil,
- clean: Boolean = false,
+ browser_info: Boolean = true,
no_build: Boolean = false,
verbose: Boolean = false,
): String = {
ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " find_facts_index" +
dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
- if_proper(clean, " -c") +
+ if_proper(!browser_info, " -N") +
if_proper(no_build, " -n") +
if_proper(verbose, " -v") +
Options.Spec.bash_strings(options, bg = true) +
@@ -603,7 +620,7 @@
sessions: List[String],
afp_root: Option[Path] = None,
dirs: List[Path] = Nil,
- clean: Boolean = false,
+ browser_info: Boolean = true,
progress: Progress = new Progress
): Unit = {
val store = Store(options)
@@ -615,47 +632,62 @@
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 {
- val start_date = Date.now()
- val stats =
- using(solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
- using(Export.open_database_context(store)) { database_context =>
- val document_info = Document_Info.read(database_context, deps, sessions)
-
- def index_session(session_name: String): Unit = {
- using(database_context.open_session0(session_name)) { session_context =>
- val info = session_structure(session_name)
- progress.echo("Session " + info.chapter + "/" + session_name + " ...")
+ Isabelle_System.with_tmp_dir("browser_info") { root_dir =>
+ val start_date = Date.now()
+ val props = meta_info(if (browser_info) Some(Path.basic("browser_info.db")) else None)
+ val stats =
+ using(solr.init_database(database, Find_Facts.private_data, props, clean = true)) { db =>
+ 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,
+ document_info = document_info)
+ if (browser_info) context1.update_root()
- Find_Facts.private_data.delete_session(db, session_name)
- deps(session_name).proper_session_theories.foreach { name =>
- val theory_context = session_context.theory(name.theory)
- Build.read_theory(theory_context) match {
- case None => progress.echo_warning("No snapshot for theory " + name.theory)
- 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)
- Find_Facts.private_data.update_theory(db, theory_context.theory, blocks)
+ def index_session(session_name: String): Unit = {
+ val background =
+ 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)
+ progress.echo("Session " + info.chapter + "/" + session_name + " ...")
+
+ if (browser_info) Browser_Info.build_session(context1, session_context)
+
+ Find_Facts.private_data.delete_session(db, session_name)
+ deps(session_name).proper_session_theories.foreach { name =>
+ val theory_context = session_context.theory(name.theory)
+ Build.read_theory(theory_context) match {
+ case None => progress.echo_warning("No snapshot for theory " + name.theory)
+ case Some(snapshot) =>
+ progress.echo("Indexing theory " + quote(name.theory), verbose = true)
+ val blocks =
+ make_thy_blocks(options, session, context, document_info, theory_context,
+ snapshot, info.chapter)
+ Find_Facts.private_data.update_theory(db, theory_context.theory, blocks)
+ }
}
}
}
+
+ Par_List.map(index_session, sessions)
+
+ if (browser_info)
+ Browser_Info.make_database(db.dir + Path.basic("browser_info.db"), root_dir)
}
- Par_List.map(index_session, sessions)
+ val query = Query(Field_Filter(Field.session, sessions.map(Atom.Exact(_))))
+ Find_Facts.query_stats(db, query)
}
- val query = Query(Field_Filter(Field.session, sessions.map(Atom.Exact(_))))
- Find_Facts.query_stats(db, query)
- }
-
- val timing = Date.now() - start_date
- progress.echo("Indexed " + stats.results + " blocks with " + stats.consts + " consts, " +
- stats.typs + " typs, " + stats.thms + " thms in " + timing.message)
+ val timing = Date.now() - start_date
+ progress.echo("Indexed " + stats.results + " blocks with " + stats.consts + " consts, " +
+ stats.typs + " typs, " + stats.thms + " thms in " + timing.message)
+ }
}
}
@@ -665,7 +697,7 @@
def main_tool1(args: Array[String]): Unit = {
Command_Line.tool {
var afp_root: Option[Path] = None
- var clean = false
+ var browser_info = true
val dirs_buffer = new mutable.ListBuffer[Path]
var no_build = false
var options = Options.init()
@@ -676,7 +708,7 @@
Options are:
-A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
- -c clean previous index
+ -N no html presentation -- use """ + Browser_Info.default_database.implode + """
-d DIR include session directory
-n no build -- take existing session build databases
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
@@ -685,7 +717,7 @@
Build and index sessions for Find_Facts.
""",
"A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
- "c" -> (_ => clean = true),
+ "N" -> (_ => browser_info = false),
"d:" -> (arg => dirs_buffer += Path.explode(arg)),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
@@ -719,8 +751,8 @@
/* index */
- find_facts_index(options, sessions, dirs = dirs, afp_root = afp_root, clean = clean,
- progress = progress)
+ find_facts_index(options, sessions, dirs = dirs, afp_root = afp_root,
+ browser_info = browser_info, progress = progress)
}
}
@@ -833,14 +865,9 @@
case class Result(blocks: Blocks, facets: Facets)
- class Encode(options: Options) {
- val library_base_url = Url(options.string("find_facts_url_library"))
- val afp_base_url = Url(options.string("find_facts_url_afp"))
-
- def url(block: Block): Url = {
- val base_url = if (block.chapter == AFP.chapter) afp_base_url else library_base_url
- base_url.resolve(block.url_path.implode)
- }
+ object Encode {
+ def print_url(block: Block): String =
+ HTTP.Browser_Info_Service.name + "/" + block.url_path.implode
def block(block: Block): JSON.T =
JSON.Object(
@@ -850,7 +877,7 @@
"theory" -> block.theory,
"file" -> block.file,
"file_name" -> block.file_name,
- "url" -> url(block).toString,
+ "url" -> print_url(block),
"command" -> block.command,
"start_line" -> block.start_line,
"src_before" -> block.src_before,
@@ -951,7 +978,6 @@
progress: Progress = new Progress
): Unit = {
val database = options.string("find_facts_database_name")
- val encode = new Encode(options)
def rebuild(): String = {
build_html(default_web_dir + web_html, progress = progress)
@@ -976,6 +1002,7 @@
HTTP.server(port, name = "", services = List(
HTTP.Fonts_Service,
HTTP.CSS_Service,
+ HTTP.Browser_Info(database = browser_info_database(db)),
new HTTP.Service("find_facts") {
def apply(request: HTTP.Request): Option[HTTP.Response] =
if (request.toplevel) Some(HTTP.Response.html(if (devel) rebuild() else html))
@@ -991,19 +1018,19 @@
for {
request <- Parse.query_block(body)
block <- query_block(db, request)
- } yield encode.block(block)
+ } yield Encode.block(block)
},
new HTTP.REST_Service("api/blocks", progress = progress) {
def handle(body: JSON.T): Option[JSON.T] =
for (request <- Parse.query_blocks(body))
- yield encode.blocks(query_blocks(db, request.query, Some(request.cursor)))
+ yield Encode.blocks(query_blocks(db, request.query, Some(request.cursor)))
},
new HTTP.REST_Service("api/query", progress = progress) {
def handle(body: JSON.T): Option[JSON.T] =
for (query <- Parse.query(body)) yield {
val facet = query_facet(db, query)
val blocks = query_blocks(db, query)
- encode.result(Result(blocks, facet))
+ Encode.result(Result(blocks, facet))
}
}))
--- a/src/Tools/Find_Facts/src/solr.scala Fri Feb 14 15:24:42 2025 +0100
+++ b/src/Tools/Find_Facts/src/solr.scala Fri Feb 14 17:40:21 2025 +0100
@@ -11,6 +11,8 @@
import isabelle._
+import java.util.{Properties => JProperties}
+
import scala.jdk.CollectionConverters._
import org.apache.solr.client.solrj.embedded.EmbeddedSolrServer
@@ -346,7 +348,12 @@
class System private[Solr](val solr_data: Path) {
def database_dir(database: String): Path = solr_data + Path.basic(database)
- def init_database(database: String, data: Data, clean: Boolean = false): Database = {
+ def init_database(
+ database: String,
+ data: Data,
+ props: Properties.T = Nil,
+ clean: Boolean = false
+ ): Database = {
val db_dir = database_dir(database)
if (clean) Isabelle_System.rm_tree(db_dir)
@@ -354,6 +361,12 @@
val conf_dir = db_dir + Path.basic("conf")
if (!conf_dir.is_dir) {
Isabelle_System.make_directory(conf_dir)
+
+ val jprops = new JProperties
+ for ((key, value) <- props) jprops.put(key, value)
+ jprops.setProperty("name", database)
+ jprops.store(File.writer((db_dir + Path.basic("core.properties")).file), null)
+
File.write(conf_dir + Path.basic("schema.xml"), XML.string_of_body(data.schema))
File.write(conf_dir + Path.basic("solrconfig.xml"), XML.string_of_body(data.solr_config))
data.more_config.foreach((path, content) => File.write(conf_dir + path, content))
@@ -365,17 +378,23 @@
def open_database(database: String): Database =
if (!database_dir(database).is_dir) error("Missing Solr database: " + quote(database))
else {
+ val jprops = File.read_props(database_dir(database) + Path.basic("core.properties"))
+ val props =
+ (for (key <- jprops.stringPropertyNames().iterator().asScala)
+ yield key -> jprops.getProperty(key)).toList
+
val server = new EmbeddedSolrServer(solr_data.java_path, database)
val cores = server.getCoreContainer.getAllCoreNames.asScala
if (cores.contains(database)) server.getCoreContainer.reload(database)
else server.getCoreContainer.create(database, Map.empty.asJava)
- new Database(server)
+ new Database(props, database_dir(database), server)
}
}
- class Database private[Solr](solr: EmbeddedSolrServer) extends AutoCloseable {
+ class Database private[Solr](val props: Properties.T, val dir: Path, solr: EmbeddedSolrServer)
+ extends AutoCloseable {
override def close(): Unit = solr.close()
def execute_query[A](