--- a/etc/build.props Sat Jan 11 23:19:10 2025 +0100
+++ b/etc/build.props Sat Jan 11 23:24:32 2025 +0100
@@ -250,6 +250,10 @@
src/Pure/term_xml.scala \
src/Pure/thm_name.scala \
src/Pure/update.scala \
+ src/Tools/Find_Facts/src/elm.scala \
+ src/Tools/Find_Facts/src/find_facts.scala \
+ src/Tools/Find_Facts/src/solr.scala \
+ src/Tools/Find_Facts/src/thy_blocks.scala \
src/Tools/Graphview/graph_file.scala \
src/Tools/Graphview/graph_panel.scala \
src/Tools/Graphview/graphview.scala \
--- a/etc/components Sat Jan 11 23:19:10 2025 +0100
+++ b/etc/components Sat Jan 11 23:24:32 2025 +0100
@@ -1,5 +1,6 @@
#built-in components
src/Tools/Demo
+src/Tools/Find_Facts
src/Tools/jEdit
src/Tools/GraphBrowser
src/Tools/Graphview
--- a/src/Pure/System/isabelle_tool.scala Sat Jan 11 23:19:10 2025 +0100
+++ b/src/Pure/System/isabelle_tool.scala Sat Jan 11 23:24:32 2025 +0100
@@ -208,6 +208,9 @@
Component_Zipperposition.isabelle_tool,
Component_Zstd.isabelle_tool,
Components.isabelle_tool,
+ isabelle.find_facts.Find_Facts.isabelle_tool1,
+ isabelle.find_facts.Find_Facts.isabelle_tool2,
+ isabelle.find_facts.Find_Facts.isabelle_tool3,
isabelle.vscode.Component_VSCode.isabelle_tool,
isabelle.vscode.Component_VSCodium.isabelle_tool1,
isabelle.vscode.Component_VSCodium.isabelle_tool2)
--- a/src/Tools/Find_Facts/components/find_facts Sat Jan 11 23:19:10 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-solr-9.6.1
-elm-0.19.1
\ No newline at end of file
--- a/src/Tools/Find_Facts/elm.scala Sat Jan 11 23:19:10 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-/* Author: Fabian Huch, TU Muenchen
-
-Elm module for Isabelle.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-import scala.jdk.CollectionConverters._
-
-import org.jsoup.nodes.Element
-
-
-object Elm {
- private lazy val exec = Path.explode("$ISABELLE_ELM_HOME/elm").expand
-
- object Project {
- def apply(
- name: String,
- dir: Path,
- main: Path = Path.explode("src/Main.elm"),
- output: Path = Path.explode("index.html"),
- head: XML.Body = Nil
- ): Project = {
- if (!dir.is_dir) error("Project directory does not exist: " + dir)
- val main_file = dir + main
- if (!main_file.is_file) error("Main elm file does not exist: " + main_file)
- new Project(name, dir, main, dir + output, head)
- }
- }
-
- class Project private(name: String, dir: Path, main: Path, output: Path, head: XML.Body) {
- val definition = JSON.parse(File.read(dir + Path.basic("elm.json")))
- val src_dirs =
- JSON.strings(definition, "source-directories").getOrElse(
- error("Missing source directories in elm.json"))
-
- def sources: List[JFile] =
- for {
- src_dir <- src_dirs
- path = dir + Path.explode(src_dir)
- file <- File.find_files(path.file, _.getName.endsWith(".elm"))
- } yield file
-
- def sources_shasum: SHA1.Shasum = {
- val meta_info = SHA1.shasum_meta_info(SHA1.digest(JSON.Format(definition)))
- val head_digest = SHA1.shasum(SHA1.digest(XML.string_of_body(head)), "head")
- val source_digest =
- SHA1.shasum_sorted(for (file <- sources) yield SHA1.digest(file) -> file.getCanonicalPath)
- meta_info ::: head_digest ::: source_digest
- }
-
- def get_digest: SHA1.Digest =
- Exn.capture {
- val html = HTML.parse_document(File.read(output))
- val elem = html.head.getElementsByTag("meta").attr("name", "shasum")
- Library.the_single(elem.eachAttr("content").asScala.toList)
- } match {
- case Exn.Res(s) => SHA1.fake_digest(s)
- case _ => SHA1.digest_empty
- }
-
- def build_html(progress: Progress): String = {
- val digest = sources_shasum.digest
- if (digest == get_digest) File.read(output)
- else {
- progress.echo("### Building " + name + " (" + output.canonical.implode + ") ...")
-
- val cmd =
- File.bash_path(exec) + " make " + File.bash_path(main) + " --optimize --output=" + output
- val res = Isabelle_System.bash(cmd, cwd = dir)
-
- if (!res.ok) {
- progress.echo(res.err)
- error("Failed to compile Elm sources")
- }
-
- val file = HTML.parse_document(File.read(output))
- file.head.appendChild(
- Element("meta").attr("name", "shasum").attr("content", digest.toString))
- file.head.append(XML.string_of_body(head))
- val html = file.html
- File.write(output, html)
-
- html
- }
- }
- }
-}
\ No newline at end of file
--- a/src/Tools/Find_Facts/etc/build.props Sat Jan 11 23:19:10 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-title = Find Facts
-module = $FIND_FACTS_HOME/lib/find-facts.jar
-requirements = \
- env:ISABELLE_SCALA_JAR \
- env:SOLR_JARS
-sources = \
- component_elm.scala \
- component_solr.scala \
- elm.scala \
- find_facts.scala \
- find_facts_tools.scala \
- solr.scala \
- thy_blocks.scala
-services = \
- isabelle.Find_Facts_Tools
\ No newline at end of file
--- a/src/Tools/Find_Facts/etc/settings Sat Jan 11 23:19:10 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings Sat Jan 11 23:24:32 2025 +0100
@@ -1,3 +1,3 @@
-FIND_FACTS_HOME="$COMPONENT"
+# -*- shell-script -*- :mode=shellscript:
-init_components "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}" "$FIND_FACTS_HOME/components/find_facts"
\ No newline at end of file
+FIND_FACTS_HOME="$COMPONENT"
--- a/src/Tools/Find_Facts/find_facts.scala Sat Jan 11 23:19:10 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,949 +0,0 @@
-/* Title: Tools/Find_Facts.scala
- Author: Fabian Huch, TU Muenchen
-
-Full-text search engine for Isabelle (including web server), using Solr as backend.
-*/
-package isabelle
-
-
-import scala.annotation.tailrec
-import scala.collection.immutable.TreeMap
-import scala.collection.mutable
-
-
-object Find_Facts {
- /** blocks **/
-
- object Kind {
- val CONST = "constant"
- val TYPE = "type"
- val THM = "fact"
- }
-
- case class Block(
- id: String,
- version: Long,
- chapter: String,
- session: String,
- theory: String,
- file: String,
- url_path: Path,
- command: String,
- start_line: Int,
- src_before: String,
- src: String,
- src_after: String,
- xml: XML.Body,
- html: String,
- entity_kname: Option[String],
- consts: List[String],
- typs: List[String],
- thms: List[String]
- ) {
- def path = Path.explode(file)
- def file_type: String = path.get_ext
- def file_name: String = path.file_name
-
- def kinds: List[String] =
- (if (typs.nonEmpty) List(Kind.TYPE) else Nil) :::
- (if (consts.nonEmpty) List(Kind.CONST) else Nil) :::
- (if (thms.nonEmpty) List(Kind.THM) else Nil)
- def names: List[String] = (typs ::: consts ::: thms).distinct
- }
-
- case class Blocks(num_found: Long, blocks: List[Block], cursor: String)
-
-
- /** queries */
-
- enum Atom {
- case Exact(s: String) extends Atom
- case Value(s: String) extends Atom
- }
-
- enum Field {
- case chapter, session, file_type, theory, command, source, names, consts, typs, thms, kinds
- }
-
- sealed trait Filter
- case class Field_Filter(field: Field, either: List[Atom]) extends Filter
- case class Any_Filter(either: List[Atom]) extends Filter {
- def fields: List[Field] = List(Field.session, Field.theory, Field.source, Field.names)
- }
-
- case class Select(field: Field, values: List[String])
-
- object Query {
- def apply(filters: Filter*): Query = new Query(filters.toList)
- }
-
- case class Query(
- filters: List[Filter] = Nil,
- exclude: List[Filter] = Nil,
- selects: List[Select] = Nil)
-
-
- /* stats and facets */
-
- case class Stats(
- results: Long,
- sessions: Long,
- theories: Long,
- commands: Long,
- consts: Long,
- typs: Long,
- thms: Long)
-
- case class Facets(
- chapter: Map[String, Long],
- session: Map[String, Long],
- theory: Map[String, Long],
- file_type: Map[String, Long],
- command: Map[String, Long],
- kinds: Map[String, Long],
- consts: Map[String, Long],
- typs: Map[String, Long],
- thms: Map[String, Long])
-
-
- /** Solr data model **/
-
- object private_data extends Solr.Data("find_facts") {
- /* types */
-
- val symbol_codes =
- for {
- entry <- Symbol.symbols.entries
- code <- entry.decode.toList
- input <- entry.symbol :: entry.abbrevs
- } yield input -> code
-
- val replacements =
- for ((symbol, codes) <- symbol_codes.groupMap(_._1)(_._2).toList if codes.length == 1)
- yield symbol -> Library.the_single(codes)
-
- val Special_Char = """(.*[(){}\[\].,:"].*)""".r
- val Arrow = """(.*=>.*)""".r
-
- val synonyms =
- for {
- (symbol, code) <- symbol_codes
- if !Special_Char.matches(symbol) && !Arrow.matches(symbol)
- } yield symbol + " => " + code
-
- override lazy val more_config = Map(Path.basic("synonyms.txt") -> synonyms.mkString("\n"))
-
- object Types {
- private val strip_html = Solr.Class("charFilter", "HTMLStripCharFilterFactory")
- private val replace_symbol_chars =
- replacements.collect {
- case (Special_Char(pattern), code) =>
- Solr.Class(
- "charFilter", "PatternReplaceCharFilterFactory",
- List("pattern" -> ("\\Q" + pattern + "\\E"), "replacement" -> code))
- }
-
- private val symbol_pattern =
- """\s*(::|[(){}\[\].,:"]|[^\p{ASCII}]|((?![^\p{ASCII}])[^(){}\[\].,:"\s])+)\s*""".r
-
- private val tokenize =
- Solr.Class("tokenizer", "WhitespaceTokenizerFactory", List("rule" -> "java"))
- private val tokenize_symbols =
- Solr.Class("tokenizer", "PatternTokenizerFactory",
- List("pattern" -> symbol_pattern.toString, "group" -> "1"))
-
- private val to_lower = Solr.Class("filter", "LowerCaseFilterFactory")
- private val add_ascii =
- Solr.Class("filter", "ASCIIFoldingFilterFactory", List("preserveOriginal" -> "true"))
- private val delimit_words =
- Solr.Class("filter", "WordDelimiterGraphFilterFactory", List(
- "splitOnCaseChange" -> "0", "stemEnglishPossessive" -> "0", "preserveOriginal" -> "1"))
- private val flatten = Solr.Class("filter", "FlattenGraphFilterFactory")
- private val replace_symbols =
- Solr.Class("filter", "SynonymGraphFilterFactory", List("synonyms" -> "synonyms.txt"))
- private val replace_special_symbols =
- replacements.collect {
- case (Arrow(arrow), code) =>
- Solr.Class("filter", "PatternReplaceFilterFactory",
- List("pattern" -> ("\\Q" + arrow + "\\E"), "replacement" -> code))
- }
-
- val source =
- Solr.Type("name", "TextField", Nil, List(
- XML.Elem(Markup("analyzer", List("type" -> "index")),
- List(strip_html, tokenize_symbols, to_lower, add_ascii, delimit_words, flatten)),
- XML.Elem(
- Markup("analyzer", List("type" -> "query")),
- replace_symbol_chars ::: tokenize_symbols :: replace_symbols ::
- replace_special_symbols ::: to_lower :: Nil)))
-
- val name =
- Solr.Type("source", "TextField", Nil, List(
- XML.Elem(Markup("analyzer", List("type" -> "index")),
- List(tokenize, to_lower, delimit_words, flatten)),
- XML.Elem(Markup("analyzer", List("type" -> "query")), List(tokenize, to_lower))))
-
- val text = Solr.Type("text", "TextField")
- }
-
-
- /* fields */
-
- object Fields {
- val id = Solr.Field("id", Solr.Type.string).make_unique_key
- val version = Solr.Field("version", Solr.Type.long, Solr.Column_Wise(true))
- val chapter = Solr.Field("chapter", Solr.Type.string, Solr.Column_Wise(true))
- val session = Solr.Field("session", Types.name)
- val session_facet = Solr.Field("session_facet", Solr.Type.string, Solr.Stored(false))
- val theory = Solr.Field("theory", Types.name)
- val theory_facet = Solr.Field("theory_facet", Solr.Type.string, Solr.Stored(false))
- val file = Solr.Field("file", Solr.Type.string, Solr.Indexed(false))
- val file_type =
- Solr.Field("file_type", Solr.Type.string, Solr.Column_Wise(true) ::: Solr.Stored(false))
- val url_path = Solr.Field("url_path", Solr.Type.string, Solr.Indexed(false))
- val command = Solr.Field("command", Solr.Type.string, Solr.Column_Wise(true))
- val start_line = Solr.Field("start_line", Solr.Type.int, Solr.Column_Wise(true))
- val src_before = Solr.Field("src_before", Solr.Type.string, Solr.Indexed(false))
- val src_after = Solr.Field("src_after", Solr.Type.string, Solr.Indexed(false))
- val src = Solr.Field("src", Types.source)
- val xml = Solr.Field("xml", Solr.Type.bytes, Solr.Indexed(false))
- val html = Solr.Field("html", Solr.Type.bytes, Solr.Indexed(false))
- val entity_kname = Solr.Field("entity_kname", Solr.Type.string, Solr.Indexed(false))
- val consts = Solr.Field("consts", Types.name, Solr.Multi_Valued(true))
- val consts_facet =
- Solr.Field("consts_facet", Solr.Type.string, Solr.Multi_Valued(true) ::: Solr.Stored(false))
- val typs = Solr.Field("typs", Types.name, Solr.Multi_Valued(true))
- val typs_facet =
- Solr.Field("typs_facet", Solr.Type.string, Solr.Multi_Valued(true) ::: Solr.Stored(false))
- val thms = Solr.Field("thms", Types.name, Solr.Multi_Valued(true))
- val thms_facet =
- Solr.Field("thms_facet", Solr.Type.string, Solr.Multi_Valued(true) ::: Solr.Stored(false))
- val names = Solr.Field("names", Types.name, Solr.Multi_Valued(true) ::: Solr.Stored(false))
- val kinds =
- Solr.Field("kinds", Solr.Type.string,
- Solr.Multi_Valued(true) ::: Solr.Column_Wise(true) ::: Solr.Stored(false))
- }
-
- lazy val fields: Solr.Fields = Solr.Fields(
- Fields.id, Fields.version, Fields.chapter, Fields.session, Fields.session_facet,
- Fields.theory, Fields.theory_facet, Fields.file, Fields.file_type, Fields.url_path,
- Fields.command, Fields.start_line, Fields.src_before, Fields.src_after, Fields.src,
- Fields.xml, Fields.html, Fields.entity_kname, Fields.consts, Fields.consts_facet, Fields.typs,
- Fields.typs_facet, Fields.thms, Fields.thms_facet, Fields.names, Fields.kinds)
-
-
- /* operations */
-
- def read_domain(db: Solr.Database, q: Solr.Source): Set[String] =
- db.execute_query(Fields.id, List(Fields.id), None, 100000,
- { results =>
- results.map(_.string(Fields.id)).toSet
- }, q = q)
-
- def read_block(res: Solr.Result): Block = {
- val id = res.string(Fields.id)
- val version = res.long(Fields.version)
- val chapter = res.string(Fields.chapter)
- val session = res.string(Fields.session)
- val theory = res.string(Fields.theory)
- val file = res.string(Fields.file)
- val url_path = Path.explode(res.string(Fields.url_path))
- val command = res.string(Fields.command)
- val start_line = res.int(Fields.start_line)
- val src_before = res.string(Fields.src_before)
- val src = res.string(Fields.src)
- val src_after = res.string(Fields.src_after)
- val xml = YXML.parse_body(res.bytes(Fields.xml))
- val html = res.bytes(Fields.html).text
- val entity_kname = res.get_string(Fields.entity_kname)
- val consts = res.list_string(Fields.consts)
- val typs = res.list_string(Fields.typs)
- val thms = res.list_string(Fields.thms)
-
- Block(id = id, version = version, chapter = chapter, session = session, theory = theory,
- file = file, url_path = url_path, command = command, start_line = start_line, src_before =
- src_before, src = src, src_after = src_after, xml = xml, html = html, entity_kname =
- entity_kname, consts = consts, typs = typs, thms = thms)
- }
-
- def read_blocks(
- db: Solr.Database,
- q: Solr.Source,
- fq: List[Solr.Source],
- cursor: Option[String] = None,
- max_results: Int = 10
- ): Blocks =
- db.execute_query(Fields.id, stored_fields, cursor, max_results,
- { results =>
- val next_cursor = results.next_cursor
- val blocks = results.map(read_block).toList
- Blocks(results.num_found, blocks, next_cursor)
- }, q = q, fq = fq, more_chunks = 0)
-
- def stream_blocks(
- db: Solr.Database,
- q: Solr.Source,
- stream: Iterator[Block] => Unit,
- cursor: Option[String] = None,
- ): Unit =
- db.execute_query(Fields.id, stored_fields, cursor, 10000,
- { results =>
- stream(results.map(read_block))
- }, q = q)
-
- def update_theory(db: Solr.Database, theory_name: String, blocks: List[Block]): Unit =
- db.transaction {
- val delete =
- read_domain(db, Solr.filter(Fields.theory, Solr.phrase(theory_name))) -- blocks.map(_.id)
-
- if (delete.nonEmpty) db.execute_batch_delete(delete.toList)
-
- db.execute_batch_insert(
- for (block <- blocks) yield { (doc: Solr.Document) =>
- doc.string(Fields.id) = block.id
- doc.long(Fields.version) = block.version
- doc.string(Fields.chapter) = block.chapter
- doc.string(Fields.session) = block.session
- doc.string(Fields.session_facet) = block.session
- doc.string(Fields.theory) = block.theory
- doc.string(Fields.theory_facet) = block.theory
- doc.string(Fields.file) = block.file
- doc.string(Fields.file_type) = block.file_type
- doc.string(Fields.url_path) = block.url_path.implode
- doc.string(Fields.command) = block.command
- doc.int(Fields.start_line) = block.start_line
- doc.string(Fields.src_before) = block.src_before
- doc.string(Fields.src) = block.src
- doc.string(Fields.src_after) = block.src_after
- doc.bytes(Fields.xml) = YXML.bytes_of_body(block.xml)
- doc.bytes(Fields.html) = Bytes(block.html)
- doc.string(Fields.entity_kname) = block.entity_kname
- doc.string(Fields.consts) = block.consts
- doc.string(Fields.consts_facet) = block.consts
- doc.string(Fields.typs) = block.typs
- doc.string(Fields.typs_facet) = block.typs
- doc.string(Fields.thms) = block.thms
- doc.string(Fields.thms_facet) = block.thms
- doc.string(Fields.names) = block.names
- doc.string(Fields.kinds) = block.kinds
- })
- }
-
- def read_theory(db: Solr.Database, theory_name: String): List[Block] = {
- val blocks = new mutable.ListBuffer[Block]
- stream_blocks(db, Solr.filter(Fields.theory_facet, Solr.phrase(theory_name)), {
- res => blocks ++= res
- })
- blocks.toList
- }
-
- def delete_session(db: Solr.Database, session_name: String): Unit =
- db.transaction {
- val delete = read_domain(db, Solr.filter(Fields.session, Solr.phrase(session_name)))
- if (delete.nonEmpty) db.execute_batch_delete(delete.toList)
- }
-
- def query_stats(db: Solr.Database, q: Solr.Source, fq: List[Solr.Source]): Stats =
- db.execute_stats_query(
- List(Fields.session_facet, Fields.theory_facet, Fields.command, Fields.consts_facet,
- Fields.typs_facet, Fields.thms_facet, Fields.start_line),
- { res =>
- val results = res.count
- val sessions = res.count(Fields.session_facet)
- val theories = res.count(Fields.theory_facet)
- val commands = res.count(Fields.theory_facet)
- val consts = res.count(Fields.consts_facet)
- val typs = res.count(Fields.typs_facet)
- val thms = res.count(Fields.thms_facet)
-
- Stats(results, sessions, theories, commands, consts, typs, thms)
- }, q = q, fq = fq)
-
- def query_facets(
- db: Solr.Database,
- q: Solr.Source,
- fq: List[Solr.Source],
- max_terms: Int = 100
- ): Facets =
- db.execute_facet_query(
- List(Fields.chapter, Fields.session_facet, Fields.theory_facet, Fields.file_type,
- Fields.command, Fields.kinds, Fields.consts_facet, Fields.typs_facet, Fields.thms_facet),
- { res =>
- val chapter = res.string(Fields.chapter)
- val sessions = res.string(Fields.session_facet)
- val theories = res.string(Fields.theory_facet)
- val file_types = res.string(Fields.file_type)
- val commands = res.string(Fields.command)
- val kinds = res.string(Fields.kinds)
- val consts = res.string(Fields.consts_facet)
- val typs = res.string(Fields.typs_facet)
- val thms = res.string(Fields.thms_facet)
-
- Facets(chapter, sessions, theories, file_types, commands, kinds, consts, typs, thms)
- }, q = q, fq = fq, max_terms = max_terms)
-
-
- /* queries */
-
- def solr_field(field: Field, select: Boolean = false): Solr.Field =
- field match {
- case Field.chapter => Fields.chapter
- case Field.session if select => Fields.session_facet
- case Field.session => Fields.session
- case Field.theory if select => Fields.theory_facet
- case Field.theory => Fields.theory
- case Field.file_type => Fields.file_type
- case Field.command => Fields.command
- case Field.source => Fields.src
- case Field.names => Fields.names
- case Field.consts if select => Fields.consts_facet
- case Field.consts => Fields.consts
- case Field.typs if select => Fields.typs_facet
- case Field.typs => Fields.typs
- case Field.thms if select => Fields.thms_facet
- case Field.thms => Fields.thms
- case Field.kinds => Fields.kinds
- }
-
- def solr_query(query: Query): (Solr.Source, List[Solr.Source]) = {
- def solr_atom(atom: Atom): List[Solr.Source] =
- atom match {
- case Atom.Value(s) if s.isEmpty => Nil
- case Atom.Value(s) if !s.exists(Solr.wildcard_char(_)) => List(Solr.term(s))
- case Atom.Value(s) =>
- val terms = s.split("\\s+").toList.filterNot(_.isBlank)
- if (terms.isEmpty) Nil else terms.map(Solr.wildcard)
- case Atom.Exact(s) => List(Solr.phrase(s))
- }
-
- def solr_atoms(field: Field, atoms: List[Atom]): List[Solr.Source] =
- for {
- atom <- atoms
- source <- solr_atom(atom)
- } yield Solr.filter(solr_field(field), source)
-
- def solr_filter(filter: Filter): List[Solr.Source] =
- filter match {
- case Field_Filter(field, atoms) => solr_atoms(field, atoms)
- case any@Any_Filter(atoms) => any.fields.flatMap(solr_atoms(_, atoms))
- }
-
- def solr_select(select: Select): Solr.Source = {
- val field = solr_field(select.field, select = true)
- Solr.tag(field.name, Solr.filter(field, Solr.OR(select.values.map(Solr.phrase))))
- }
-
- val filter = query.filters.map(filter => Solr.OR(solr_filter(filter)))
- val exclude = query.exclude.flatMap(solr_filter).map(Solr.exclude)
- val selects = query.selects.map(solr_select)
-
- (Solr.AND(filter ::: exclude), selects)
- }
- }
-
- 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
- }
-
- def query_blocks(db: Solr.Database, query: Query, cursor: Option[String] = None): Blocks = {
- val (q, fq) = Find_Facts.private_data.solr_query(query)
- Find_Facts.private_data.read_blocks(db, q, fq, cursor = cursor)
- }
-
- def query_stats(db: Solr.Database, query: Query): Stats = {
- val (q, fq) = Find_Facts.private_data.solr_query(query)
- Find_Facts.private_data.query_stats(db, q, fq)
- }
-
- def query_facet(db: Solr.Database, query: Query): Facets = {
- val (q, fq) = Find_Facts.private_data.solr_query(query)
- Find_Facts.private_data.query_facets(db, q, fq)
- }
-
-
- /** indexing **/
-
- def make_thy_blocks(
- options: Options,
- session: Session,
- browser_info_context: Browser_Info.Context,
- document_info: Document_Info,
- theory_context: Export.Theory_Context,
- snapshot: Document.Snapshot,
- chapter: String
- ): List[Block] = {
- val theory = theory_context.theory
- val entities = Export_Theory.read_theory(theory_context).entity_iterator.toList
- val session_name = theory_context.session_context.session_name
-
- 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)
-
- def make_node_blocks(
- snapshot: Document.Snapshot,
- command_ranges: List[(String, Text.Range)]
- ): 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 elements =
- Browser_Info.Elements(html = Browser_Info.default_elements.html - Markup.ENTITY)
- val node_context = Browser_Info.Node_Context.empty
-
- val content = XML.content(snapshot.xml_markup(elements = Markup.Elements.empty))
- def get_content(range: Text.Range): String =
- Symbol.decode(Line.normalize(range.substring(content)))
-
- val document = Line.Document(content.replace('\r', '\u001a'))
- val num_lines = document.lines.length
- def content_range(start: Line.Position, stop: Line.Position): Text.Range =
- Text.Range(document.offset(start).get, document.offset(stop).get)
-
- val index = Symbol.Index(content)
- val node_entities =
- TreeMap.from(entities
- .filter(entity => entity.file == snapshot.node_name.node)
- .groupBy(entity => index.decode(entity.range).start))
-
- val rendering = new Rendering(snapshot, options, session)
- val comment_ranges = rendering.comments(Text.Range.full).map(markup => ("", markup.range))
-
- for ((command, range) <- command_ranges ::: comment_ranges) yield {
- val line_range = document.range(range)
- val start_line = line_range.start.line1
-
- val id = file + "|" + range.start + ".." + range.stop
-
- val src_before = get_content(
- content_range(Line.Position((line_range.start.line - 5).max(0)), line_range.start))
- val src = get_content(range)
- val src_after = get_content(
- content_range(line_range.stop, Line.Position((line_range.stop.line + 5).min(num_lines))))
-
- val xml = snapshot.xml_markup(range, elements = elements.html)
- val html =
- HTML.output(node_context.make_html(elements, xml), hidden = true, structural = false)
-
- val entities = node_entities.range(range.start, range.stop).values.toList.flatten.distinct
-
- def get_entities(kind: String): List[String] =
- for {
- entity <- entities
- if entity.export_kind == kind
- if range.contains(index.decode(entity.range))
- } yield entity.name
-
- val entity_kname = entities.sortBy(_.name.length).headOption.map(_.kname)
-
- val typs = get_entities(Export_Theory.Kind.TYPE)
- val consts = get_entities(Export_Theory.Kind.CONST)
- val thms = get_entities(Export_Theory.Kind.THM)
-
- Block(id = id, version = version, chapter = chapter, session = session_name, theory =
- theory, file = file, url_path = url_path, command = command, start_line = start_line,
- src_before = src_before, src = src, src_after = src_after, xml = xml, html = html,
- entity_kname = entity_kname, consts = consts, typs = typs, thms = thms)
- }
- }
-
- def expand_block(block: Thy_Blocks.Block): List[Thy_Blocks.Block] =
- block match {
- case Thy_Blocks.Thy(inner) => inner.flatMap(expand_block)
- case e@Thy_Blocks.Decl(inner) =>
- val inner1 = inner.flatMap(expand_block)
- if (inner.length > 1) e :: inner1 else List(e)
- case _ => List(block)
- }
-
- val thy_command_ranges =
- for (block <- Thy_Blocks.read_blocks(snapshot).flatMap(expand_block))
- yield (block.command, block.range)
-
- make_node_blocks(snapshot, thy_command_ranges) :::
- (for {
- blob_name <- snapshot.node_files.tail
- snapshot1 = snapshot.switch(blob_name)
- if snapshot1.node.source_wellformed
- range = Text.Range.length(snapshot1.node.source)
- block <- make_node_blocks(snapshot1, List(("", range)))
- } yield block)
- }
-
- def find_facts_index(
- options: Options,
- sessions: List[String],
- dirs: List[Path] = Nil,
- clean: Boolean = false,
- progress: Progress = new Progress
- ): Unit = {
- val store = Store(options)
- val database = options.string("find_facts_database_name")
- val session = Session(options, Resources.bootstrap)
-
- val selection = Sessions.Selection(sessions = sessions)
- val session_structure = Sessions.load_structure(options, dirs = dirs).selection(selection)
- val deps = Sessions.Deps.load(session_structure)
- val browser_info_context = Browser_Info.context(session_structure)
-
- if (sessions.isEmpty) progress.echo("Nothing to index")
- else {
- 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 + " ...")
-
- 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("Theory " + name.theory + " ...")
- 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)
- }
- }
- }
- }
-
- Par_List.map(index_session, sessions)
- }
-
- val query = Query(Field_Filter(Field.session, sessions.map(Atom.Exact(_))))
- Find_Facts.query_stats(db, query)
- }
-
- progress.echo("Indexed " + stats.results + " blocks with " +
- stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
- }
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool = Isabelle_Tool("find_facts_index", "index sessions for find_facts",
- Scala_Project.here,
- { args =>
- var clean = false
- val dirs = new mutable.ListBuffer[Path]
- var options = Options.init()
-
- val getopts = Getopts("""
- Usage: isabelle find_facts_index [OPTIONS] [SESSIONS ...]
-
- Options are:
- -c clean previous index
- -d DIR include session directory
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-
- Index sessions for find_facts.
- """,
- "c" -> (_ => clean = true),
- "d:" -> (arg => dirs += Path.explode(arg)),
- "o:" -> (arg => options = options + arg))
-
- val sessions = getopts(args)
-
- val progress = new Console_Progress()
-
- find_facts_index(options, sessions, dirs = dirs.toList, clean = clean, progress = progress)
- })
-
-
- /** index components **/
-
- def find_facts_index_component(
- options: Options,
- target_dir: Path = Path.current,
- progress: Progress = new Progress
- ): Unit = {
- val database = options.string("find_facts_database_name")
-
- val component = "find_facts_index-" + database
- val component_dir =
- Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
-
- Isabelle_System.copy_dir(Solr.database_dir(database), component_dir.path)
- component_dir.write_settings("SOLR_COMPONENTS=\"$SOLR_COMPONENTS:$COMPONENT/" + database + "\"")
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool1 = Isabelle_Tool("find_facts_index_component",
- "build component from find_facts index", Scala_Project.here,
- { args =>
- var options = Options.init()
- var target_dir = Path.current
-
- val getopts = Getopts("""
- Usage: isabelle find_facts_index_component
-
- Options are:
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -D DIR target directory (default ".")
-
- Build component from finalized find_facts index with given name.
- """,
- "o:" -> (arg => options = options + arg),
- "D:" -> (arg => target_dir = Path.explode(arg)))
-
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
-
- find_facts_index_component(options, target_dir = target_dir)
- })
-
-
- /** querying **/
-
- /* requests and parsing */
-
- case class Query_Blocks(query: Query, cursor: String)
-
- object Parse {
- def atom(json: JSON.T): Option[Atom] =
- JSON.string(json, "value").map(Atom.Value(_)) orElse
- JSON.string(json, "exact").map(Atom.Exact(_))
-
- def field(name: String): Option[Field] = Field.values.find(_.toString == name)
-
- def filter(json: JSON.T): Option[Filter] =
- for {
- atoms <- JSON.list(json, "either", atom)
- filter <-
- JSON.string(json, "field") match {
- case None => Some(Any_Filter(atoms))
- case Some(name) => for (field <- field(name)) yield Field_Filter(field, atoms)
- }
- } yield filter
-
- def select(json: JSON.T): Option[Select] =
- for {
- name <- JSON.string(json, "field")
- field <- field(name)
- values <- JSON.strings(json, "values")
- } yield Select(field, values)
-
- def query(json: JSON.T): Option[Query] =
- for {
- filters <- JSON.list(json, "filters", filter)
- exclude <- JSON.list(json, "exclude", filter)
- selects <- JSON.list(json, "selects", select)
- } yield Query(filters, exclude, selects)
-
- def query_blocks(json: JSON.T): Option[Query_Blocks] =
- for {
- query <- JSON.value(json, "query", query)
- cursor <- JSON.string(json, "cursor")
- } yield Query_Blocks(query, cursor)
-
- def query_block(json: JSON.T): Option[String] = for (id <- JSON.string(json, "id")) yield id
- }
-
-
- /* responses and encoding */
-
- case class Result(blocks: Blocks, facets: Facets)
-
- class Encode(options: Options) {
- val library_base_url = Url(options.string("browser_info_url_library"))
- val afp_base_url = Url(options.string("browser_info_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)
- }
-
- def block(block: Block): JSON.T =
- JSON.Object(
- "id" -> block.id,
- "chapter" -> block.chapter,
- "session" -> block.session,
- "theory" -> block.theory,
- "file" -> block.file,
- "file_name" -> block.file_name,
- "url" -> url(block).toString,
- "command" -> block.command,
- "start_line" -> block.start_line,
- "src_before" -> block.src_before,
- "src_after" -> block.src_after,
- "html" -> block.html,
- "entity_kname" -> block.entity_kname.orNull)
-
- def blocks(blocks: Blocks): JSON.T =
- JSON.Object(
- "num_found" -> blocks.num_found,
- "blocks" -> blocks.blocks.map(block),
- "cursor" -> blocks.cursor)
-
- def facets(facet: Facets): JSON.T =
- JSON.Object(
- "chapter" -> facet.chapter,
- "session" -> facet.session,
- "file_type" -> facet.file_type,
- "theory" -> facet.theory,
- "command" -> facet.command,
- "kinds" -> facet.kinds,
- "consts" -> facet.consts,
- "typs" -> facet.typs,
- "thms" -> facet.thms)
-
- def result(result: Result): JSON.T =
- JSON.Object(
- "blocks" -> blocks(result.blocks),
- "facets" -> facets(result.facets))
- }
-
-
- /* find facts */
-
- abstract class REST_Service(path: Path, progress: Progress, method: String = "POST")
- extends HTTP.Service(path.implode, method = method) {
- def handle(body: JSON.T): Option[JSON.T]
-
- def apply(request: HTTP.Request): Option[HTTP.Response] =
- try {
- for {
- json <-
- Exn.capture(JSON.parse(request.input.text)) match {
- case Exn.Res(json) => Some(json)
- case _ =>
- progress.echo("Could not parse: " + quote(request.input.text), verbose = true)
- None
- }
- res <-
- handle(json) match {
- case Some(res) => Some(res)
- case None =>
- progress.echo("Invalid request: " + JSON.Format(json), verbose = true)
- None
- }
- } yield HTTP.Response(Bytes(JSON.Format(res)), content_type = "application/json")
- }
- catch { case exn: Throwable =>
- val uuid = UUID.random()
- progress.echo_error_message("Server error <" + uuid + ">: " + exn)
- Some(HTTP.Response.text("internal server error: " + uuid))
- }
- }
-
- def find_facts(
- options: Options,
- port: Int,
- devel: Boolean = false,
- progress: Progress = new Progress
- ): Unit = {
- val database = options.string("find_facts_database_name")
- val encode = new Encode(options)
- val logo = Bytes.read(Path.explode("$FIND_FACTS_HOME/web/favicon.ico"))
-
- val isabelle_style = HTML.fonts_css("/fonts/" + _) + "\n\n" + File.read(HTML.isabelle_css)
-
- val project = Elm.Project("Find_Facts", Path.explode("$FIND_FACTS_HOME/web"), head = List(
- HTML.style("html,body {width: 100%, height: 100%}"),
- Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text),
- HTML.style_file("isabelle.css"),
- HTML.style_file("https://fonts.googleapis.com/css?family=Roboto:300,400,500|Material+Icons"),
- HTML.style_file(
- "https://unpkg.com/material-components-web-elm@9.1.0/dist/material-components-web-elm.min.css"),
- HTML.script_file(
- "https://unpkg.com/material-components-web-elm@9.1.0/dist/material-components-web-elm.min.js")))
-
- val frontend = project.build_html(progress)
-
- using(Solr.open_database(database)) { db =>
- val stats = Find_Facts.query_stats(db, Query(Nil))
- progress.echo("Started find facts with " + stats.results + " blocks, " +
- stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
-
- val server =
- HTTP.server(port, name = "", services = List(
- HTTP.Fonts_Service,
- new HTTP.Service("isabelle.css") {
- def apply(request: HTTP.Request): Option[HTTP.Response] =
- Some(HTTP.Response(Bytes(isabelle_style), "text/css"))
- },
- new HTTP.Service("app") {
- def apply(request: HTTP.Request): Option[HTTP.Response] =
- Some(HTTP.Response.html(if (devel) project.build_html(progress) else frontend))
- },
- new REST_Service(Path.explode("api/block"), progress) {
- def handle(body: JSON.T): Option[JSON.T] =
- for {
- request <- Parse.query_block(body)
- block <- query_block(db, request)
- } yield encode.block(block)
- },
- new REST_Service(Path.explode("api/blocks"), 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)))
- },
- new REST_Service(Path.explode("api/query"), 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))
- }
- }))
-
- server.start()
- progress.echo("Server started on port " + server.http_server.getAddress.getPort)
-
- @tailrec
- def loop(): Unit = {
- Thread.sleep(Long.MaxValue)
- loop()
- }
-
- Isabelle_Thread.interrupt_handler(_ => server.stop()) { loop() }
- }
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool2 = Isabelle_Tool("find_facts", "run find_facts server", Scala_Project.here,
- { args =>
- var devel = false
- var options = Options.init()
- var port = 8080
- var verbose = false
-
- val getopts = Getopts("""
-Usage: isabelle find_facts [OPTIONS]
-
- Options are:
- -d devel mode
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -p PORT explicit web server port
- -v verbose server
-
- Run the find_facts web service.
-""",
- "d" -> (_ => devel = true),
- "o:" -> (arg => options = options + arg),
- "p:" -> (arg => port = Value.Int.parse(arg)),
- "v" -> (_ => verbose = true))
-
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
-
- val progress = new Console_Progress(verbose = verbose)
-
- find_facts(options, port, devel = devel, progress = progress)
- })
-}
--- a/src/Tools/Find_Facts/find_facts_tools.scala Sat Jan 11 23:19:10 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-package isabelle
-
-class Find_Facts_Tools extends Isabelle_Scala_Tools(
- Find_Facts.isabelle_tool,
- Find_Facts.isabelle_tool1,
- Find_Facts.isabelle_tool2)
--- a/src/Tools/Find_Facts/solr.scala Sat Jan 11 23:19:10 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,453 +0,0 @@
-/* Author: Fabian Huch, TU Muenchen
-
-Support for full-text search via Solr. See also: https://solr.apache.org/
-*/
-
-package isabelle
-
-
-import scala.jdk.CollectionConverters.*
-
-import org.apache.solr.client.solrj.embedded.EmbeddedSolrServer
-import org.apache.solr.client.solrj.request.json.{JsonQueryRequest, TermsFacetMap, DomainMap}
-import org.apache.solr.client.solrj.response.json.{BucketJsonFacet, NestableJsonFacet}
-import org.apache.solr.client.solrj.response.QueryResponse
-import org.apache.solr.client.solrj.SolrQuery
-import org.apache.solr.common.params.CursorMarkParams
-import org.apache.solr.common.{SolrDocument, SolrInputDocument}
-
-
-object Solr {
- def init(solr_home: Path): Path = {
- File.write(Isabelle_System.make_directory(solr_home) + Path.basic("solr.xml"), "<solr/>")
-
- for (entry <- space_explode(':', Isabelle_System.getenv("SOLR_COMPONENTS")) if entry.nonEmpty)
- Isabelle_System.symlink(Path.explode(entry).absolute, solr_home, force = true)
-
- java.util.logging.LogManager.getLogManager.reset()
- solr_home
- }
-
- lazy val solr_home = init(Path.explode("$ISABELLE_HOME_USER/solr"))
-
-
- /** query language */
-
- val wildcard_char = Set('*', '?')
- val special =
- Set("+", "-", "&&", "||", "!", "(", ")", "{", "}", "[", "]", "^", "\"", "~", "*", "?", ":", "/")
-
- type Source = String
-
- val all: Source = "*"
-
- def enclose(s: Source): Source = "(" + s + ")"
-
- def escape(s: String, seqs: Set[String]): Source =
- seqs.foldLeft(s.replace("\\", "\\\\"))((s, seq) => s.replace(seq, "\\" + seq))
-
- def term(b: Boolean): Source = b.toString
- def term(i: Int): Source = i.toString
- def term(s: String): Source =
- "(\\s+)".r.replaceAllIn(escape(s, special), ws => "\\\\" + ws.matched)
-
- def range(from: Int, to: Int): Source = "[" + from + " TO " + to + "]"
- def phrase(s: String): Source = quote(escape(s, special))
- def wildcard(s: String): Source =
- if (!s.toList.exists(Symbol.is_ascii_blank)) escape(s, special -- wildcard_char.map(_.toString))
- else error("Invalid whitespace character in wildcard: " + quote(s))
-
- def filter(field: Field, x: Source): Source = field.name + ":" + x
-
- def infix(op: Source, args: Iterable[Source]): Source = {
- val body = args.iterator.filterNot(_.isBlank).mkString(" " + op + " ")
- if_proper(body, enclose(body))
- }
-
- def AND(args: Iterable[Source]): Source = infix("AND", args)
- def OR(args: Iterable[Source]): Source = infix("OR", args)
-
- def and(args: Source*): Source = AND(args)
- def or(args: Source*): Source = OR(args)
-
- def exclude(arg: Source): Source = if_proper(arg, "-" + arg)
-
- val query_all: Source = "*:" + all
-
- def tag(name: String, arg: Source): Source = "{!tag=" + name + "}" + arg
-
-
- /** solr schema **/
-
- object Class {
- def apply(
- markup: String,
- name: String,
- props: Properties.T = Nil,
- body: XML.Body = Nil
- ): XML.Elem = XML.Elem(Markup(markup, ("class" -> ("solr." + name)) :: props), body)
- }
-
-
- /* properties */
-
- val Indexed = new Properties.Boolean("indexed")
- val Stored = new Properties.Boolean("stored")
- val Column_Wise = new Properties.Boolean("docValues")
- val Multi_Valued = new Properties.Boolean("multiValued")
-
-
- /* types */
-
- object Type {
- val bool = Type("bool", "BoolField")
- val int = Type("int", "IntPointField")
- val long = Type("long", "LongPointField")
- val double = Type("double", "DoublePointField")
- val string = Type("string", "StrField")
- val bytes = Type("bytes", "BinaryField")
- val date = Type("date", "DatePointField")
- }
-
- case class Type(name: String, cls: String, props: Properties.T = Nil, body: XML.Body = Nil) {
- def defn: XML.Elem = Class("fieldType", cls, Markup.Name(name) ::: props, body)
- }
-
-
- /* fields */
-
- sealed case class Field(
- name: String,
- T: Type,
- props: Properties.T = Nil,
- unique_key: Boolean = false
- ) {
- def make_unique_key: Field = copy(unique_key = true)
- def defn: XML.Elem = XML.elem(Markup("field", ("name" -> name) :: ("type" -> T.name) :: props))
- }
-
- object Fields {
- def list(list: List[Field]): Fields = new Fields(list)
- def apply(args: Field*): Fields = list(args.toList)
- }
-
- final class Fields private(val list: List[Field]) extends Iterable[Field] {
- override def toString: String = list.mkString("Solr.Fields(", ", ", ")")
- def iterator: Iterator[Field] = list.iterator
- }
-
-
- /* data */
-
- abstract class Data(val name: String) {
- def fields: Fields
- def more_config: Map[Path, String] = Map.empty
-
- def stored_fields: List[Field] =
- fields.toList.filter(_.props match {
- case Stored(false) => false
- case _ => true
- })
-
- def unique_key: Field = Library.the_single(fields.filter(_.unique_key).toList)
-
- def solr_config: XML.Body = List(XML.elem("config", List(
- Class("schemaFactory", "ClassicIndexSchemaFactory"),
- XML.elem("luceneMatchVersion", XML.string(Isabelle_System.getenv("SOLR_LUCENE_VERSION"))),
- Class("updateHandler", "DirectUpdateHandler2", body = List(
- XML.elem("autoCommit", List(
- XML.elem("maxDocs", XML.string("-1")),
- XML.elem("maxTime", XML.string("-1")),
- XML.elem("maxSize", XML.string("-1")))))),
- Class("requestHandler", "SearchHandler", Markup.Name("/select")))))
-
- def schema: XML.Body =
- List(XML.Elem(Markup("schema",
- List(
- "name" -> "isabelle",
- "version" -> Isabelle_System.getenv("SOLR_SCHEMA_VERSION"))),
- List(
- XML.elem("uniqueKey", XML.string(unique_key.name)),
- XML.elem("fields", fields.toList.map(_.defn)),
- XML.elem("types", fields.map(_.T).toList.distinct.map(_.defn)))))
- }
-
-
- /** solr operations */
-
- /* documents */
-
- object Document {
- def empty: Document = new Document(new SolrInputDocument())
- }
-
- class Document private[Solr](val rep: SolrInputDocument) {
- private def obj[A](a: A): Object = a.asInstanceOf[Object]
- private def set[A](field: Field, x: A, f: A => Object = obj): Unit =
- rep.addField(field.name, f(x))
- private def set_option[A](field: Field, x: Option[A], f: A => Object = obj): Unit =
- rep.addField(field.name, x.map(f).orNull)
- private def set_list[A](field: Field, x: List[A], f: A => Object = obj): Unit =
- rep.addField(field.name, x.map(f).toArray)
-
- object bool {
- def update(field: Field, x: Boolean): Unit = set(field, x)
- def update(field: Field, x: Option[Boolean]): Unit = set_option(field, x)
- def update(field: Field, x: List[Boolean]): Unit = set_list(field, x)
- }
- object int {
- def update(field: Field, x: Int): Unit = set(field, x)
- def update(field: Field, x: Option[Int]): Unit = set_option(field, x)
- def update(field: Field, x: List[Int]): Unit = set_list(field, x)
- }
- object long {
- def update(field: Field, x: Long): Unit = set(field, x)
- def update(field: Field, x: Option[Long]): Unit = set_option(field, x)
- def update(field: Field, x: List[Long]): Unit = set_list(field, x)
- }
- object double {
- def update(field: Field, x: Double): Unit = set(field, x)
- def update(field: Field, x: Option[Double]): Unit = set_option(field, x)
- def update(field: Field, x: List[Double]): Unit = set_list(field, x)
- }
- object string {
- def update(field: Field, x: String): Unit = set(field, x)
- def update(field: Field, x: Option[String]): Unit = set_option(field, x)
- def update(field: Field, x: List[String]): Unit = set_list(field, x)
- }
- object bytes {
- private def value(bytes: Bytes): Array[Byte] =
- if (bytes.size > Int.MaxValue) throw new IllegalArgumentException else bytes.make_array
- def update(field: Field, x: Bytes): Unit = set(field, x, value)
- def update(field: Field, x: Option[Bytes]): Unit = set_option(field, x, value)
- def update(field: Field, x: List[Bytes]): Unit = set_list(field, x, value)
- }
- object date {
- private def value(date: Date): java.util.Date = java.util.Date.from(date.rep.toInstant)
- def update(field: Field, x: Date): Unit = set(field, x, value)
- def update(field: Field, x: Option[Date]): Unit = set_option(field, x, value)
- def update(field: Field, x: List[Date]): Unit = set_list(field, x, value)
- }
- }
-
-
- /* results */
-
- class Result private[Solr](rep: SolrDocument) {
- private def single[A](field: Field, f: Object => A): A = {
- val obj = rep.getFieldValue(field.name)
- if (obj == null) error("No such field: " + field.name) else f(obj)
- }
- private def get[A](field: Field, f: Object => A): Option[A] = {
- val obj = rep.getFieldValue(field.name)
- if (obj == null) None else Some(f(obj))
- }
- private def list[A](field: Field, f: Object => A): List[A] = {
- val objs = rep.getFieldValues(field.name)
- if (objs == null) Nil else objs.iterator().asScala.toList.map(f)
- }
-
- def bool_value(obj: Object): Boolean = obj.asInstanceOf[Boolean]
- def int_value(obj: Object): Int = obj.asInstanceOf[Int]
- def long_value(obj: Object): Long = obj.asInstanceOf[Long]
- def double_value(obj: Object): Double = obj.asInstanceOf[Double]
- def string_value(obj: Object): String = obj.asInstanceOf[String]
- def bytes_value(obj: Object): Bytes = Bytes(obj.asInstanceOf[Array[Byte]])
- def date_value(obj: Object): Date = Date.instant(obj.asInstanceOf[java.util.Date].toInstant)
-
- def bool(field: Field): Boolean = single(field, bool_value)
- def int(field: Field): Int = single(field, int_value)
- def long(field: Field): Long = single(field, long_value)
- def double(field: Field): Double = single(field, double_value)
- def string(field: Field): String = single(field, string_value)
- def bytes(field: Field): Bytes = single(field, bytes_value)
- def date(field: Field): Date = single(field, date_value)
-
- def get_bool(field: Field): Option[Boolean] = get(field, bool_value)
- def get_int(field: Field): Option[Int] = get(field, int_value)
- def get_long(field: Field): Option[Long] = get(field, long_value)
- def get_double(field: Field): Option[Double] = get(field, double_value)
- def get_string(field: Field): Option[String] = get(field, string_value)
- def get_bytes(field: Field): Option[Bytes] = get(field, bytes_value)
- def get_date(field: Field): Option[Date] = get(field, date_value)
-
- def list_bool(field: Field): List[Boolean] = list(field, bool_value)
- def list_int(field: Field): List[Int] = list(field, int_value)
- def list_long(field: Field): List[Long] = list(field, long_value)
- def list_double(field: Field): List[Double] = list(field, double_value)
- def list_string(field: Field): List[String] = list(field, string_value)
- def list_bytes(field: Field): List[Bytes] = list(field, bytes_value)
- def list_date(field: Field): List[Date] = list(field, date_value)
- }
-
- class Results private[Solr](
- solr: EmbeddedSolrServer,
- query: SolrQuery,
- private var cursor: String,
- private var more_chunks: Int = -1
- ) extends Iterator[Result] {
- private def response: QueryResponse =
- solr.query(query.set(CursorMarkParams.CURSOR_MARK_PARAM, cursor))
-
- private var _response = response
- private var _iterator = _response.getResults.iterator
-
- def num_found: Long = _response.getResults.getNumFound
- def next_cursor: String = _response.getNextCursorMark
-
- def hasNext: Boolean = _iterator.hasNext
- def next(): Result = {
- val res = new Result(_iterator.next())
-
- if (!_iterator.hasNext && next_cursor != cursor && more_chunks != 0) {
- cursor = next_cursor
- more_chunks = more_chunks - 1
- _response = response
- _iterator = _response.getResults.iterator
- }
-
- res
- }
- }
-
-
- /* facet results */
-
- class Facet_Result private[Solr](rep: NestableJsonFacet) {
- def count: Long = rep.getCount
-
- private def get_bucket[A](bucket: BucketJsonFacet): (A, Long) =
- bucket.getVal.asInstanceOf[A] -> bucket.getCount
- private def get_facet[A](field: Field): Map[A, Long] =
- rep.getBucketBasedFacets(field.name).getBuckets.asScala.map(get_bucket).toMap
-
- def bool(field: Field): Map[Boolean, Long] = get_facet(field)
- def int(field: Field): Map[Int, Long] = get_facet(field)
- def long(field: Field): Map[Long, Long] = get_facet(field)
- def string(field: Field): Map[String, Long] = get_facet(field)
- }
-
-
- /* stat results */
-
- private def count_field(field: Field): String = field.name + "/count"
-
- class Stat_Result private[Solr](rep: NestableJsonFacet) {
- def count: Long = rep.getCount
- def count(field: Field): Long = rep.getStatValue(count_field(field)).asInstanceOf[Long]
- }
-
-
- /* database */
-
- def database_dir(database: String): Path = solr_home + Path.basic(database)
-
- def init_database(database: String, data: Data, clean: Boolean = false): Database = {
- val db_dir = database_dir(database)
-
- if (clean) Isabelle_System.rm_tree(db_dir)
-
- val conf_dir = db_dir + Path.basic("conf")
- if (!conf_dir.is_dir) {
- Isabelle_System.make_directory(conf_dir)
- 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))
- }
-
- open_database(database)
- }
-
- def open_database(database: String): Database = {
- val server = new EmbeddedSolrServer(solr_home.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)
- }
-
- class Database private[Solr](solr: EmbeddedSolrServer) extends AutoCloseable {
- override def close(): Unit = solr.close()
-
- def execute_query[A](
- id: Field,
- fields: List[Field],
- cursor: Option[String],
- chunk_size: Int,
- make_result: Results => A,
- q: Source = query_all,
- fq: List[Source] = Nil,
- more_chunks: Int = -1
- ): A = {
- val query = new SolrQuery(proper_string(q).getOrElse(query_all))
- .setFields(fields.map(_.name): _*)
- .setFilterQueries(fq.filterNot(_.isBlank): _*)
- .setRows(chunk_size)
- .addSort("score", SolrQuery.ORDER.desc)
- .addSort(id.name, SolrQuery.ORDER.asc)
-
- val cursor1 = cursor.getOrElse(CursorMarkParams.CURSOR_MARK_START)
- make_result(new Results(solr, query, cursor1, more_chunks))
- }
-
- private val in_transaction = Synchronized(false)
- def transaction[A](body: => A): A = synchronized {
- in_transaction.change(b => { require(!b, "transaction already active"); true })
- try {
- val result = body
- solr.commit()
- result
- }
- catch { case exn: Throwable => solr.rollback(); throw exn }
- finally { in_transaction.change(_ => false) }
- }
-
- def execute_facet_query[A](
- fields: List[Field],
- make_result: Facet_Result => A,
- q: Source = query_all,
- fq: List[Source] = Nil,
- max_terms: Int = -1
- ): A = {
- val query = new JsonQueryRequest().setQuery(proper_string(q).getOrElse(query_all)).setLimit(0)
- fq.filterNot(_.isBlank).foreach(query.withFilter)
-
- for (field <- fields) {
- val facet =
- new TermsFacetMap(field.name).setLimit(max_terms).withDomain(
- new DomainMap().withTagsToExclude(field.name))
- query.withFacet(field.name, facet)
- }
-
- make_result(new Facet_Result(query.process(solr).getJsonFacetingResponse))
- }
-
- def execute_stats_query[A](
- fields: List[Field],
- make_result: Stat_Result => A,
- q: Source = query_all,
- fq: List[Source] = Nil
- ): A = {
- val query = new JsonQueryRequest().setQuery(proper_string(q).getOrElse(query_all)).setLimit(0)
- fq.filterNot(_.isBlank).foreach(query.withFilter)
-
- for (field <- fields) query.withStatFacet(count_field(field), "unique(" + field.name + ")")
-
- make_result(new Stat_Result(query.process(solr).getJsonFacetingResponse))
- }
-
- def execute_batch_insert(batch: IterableOnce[Document => Unit]): Unit = {
- val it =
- batch.iterator.map { fill =>
- val doc = Document.empty
- fill(doc)
- doc.rep
- }
- solr.add(it.asJava)
- }
-
- def execute_batch_delete(ids: List[String]): Unit = solr.deleteById(ids.asJava)
- }
-}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/src/elm.scala Sat Jan 11 23:24:32 2025 +0100
@@ -0,0 +1,93 @@
+/* Author: Fabian Huch, TU Muenchen
+
+Elm module for Isabelle.
+*/
+
+package isabelle.find_facts
+
+
+import isabelle._
+
+import java.io.{File => JFile}
+
+import scala.jdk.CollectionConverters._
+
+import org.jsoup.nodes.Element
+
+
+object Elm {
+ private lazy val exec = Path.explode("$ISABELLE_ELM_HOME/elm").expand
+
+ object Project {
+ def apply(
+ name: String,
+ dir: Path,
+ main: Path = Path.explode("src/Main.elm"),
+ output: Path = Path.explode("index.html"),
+ head: XML.Body = Nil
+ ): Project = {
+ if (!dir.is_dir) error("Project directory does not exist: " + dir)
+ val main_file = dir + main
+ if (!main_file.is_file) error("Main elm file does not exist: " + main_file)
+ new Project(name, dir, main, dir + output, head)
+ }
+ }
+
+ class Project private(name: String, dir: Path, main: Path, output: Path, head: XML.Body) {
+ val definition = JSON.parse(File.read(dir + Path.basic("elm.json")))
+ val src_dirs =
+ JSON.strings(definition, "source-directories").getOrElse(
+ error("Missing source directories in elm.json"))
+
+ def sources: List[JFile] =
+ for {
+ src_dir <- src_dirs
+ path = dir + Path.explode(src_dir)
+ file <- File.find_files(path.file, _.getName.endsWith(".elm"))
+ } yield file
+
+ def sources_shasum: SHA1.Shasum = {
+ val meta_info = SHA1.shasum_meta_info(SHA1.digest(JSON.Format(definition)))
+ val head_digest = SHA1.shasum(SHA1.digest(XML.string_of_body(head)), "head")
+ val source_digest =
+ SHA1.shasum_sorted(for (file <- sources) yield SHA1.digest(file) -> file.getCanonicalPath)
+ meta_info ::: head_digest ::: source_digest
+ }
+
+ def get_digest: SHA1.Digest =
+ Exn.capture {
+ val html = HTML.parse_document(File.read(output))
+ val elem = html.head.getElementsByTag("meta").attr("name", "shasum")
+ Library.the_single(elem.eachAttr("content").asScala.toList)
+ } match {
+ case Exn.Res(s) => SHA1.fake_digest(s)
+ case _ => SHA1.digest_empty
+ }
+
+ def build_html(progress: Progress): String = {
+ val digest = sources_shasum.digest
+ if (digest == get_digest) File.read(output)
+ else {
+ progress.echo("### Building " + name + " (" + output.canonical.implode + ") ...")
+
+ val cmd =
+ File.bash_path(exec) + " make " + File.bash_path(main) + " --optimize --output=" + output
+ val res = Isabelle_System.bash(cmd, cwd = dir)
+
+ if (!res.ok) {
+ progress.echo(res.err)
+ error("Failed to compile Elm sources")
+ }
+
+ val file = HTML.parse_document(File.read(output))
+ file.head.appendChild(
+ Element("meta").attr("name", "shasum").attr("content", digest.toString))
+ file.head.append(XML.string_of_body(head))
+ val html = file.html
+ File.write(output, html)
+
+ html
+ }
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/src/find_facts.scala Sat Jan 11 23:24:32 2025 +0100
@@ -0,0 +1,952 @@
+/* Title: Tools/Find_Facts.scala
+ Author: Fabian Huch, TU Muenchen
+
+Full-text search engine for Isabelle (including web server), using Solr as backend.
+*/
+
+package isabelle.find_facts
+
+
+import isabelle._
+
+import scala.annotation.tailrec
+import scala.collection.immutable.TreeMap
+import scala.collection.mutable
+
+
+object Find_Facts {
+ /** blocks **/
+
+ object Kind {
+ val CONST = "constant"
+ val TYPE = "type"
+ val THM = "fact"
+ }
+
+ case class Block(
+ id: String,
+ version: Long,
+ chapter: String,
+ session: String,
+ theory: String,
+ file: String,
+ url_path: Path,
+ command: String,
+ start_line: Int,
+ src_before: String,
+ src: String,
+ src_after: String,
+ xml: XML.Body,
+ html: String,
+ entity_kname: Option[String],
+ consts: List[String],
+ typs: List[String],
+ thms: List[String]
+ ) {
+ def path = Path.explode(file)
+ def file_type: String = path.get_ext
+ def file_name: String = path.file_name
+
+ def kinds: List[String] =
+ (if (typs.nonEmpty) List(Kind.TYPE) else Nil) :::
+ (if (consts.nonEmpty) List(Kind.CONST) else Nil) :::
+ (if (thms.nonEmpty) List(Kind.THM) else Nil)
+ def names: List[String] = (typs ::: consts ::: thms).distinct
+ }
+
+ case class Blocks(num_found: Long, blocks: List[Block], cursor: String)
+
+
+ /** queries */
+
+ enum Atom {
+ case Exact(s: String) extends Atom
+ case Value(s: String) extends Atom
+ }
+
+ enum Field {
+ case chapter, session, file_type, theory, command, source, names, consts, typs, thms, kinds
+ }
+
+ sealed trait Filter
+ case class Field_Filter(field: Field, either: List[Atom]) extends Filter
+ case class Any_Filter(either: List[Atom]) extends Filter {
+ def fields: List[Field] = List(Field.session, Field.theory, Field.source, Field.names)
+ }
+
+ case class Select(field: Field, values: List[String])
+
+ object Query {
+ def apply(filters: Filter*): Query = new Query(filters.toList)
+ }
+
+ case class Query(
+ filters: List[Filter] = Nil,
+ exclude: List[Filter] = Nil,
+ selects: List[Select] = Nil)
+
+
+ /* stats and facets */
+
+ case class Stats(
+ results: Long,
+ sessions: Long,
+ theories: Long,
+ commands: Long,
+ consts: Long,
+ typs: Long,
+ thms: Long)
+
+ case class Facets(
+ chapter: Map[String, Long],
+ session: Map[String, Long],
+ theory: Map[String, Long],
+ file_type: Map[String, Long],
+ command: Map[String, Long],
+ kinds: Map[String, Long],
+ consts: Map[String, Long],
+ typs: Map[String, Long],
+ thms: Map[String, Long])
+
+
+ /** Solr data model **/
+
+ object private_data extends Solr.Data("find_facts") {
+ /* types */
+
+ val symbol_codes =
+ for {
+ entry <- Symbol.symbols.entries
+ code <- entry.decode.toList
+ input <- entry.symbol :: entry.abbrevs
+ } yield input -> code
+
+ val replacements =
+ for ((symbol, codes) <- symbol_codes.groupMap(_._1)(_._2).toList if codes.length == 1)
+ yield symbol -> Library.the_single(codes)
+
+ val Special_Char = """(.*[(){}\[\].,:"].*)""".r
+ val Arrow = """(.*=>.*)""".r
+
+ val synonyms =
+ for {
+ (symbol, code) <- symbol_codes
+ if !Special_Char.matches(symbol) && !Arrow.matches(symbol)
+ } yield symbol + " => " + code
+
+ override lazy val more_config = Map(Path.basic("synonyms.txt") -> synonyms.mkString("\n"))
+
+ object Types {
+ private val strip_html = Solr.Class("charFilter", "HTMLStripCharFilterFactory")
+ private val replace_symbol_chars =
+ replacements.collect {
+ case (Special_Char(pattern), code) =>
+ Solr.Class(
+ "charFilter", "PatternReplaceCharFilterFactory",
+ List("pattern" -> ("\\Q" + pattern + "\\E"), "replacement" -> code))
+ }
+
+ private val symbol_pattern =
+ """\s*(::|[(){}\[\].,:"]|[^\p{ASCII}]|((?![^\p{ASCII}])[^(){}\[\].,:"\s])+)\s*""".r
+
+ private val tokenize =
+ Solr.Class("tokenizer", "WhitespaceTokenizerFactory", List("rule" -> "java"))
+ private val tokenize_symbols =
+ Solr.Class("tokenizer", "PatternTokenizerFactory",
+ List("pattern" -> symbol_pattern.toString, "group" -> "1"))
+
+ private val to_lower = Solr.Class("filter", "LowerCaseFilterFactory")
+ private val add_ascii =
+ Solr.Class("filter", "ASCIIFoldingFilterFactory", List("preserveOriginal" -> "true"))
+ private val delimit_words =
+ Solr.Class("filter", "WordDelimiterGraphFilterFactory", List(
+ "splitOnCaseChange" -> "0", "stemEnglishPossessive" -> "0", "preserveOriginal" -> "1"))
+ private val flatten = Solr.Class("filter", "FlattenGraphFilterFactory")
+ private val replace_symbols =
+ Solr.Class("filter", "SynonymGraphFilterFactory", List("synonyms" -> "synonyms.txt"))
+ private val replace_special_symbols =
+ replacements.collect {
+ case (Arrow(arrow), code) =>
+ Solr.Class("filter", "PatternReplaceFilterFactory",
+ List("pattern" -> ("\\Q" + arrow + "\\E"), "replacement" -> code))
+ }
+
+ val source =
+ Solr.Type("name", "TextField", Nil, List(
+ XML.Elem(Markup("analyzer", List("type" -> "index")),
+ List(strip_html, tokenize_symbols, to_lower, add_ascii, delimit_words, flatten)),
+ XML.Elem(
+ Markup("analyzer", List("type" -> "query")),
+ replace_symbol_chars ::: tokenize_symbols :: replace_symbols ::
+ replace_special_symbols ::: to_lower :: Nil)))
+
+ val name =
+ Solr.Type("source", "TextField", Nil, List(
+ XML.Elem(Markup("analyzer", List("type" -> "index")),
+ List(tokenize, to_lower, delimit_words, flatten)),
+ XML.Elem(Markup("analyzer", List("type" -> "query")), List(tokenize, to_lower))))
+
+ val text = Solr.Type("text", "TextField")
+ }
+
+
+ /* fields */
+
+ object Fields {
+ val id = Solr.Field("id", Solr.Type.string).make_unique_key
+ val version = Solr.Field("version", Solr.Type.long, Solr.Column_Wise(true))
+ val chapter = Solr.Field("chapter", Solr.Type.string, Solr.Column_Wise(true))
+ val session = Solr.Field("session", Types.name)
+ val session_facet = Solr.Field("session_facet", Solr.Type.string, Solr.Stored(false))
+ val theory = Solr.Field("theory", Types.name)
+ val theory_facet = Solr.Field("theory_facet", Solr.Type.string, Solr.Stored(false))
+ val file = Solr.Field("file", Solr.Type.string, Solr.Indexed(false))
+ val file_type =
+ Solr.Field("file_type", Solr.Type.string, Solr.Column_Wise(true) ::: Solr.Stored(false))
+ val url_path = Solr.Field("url_path", Solr.Type.string, Solr.Indexed(false))
+ val command = Solr.Field("command", Solr.Type.string, Solr.Column_Wise(true))
+ val start_line = Solr.Field("start_line", Solr.Type.int, Solr.Column_Wise(true))
+ val src_before = Solr.Field("src_before", Solr.Type.string, Solr.Indexed(false))
+ val src_after = Solr.Field("src_after", Solr.Type.string, Solr.Indexed(false))
+ val src = Solr.Field("src", Types.source)
+ val xml = Solr.Field("xml", Solr.Type.bytes, Solr.Indexed(false))
+ val html = Solr.Field("html", Solr.Type.bytes, Solr.Indexed(false))
+ val entity_kname = Solr.Field("entity_kname", Solr.Type.string, Solr.Indexed(false))
+ val consts = Solr.Field("consts", Types.name, Solr.Multi_Valued(true))
+ val consts_facet =
+ Solr.Field("consts_facet", Solr.Type.string, Solr.Multi_Valued(true) ::: Solr.Stored(false))
+ val typs = Solr.Field("typs", Types.name, Solr.Multi_Valued(true))
+ val typs_facet =
+ Solr.Field("typs_facet", Solr.Type.string, Solr.Multi_Valued(true) ::: Solr.Stored(false))
+ val thms = Solr.Field("thms", Types.name, Solr.Multi_Valued(true))
+ val thms_facet =
+ Solr.Field("thms_facet", Solr.Type.string, Solr.Multi_Valued(true) ::: Solr.Stored(false))
+ val names = Solr.Field("names", Types.name, Solr.Multi_Valued(true) ::: Solr.Stored(false))
+ val kinds =
+ Solr.Field("kinds", Solr.Type.string,
+ Solr.Multi_Valued(true) ::: Solr.Column_Wise(true) ::: Solr.Stored(false))
+ }
+
+ lazy val fields: Solr.Fields = Solr.Fields(
+ Fields.id, Fields.version, Fields.chapter, Fields.session, Fields.session_facet,
+ Fields.theory, Fields.theory_facet, Fields.file, Fields.file_type, Fields.url_path,
+ Fields.command, Fields.start_line, Fields.src_before, Fields.src_after, Fields.src,
+ Fields.xml, Fields.html, Fields.entity_kname, Fields.consts, Fields.consts_facet, Fields.typs,
+ Fields.typs_facet, Fields.thms, Fields.thms_facet, Fields.names, Fields.kinds)
+
+
+ /* operations */
+
+ def read_domain(db: Solr.Database, q: Solr.Source): Set[String] =
+ db.execute_query(Fields.id, List(Fields.id), None, 100000,
+ { results =>
+ results.map(_.string(Fields.id)).toSet
+ }, q = q)
+
+ def read_block(res: Solr.Result): Block = {
+ val id = res.string(Fields.id)
+ val version = res.long(Fields.version)
+ val chapter = res.string(Fields.chapter)
+ val session = res.string(Fields.session)
+ val theory = res.string(Fields.theory)
+ val file = res.string(Fields.file)
+ val url_path = Path.explode(res.string(Fields.url_path))
+ val command = res.string(Fields.command)
+ val start_line = res.int(Fields.start_line)
+ val src_before = res.string(Fields.src_before)
+ val src = res.string(Fields.src)
+ val src_after = res.string(Fields.src_after)
+ val xml = YXML.parse_body(res.bytes(Fields.xml))
+ val html = res.bytes(Fields.html).text
+ val entity_kname = res.get_string(Fields.entity_kname)
+ val consts = res.list_string(Fields.consts)
+ val typs = res.list_string(Fields.typs)
+ val thms = res.list_string(Fields.thms)
+
+ Block(id = id, version = version, chapter = chapter, session = session, theory = theory,
+ file = file, url_path = url_path, command = command, start_line = start_line, src_before =
+ src_before, src = src, src_after = src_after, xml = xml, html = html, entity_kname =
+ entity_kname, consts = consts, typs = typs, thms = thms)
+ }
+
+ def read_blocks(
+ db: Solr.Database,
+ q: Solr.Source,
+ fq: List[Solr.Source],
+ cursor: Option[String] = None,
+ max_results: Int = 10
+ ): Blocks =
+ db.execute_query(Fields.id, stored_fields, cursor, max_results,
+ { results =>
+ val next_cursor = results.next_cursor
+ val blocks = results.map(read_block).toList
+ Blocks(results.num_found, blocks, next_cursor)
+ }, q = q, fq = fq, more_chunks = 0)
+
+ def stream_blocks(
+ db: Solr.Database,
+ q: Solr.Source,
+ stream: Iterator[Block] => Unit,
+ cursor: Option[String] = None,
+ ): Unit =
+ db.execute_query(Fields.id, stored_fields, cursor, 10000,
+ { results =>
+ stream(results.map(read_block))
+ }, q = q)
+
+ def update_theory(db: Solr.Database, theory_name: String, blocks: List[Block]): Unit =
+ db.transaction {
+ val delete =
+ read_domain(db, Solr.filter(Fields.theory, Solr.phrase(theory_name))) -- blocks.map(_.id)
+
+ if (delete.nonEmpty) db.execute_batch_delete(delete.toList)
+
+ db.execute_batch_insert(
+ for (block <- blocks) yield { (doc: Solr.Document) =>
+ doc.string(Fields.id) = block.id
+ doc.long(Fields.version) = block.version
+ doc.string(Fields.chapter) = block.chapter
+ doc.string(Fields.session) = block.session
+ doc.string(Fields.session_facet) = block.session
+ doc.string(Fields.theory) = block.theory
+ doc.string(Fields.theory_facet) = block.theory
+ doc.string(Fields.file) = block.file
+ doc.string(Fields.file_type) = block.file_type
+ doc.string(Fields.url_path) = block.url_path.implode
+ doc.string(Fields.command) = block.command
+ doc.int(Fields.start_line) = block.start_line
+ doc.string(Fields.src_before) = block.src_before
+ doc.string(Fields.src) = block.src
+ doc.string(Fields.src_after) = block.src_after
+ doc.bytes(Fields.xml) = YXML.bytes_of_body(block.xml)
+ doc.bytes(Fields.html) = Bytes(block.html)
+ doc.string(Fields.entity_kname) = block.entity_kname
+ doc.string(Fields.consts) = block.consts
+ doc.string(Fields.consts_facet) = block.consts
+ doc.string(Fields.typs) = block.typs
+ doc.string(Fields.typs_facet) = block.typs
+ doc.string(Fields.thms) = block.thms
+ doc.string(Fields.thms_facet) = block.thms
+ doc.string(Fields.names) = block.names
+ doc.string(Fields.kinds) = block.kinds
+ })
+ }
+
+ def read_theory(db: Solr.Database, theory_name: String): List[Block] = {
+ val blocks = new mutable.ListBuffer[Block]
+ stream_blocks(db, Solr.filter(Fields.theory_facet, Solr.phrase(theory_name)), {
+ res => blocks ++= res
+ })
+ blocks.toList
+ }
+
+ def delete_session(db: Solr.Database, session_name: String): Unit =
+ db.transaction {
+ val delete = read_domain(db, Solr.filter(Fields.session, Solr.phrase(session_name)))
+ if (delete.nonEmpty) db.execute_batch_delete(delete.toList)
+ }
+
+ def query_stats(db: Solr.Database, q: Solr.Source, fq: List[Solr.Source]): Stats =
+ db.execute_stats_query(
+ List(Fields.session_facet, Fields.theory_facet, Fields.command, Fields.consts_facet,
+ Fields.typs_facet, Fields.thms_facet, Fields.start_line),
+ { res =>
+ val results = res.count
+ val sessions = res.count(Fields.session_facet)
+ val theories = res.count(Fields.theory_facet)
+ val commands = res.count(Fields.theory_facet)
+ val consts = res.count(Fields.consts_facet)
+ val typs = res.count(Fields.typs_facet)
+ val thms = res.count(Fields.thms_facet)
+
+ Stats(results, sessions, theories, commands, consts, typs, thms)
+ }, q = q, fq = fq)
+
+ def query_facets(
+ db: Solr.Database,
+ q: Solr.Source,
+ fq: List[Solr.Source],
+ max_terms: Int = 100
+ ): Facets =
+ db.execute_facet_query(
+ List(Fields.chapter, Fields.session_facet, Fields.theory_facet, Fields.file_type,
+ Fields.command, Fields.kinds, Fields.consts_facet, Fields.typs_facet, Fields.thms_facet),
+ { res =>
+ val chapter = res.string(Fields.chapter)
+ val sessions = res.string(Fields.session_facet)
+ val theories = res.string(Fields.theory_facet)
+ val file_types = res.string(Fields.file_type)
+ val commands = res.string(Fields.command)
+ val kinds = res.string(Fields.kinds)
+ val consts = res.string(Fields.consts_facet)
+ val typs = res.string(Fields.typs_facet)
+ val thms = res.string(Fields.thms_facet)
+
+ Facets(chapter, sessions, theories, file_types, commands, kinds, consts, typs, thms)
+ }, q = q, fq = fq, max_terms = max_terms)
+
+
+ /* queries */
+
+ def solr_field(field: Field, select: Boolean = false): Solr.Field =
+ field match {
+ case Field.chapter => Fields.chapter
+ case Field.session if select => Fields.session_facet
+ case Field.session => Fields.session
+ case Field.theory if select => Fields.theory_facet
+ case Field.theory => Fields.theory
+ case Field.file_type => Fields.file_type
+ case Field.command => Fields.command
+ case Field.source => Fields.src
+ case Field.names => Fields.names
+ case Field.consts if select => Fields.consts_facet
+ case Field.consts => Fields.consts
+ case Field.typs if select => Fields.typs_facet
+ case Field.typs => Fields.typs
+ case Field.thms if select => Fields.thms_facet
+ case Field.thms => Fields.thms
+ case Field.kinds => Fields.kinds
+ }
+
+ def solr_query(query: Query): (Solr.Source, List[Solr.Source]) = {
+ def solr_atom(atom: Atom): List[Solr.Source] =
+ atom match {
+ case Atom.Value(s) if s.isEmpty => Nil
+ case Atom.Value(s) if !s.exists(Solr.wildcard_char(_)) => List(Solr.term(s))
+ case Atom.Value(s) =>
+ val terms = s.split("\\s+").toList.filterNot(_.isBlank)
+ if (terms.isEmpty) Nil else terms.map(Solr.wildcard)
+ case Atom.Exact(s) => List(Solr.phrase(s))
+ }
+
+ def solr_atoms(field: Field, atoms: List[Atom]): List[Solr.Source] =
+ for {
+ atom <- atoms
+ source <- solr_atom(atom)
+ } yield Solr.filter(solr_field(field), source)
+
+ def solr_filter(filter: Filter): List[Solr.Source] =
+ filter match {
+ case Field_Filter(field, atoms) => solr_atoms(field, atoms)
+ case any@Any_Filter(atoms) => any.fields.flatMap(solr_atoms(_, atoms))
+ }
+
+ def solr_select(select: Select): Solr.Source = {
+ val field = solr_field(select.field, select = true)
+ Solr.tag(field.name, Solr.filter(field, Solr.OR(select.values.map(Solr.phrase))))
+ }
+
+ val filter = query.filters.map(filter => Solr.OR(solr_filter(filter)))
+ val exclude = query.exclude.flatMap(solr_filter).map(Solr.exclude)
+ val selects = query.selects.map(solr_select)
+
+ (Solr.AND(filter ::: exclude), selects)
+ }
+ }
+
+ 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
+ }
+
+ def query_blocks(db: Solr.Database, query: Query, cursor: Option[String] = None): Blocks = {
+ val (q, fq) = Find_Facts.private_data.solr_query(query)
+ Find_Facts.private_data.read_blocks(db, q, fq, cursor = cursor)
+ }
+
+ def query_stats(db: Solr.Database, query: Query): Stats = {
+ val (q, fq) = Find_Facts.private_data.solr_query(query)
+ Find_Facts.private_data.query_stats(db, q, fq)
+ }
+
+ def query_facet(db: Solr.Database, query: Query): Facets = {
+ val (q, fq) = Find_Facts.private_data.solr_query(query)
+ Find_Facts.private_data.query_facets(db, q, fq)
+ }
+
+
+ /** indexing **/
+
+ def make_thy_blocks(
+ options: Options,
+ session: Session,
+ browser_info_context: Browser_Info.Context,
+ document_info: Document_Info,
+ theory_context: Export.Theory_Context,
+ snapshot: Document.Snapshot,
+ chapter: String
+ ): List[Block] = {
+ val theory = theory_context.theory
+ val entities = Export_Theory.read_theory(theory_context).entity_iterator.toList
+ val session_name = theory_context.session_context.session_name
+
+ 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)
+
+ def make_node_blocks(
+ snapshot: Document.Snapshot,
+ command_ranges: List[(String, Text.Range)]
+ ): 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 elements =
+ Browser_Info.Elements(html = Browser_Info.default_elements.html - Markup.ENTITY)
+ val node_context = Browser_Info.Node_Context.empty
+
+ val content = XML.content(snapshot.xml_markup(elements = Markup.Elements.empty))
+ def get_content(range: Text.Range): String =
+ Symbol.decode(Line.normalize(range.substring(content)))
+
+ val document = Line.Document(content.replace('\r', '\u001a'))
+ val num_lines = document.lines.length
+ def content_range(start: Line.Position, stop: Line.Position): Text.Range =
+ Text.Range(document.offset(start).get, document.offset(stop).get)
+
+ val index = Symbol.Index(content)
+ val node_entities =
+ TreeMap.from(entities
+ .filter(entity => entity.file == snapshot.node_name.node)
+ .groupBy(entity => index.decode(entity.range).start))
+
+ val rendering = new Rendering(snapshot, options, session)
+ val comment_ranges = rendering.comments(Text.Range.full).map(markup => ("", markup.range))
+
+ for ((command, range) <- command_ranges ::: comment_ranges) yield {
+ val line_range = document.range(range)
+ val start_line = line_range.start.line1
+
+ val id = file + "|" + range.start + ".." + range.stop
+
+ val src_before = get_content(
+ content_range(Line.Position((line_range.start.line - 5).max(0)), line_range.start))
+ val src = get_content(range)
+ val src_after = get_content(
+ content_range(line_range.stop, Line.Position((line_range.stop.line + 5).min(num_lines))))
+
+ val xml = snapshot.xml_markup(range, elements = elements.html)
+ val html =
+ HTML.output(node_context.make_html(elements, xml), hidden = true, structural = false)
+
+ val entities = node_entities.range(range.start, range.stop).values.toList.flatten.distinct
+
+ def get_entities(kind: String): List[String] =
+ for {
+ entity <- entities
+ if entity.export_kind == kind
+ if range.contains(index.decode(entity.range))
+ } yield entity.name
+
+ val entity_kname = entities.sortBy(_.name.length).headOption.map(_.kname)
+
+ val typs = get_entities(Export_Theory.Kind.TYPE)
+ val consts = get_entities(Export_Theory.Kind.CONST)
+ val thms = get_entities(Export_Theory.Kind.THM)
+
+ Block(id = id, version = version, chapter = chapter, session = session_name, theory =
+ theory, file = file, url_path = url_path, command = command, start_line = start_line,
+ src_before = src_before, src = src, src_after = src_after, xml = xml, html = html,
+ entity_kname = entity_kname, consts = consts, typs = typs, thms = thms)
+ }
+ }
+
+ def expand_block(block: Thy_Blocks.Block): List[Thy_Blocks.Block] =
+ block match {
+ case Thy_Blocks.Thy(inner) => inner.flatMap(expand_block)
+ case e@Thy_Blocks.Decl(inner) =>
+ val inner1 = inner.flatMap(expand_block)
+ if (inner.length > 1) e :: inner1 else List(e)
+ case _ => List(block)
+ }
+
+ val thy_command_ranges =
+ for (block <- Thy_Blocks.read_blocks(snapshot).flatMap(expand_block))
+ yield (block.command, block.range)
+
+ make_node_blocks(snapshot, thy_command_ranges) :::
+ (for {
+ blob_name <- snapshot.node_files.tail
+ snapshot1 = snapshot.switch(blob_name)
+ if snapshot1.node.source_wellformed
+ range = Text.Range.length(snapshot1.node.source)
+ block <- make_node_blocks(snapshot1, List(("", range)))
+ } yield block)
+ }
+
+ def find_facts_index(
+ options: Options,
+ sessions: List[String],
+ dirs: List[Path] = Nil,
+ clean: Boolean = false,
+ progress: Progress = new Progress
+ ): Unit = {
+ val store = Store(options)
+ val database = options.string("find_facts_database_name")
+ val session = Session(options, Resources.bootstrap)
+
+ val selection = Sessions.Selection(sessions = sessions)
+ val session_structure = Sessions.load_structure(options, dirs = dirs).selection(selection)
+ val deps = Sessions.Deps.load(session_structure)
+ val browser_info_context = Browser_Info.context(session_structure)
+
+ if (sessions.isEmpty) progress.echo("Nothing to index")
+ else {
+ 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 + " ...")
+
+ 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("Theory " + name.theory + " ...")
+ 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)
+ }
+ }
+ }
+ }
+
+ Par_List.map(index_session, sessions)
+ }
+
+ val query = Query(Field_Filter(Field.session, sessions.map(Atom.Exact(_))))
+ Find_Facts.query_stats(db, query)
+ }
+
+ progress.echo("Indexed " + stats.results + " blocks with " +
+ stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
+ }
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool1 = Isabelle_Tool("find_facts_index", "index sessions for find_facts",
+ Scala_Project.here,
+ { args =>
+ var clean = false
+ val dirs = new mutable.ListBuffer[Path]
+ var options = Options.init()
+
+ val getopts = Getopts("""
+ Usage: isabelle find_facts_index [OPTIONS] [SESSIONS ...]
+
+ Options are:
+ -c clean previous index
+ -d DIR include session directory
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+
+ Index sessions for find_facts.
+ """,
+ "c" -> (_ => clean = true),
+ "d:" -> (arg => dirs += Path.explode(arg)),
+ "o:" -> (arg => options = options + arg))
+
+ val sessions = getopts(args)
+
+ val progress = new Console_Progress()
+
+ find_facts_index(options, sessions, dirs = dirs.toList, clean = clean, progress = progress)
+ })
+
+
+ /** index components **/
+
+ def find_facts_index_component(
+ options: Options,
+ target_dir: Path = Path.current,
+ progress: Progress = new Progress
+ ): Unit = {
+ val database = options.string("find_facts_database_name")
+
+ val component = "find_facts_index-" + database
+ val component_dir =
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
+
+ Isabelle_System.copy_dir(Solr.database_dir(database), component_dir.path)
+ component_dir.write_settings("SOLR_COMPONENTS=\"$SOLR_COMPONENTS:$COMPONENT/" + database + "\"")
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool2 = Isabelle_Tool("find_facts_index_component",
+ "build component from find_facts index", Scala_Project.here,
+ { args =>
+ var options = Options.init()
+ var target_dir = Path.current
+
+ val getopts = Getopts("""
+ Usage: isabelle find_facts_index_component
+
+ Options are:
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -D DIR target directory (default ".")
+
+ Build component from finalized find_facts index with given name.
+ """,
+ "o:" -> (arg => options = options + arg),
+ "D:" -> (arg => target_dir = Path.explode(arg)))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ find_facts_index_component(options, target_dir = target_dir)
+ })
+
+
+ /** querying **/
+
+ /* requests and parsing */
+
+ case class Query_Blocks(query: Query, cursor: String)
+
+ object Parse {
+ def atom(json: JSON.T): Option[Atom] =
+ JSON.string(json, "value").map(Atom.Value(_)) orElse
+ JSON.string(json, "exact").map(Atom.Exact(_))
+
+ def field(name: String): Option[Field] = Field.values.find(_.toString == name)
+
+ def filter(json: JSON.T): Option[Filter] =
+ for {
+ atoms <- JSON.list(json, "either", atom)
+ filter <-
+ JSON.string(json, "field") match {
+ case None => Some(Any_Filter(atoms))
+ case Some(name) => for (field <- field(name)) yield Field_Filter(field, atoms)
+ }
+ } yield filter
+
+ def select(json: JSON.T): Option[Select] =
+ for {
+ name <- JSON.string(json, "field")
+ field <- field(name)
+ values <- JSON.strings(json, "values")
+ } yield Select(field, values)
+
+ def query(json: JSON.T): Option[Query] =
+ for {
+ filters <- JSON.list(json, "filters", filter)
+ exclude <- JSON.list(json, "exclude", filter)
+ selects <- JSON.list(json, "selects", select)
+ } yield Query(filters, exclude, selects)
+
+ def query_blocks(json: JSON.T): Option[Query_Blocks] =
+ for {
+ query <- JSON.value(json, "query", query)
+ cursor <- JSON.string(json, "cursor")
+ } yield Query_Blocks(query, cursor)
+
+ def query_block(json: JSON.T): Option[String] = for (id <- JSON.string(json, "id")) yield id
+ }
+
+
+ /* responses and encoding */
+
+ case class Result(blocks: Blocks, facets: Facets)
+
+ class Encode(options: Options) {
+ val library_base_url = Url(options.string("browser_info_url_library"))
+ val afp_base_url = Url(options.string("browser_info_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)
+ }
+
+ def block(block: Block): JSON.T =
+ JSON.Object(
+ "id" -> block.id,
+ "chapter" -> block.chapter,
+ "session" -> block.session,
+ "theory" -> block.theory,
+ "file" -> block.file,
+ "file_name" -> block.file_name,
+ "url" -> url(block).toString,
+ "command" -> block.command,
+ "start_line" -> block.start_line,
+ "src_before" -> block.src_before,
+ "src_after" -> block.src_after,
+ "html" -> block.html,
+ "entity_kname" -> block.entity_kname.orNull)
+
+ def blocks(blocks: Blocks): JSON.T =
+ JSON.Object(
+ "num_found" -> blocks.num_found,
+ "blocks" -> blocks.blocks.map(block),
+ "cursor" -> blocks.cursor)
+
+ def facets(facet: Facets): JSON.T =
+ JSON.Object(
+ "chapter" -> facet.chapter,
+ "session" -> facet.session,
+ "file_type" -> facet.file_type,
+ "theory" -> facet.theory,
+ "command" -> facet.command,
+ "kinds" -> facet.kinds,
+ "consts" -> facet.consts,
+ "typs" -> facet.typs,
+ "thms" -> facet.thms)
+
+ def result(result: Result): JSON.T =
+ JSON.Object(
+ "blocks" -> blocks(result.blocks),
+ "facets" -> facets(result.facets))
+ }
+
+
+ /* find facts */
+
+ abstract class REST_Service(path: Path, progress: Progress, method: String = "POST")
+ extends HTTP.Service(path.implode, method = method) {
+ def handle(body: JSON.T): Option[JSON.T]
+
+ def apply(request: HTTP.Request): Option[HTTP.Response] =
+ try {
+ for {
+ json <-
+ Exn.capture(JSON.parse(request.input.text)) match {
+ case Exn.Res(json) => Some(json)
+ case _ =>
+ progress.echo("Could not parse: " + quote(request.input.text), verbose = true)
+ None
+ }
+ res <-
+ handle(json) match {
+ case Some(res) => Some(res)
+ case None =>
+ progress.echo("Invalid request: " + JSON.Format(json), verbose = true)
+ None
+ }
+ } yield HTTP.Response(Bytes(JSON.Format(res)), content_type = "application/json")
+ }
+ catch { case exn: Throwable =>
+ val uuid = UUID.random()
+ progress.echo_error_message("Server error <" + uuid + ">: " + exn)
+ Some(HTTP.Response.text("internal server error: " + uuid))
+ }
+ }
+
+ def find_facts(
+ options: Options,
+ port: Int,
+ devel: Boolean = false,
+ progress: Progress = new Progress
+ ): Unit = {
+ val database = options.string("find_facts_database_name")
+ val encode = new Encode(options)
+ val logo = Bytes.read(Path.explode("$FIND_FACTS_HOME/web/favicon.ico"))
+
+ val isabelle_style = HTML.fonts_css("/fonts/" + _) + "\n\n" + File.read(HTML.isabelle_css)
+
+ val project = Elm.Project("Find_Facts", Path.explode("$FIND_FACTS_HOME/web"), head = List(
+ HTML.style("html,body {width: 100%, height: 100%}"),
+ Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text),
+ HTML.style_file("isabelle.css"),
+ HTML.style_file("https://fonts.googleapis.com/css?family=Roboto:300,400,500|Material+Icons"),
+ HTML.style_file(
+ "https://unpkg.com/material-components-web-elm@9.1.0/dist/material-components-web-elm.min.css"),
+ HTML.script_file(
+ "https://unpkg.com/material-components-web-elm@9.1.0/dist/material-components-web-elm.min.js")))
+
+ val frontend = project.build_html(progress)
+
+ using(Solr.open_database(database)) { db =>
+ val stats = Find_Facts.query_stats(db, Query(Nil))
+ progress.echo("Started find facts with " + stats.results + " blocks, " +
+ stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
+
+ val server =
+ HTTP.server(port, name = "", services = List(
+ HTTP.Fonts_Service,
+ new HTTP.Service("isabelle.css") {
+ def apply(request: HTTP.Request): Option[HTTP.Response] =
+ Some(HTTP.Response(Bytes(isabelle_style), "text/css"))
+ },
+ new HTTP.Service("app") {
+ def apply(request: HTTP.Request): Option[HTTP.Response] =
+ Some(HTTP.Response.html(if (devel) project.build_html(progress) else frontend))
+ },
+ new REST_Service(Path.explode("api/block"), progress) {
+ def handle(body: JSON.T): Option[JSON.T] =
+ for {
+ request <- Parse.query_block(body)
+ block <- query_block(db, request)
+ } yield encode.block(block)
+ },
+ new REST_Service(Path.explode("api/blocks"), 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)))
+ },
+ new REST_Service(Path.explode("api/query"), 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))
+ }
+ }))
+
+ server.start()
+ progress.echo("Server started on port " + server.http_server.getAddress.getPort)
+
+ @tailrec
+ def loop(): Unit = {
+ Thread.sleep(Long.MaxValue)
+ loop()
+ }
+
+ Isabelle_Thread.interrupt_handler(_ => server.stop()) { loop() }
+ }
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool3 = Isabelle_Tool("find_facts", "run find_facts server", Scala_Project.here,
+ { args =>
+ var devel = false
+ var options = Options.init()
+ var port = 8080
+ var verbose = false
+
+ val getopts = Getopts("""
+Usage: isabelle find_facts [OPTIONS]
+
+ Options are:
+ -d devel mode
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -p PORT explicit web server port
+ -v verbose server
+
+ Run the find_facts web service.
+""",
+ "d" -> (_ => devel = true),
+ "o:" -> (arg => options = options + arg),
+ "p:" -> (arg => port = Value.Int.parse(arg)),
+ "v" -> (_ => verbose = true))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress(verbose = verbose)
+
+ find_facts(options, port, devel = devel, progress = progress)
+ })
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/src/solr.scala Sat Jan 11 23:24:32 2025 +0100
@@ -0,0 +1,455 @@
+/* Author: Fabian Huch, TU Muenchen
+
+Support for full-text search via Solr. See also: https://solr.apache.org/
+*/
+
+package isabelle.find_facts
+
+
+import isabelle._
+
+import scala.jdk.CollectionConverters._
+
+import org.apache.solr.client.solrj.embedded.EmbeddedSolrServer
+import org.apache.solr.client.solrj.request.json.{JsonQueryRequest, TermsFacetMap, DomainMap}
+import org.apache.solr.client.solrj.response.json.{BucketJsonFacet, NestableJsonFacet}
+import org.apache.solr.client.solrj.response.QueryResponse
+import org.apache.solr.client.solrj.SolrQuery
+import org.apache.solr.common.params.CursorMarkParams
+import org.apache.solr.common.{SolrDocument, SolrInputDocument}
+
+
+object Solr {
+ def init(solr_home: Path): Path = {
+ File.write(Isabelle_System.make_directory(solr_home) + Path.basic("solr.xml"), "<solr/>")
+
+ for (entry <- space_explode(':', Isabelle_System.getenv("SOLR_COMPONENTS")) if entry.nonEmpty)
+ Isabelle_System.symlink(Path.explode(entry).absolute, solr_home, force = true)
+
+ java.util.logging.LogManager.getLogManager.reset()
+ solr_home
+ }
+
+ lazy val solr_home = init(Path.explode("$ISABELLE_HOME_USER/solr"))
+
+
+ /** query language */
+
+ val wildcard_char = Set('*', '?')
+ val special =
+ Set("+", "-", "&&", "||", "!", "(", ")", "{", "}", "[", "]", "^", "\"", "~", "*", "?", ":", "/")
+
+ type Source = String
+
+ val all: Source = "*"
+
+ def enclose(s: Source): Source = "(" + s + ")"
+
+ def escape(s: String, seqs: Set[String]): Source =
+ seqs.foldLeft(s.replace("\\", "\\\\"))((s, seq) => s.replace(seq, "\\" + seq))
+
+ def term(b: Boolean): Source = b.toString
+ def term(i: Int): Source = i.toString
+ def term(s: String): Source =
+ "(\\s+)".r.replaceAllIn(escape(s, special), ws => "\\\\" + ws.matched)
+
+ def range(from: Int, to: Int): Source = "[" + from + " TO " + to + "]"
+ def phrase(s: String): Source = quote(escape(s, special))
+ def wildcard(s: String): Source =
+ if (!s.toList.exists(Symbol.is_ascii_blank)) escape(s, special -- wildcard_char.map(_.toString))
+ else error("Invalid whitespace character in wildcard: " + quote(s))
+
+ def filter(field: Field, x: Source): Source = field.name + ":" + x
+
+ def infix(op: Source, args: Iterable[Source]): Source = {
+ val body = args.iterator.filterNot(_.isBlank).mkString(" " + op + " ")
+ if_proper(body, enclose(body))
+ }
+
+ def AND(args: Iterable[Source]): Source = infix("AND", args)
+ def OR(args: Iterable[Source]): Source = infix("OR", args)
+
+ def and(args: Source*): Source = AND(args)
+ def or(args: Source*): Source = OR(args)
+
+ def exclude(arg: Source): Source = if_proper(arg, "-" + arg)
+
+ val query_all: Source = "*:" + all
+
+ def tag(name: String, arg: Source): Source = "{!tag=" + name + "}" + arg
+
+
+ /** solr schema **/
+
+ object Class {
+ def apply(
+ markup: String,
+ name: String,
+ props: Properties.T = Nil,
+ body: XML.Body = Nil
+ ): XML.Elem = XML.Elem(Markup(markup, ("class" -> ("solr." + name)) :: props), body)
+ }
+
+
+ /* properties */
+
+ val Indexed = new Properties.Boolean("indexed")
+ val Stored = new Properties.Boolean("stored")
+ val Column_Wise = new Properties.Boolean("docValues")
+ val Multi_Valued = new Properties.Boolean("multiValued")
+
+
+ /* types */
+
+ object Type {
+ val bool = Type("bool", "BoolField")
+ val int = Type("int", "IntPointField")
+ val long = Type("long", "LongPointField")
+ val double = Type("double", "DoublePointField")
+ val string = Type("string", "StrField")
+ val bytes = Type("bytes", "BinaryField")
+ val date = Type("date", "DatePointField")
+ }
+
+ case class Type(name: String, cls: String, props: Properties.T = Nil, body: XML.Body = Nil) {
+ def defn: XML.Elem = Class("fieldType", cls, Markup.Name(name) ::: props, body)
+ }
+
+
+ /* fields */
+
+ sealed case class Field(
+ name: String,
+ T: Type,
+ props: Properties.T = Nil,
+ unique_key: Boolean = false
+ ) {
+ def make_unique_key: Field = copy(unique_key = true)
+ def defn: XML.Elem = XML.elem(Markup("field", ("name" -> name) :: ("type" -> T.name) :: props))
+ }
+
+ object Fields {
+ def list(list: List[Field]): Fields = new Fields(list)
+ def apply(args: Field*): Fields = list(args.toList)
+ }
+
+ final class Fields private(val list: List[Field]) extends Iterable[Field] {
+ override def toString: String = list.mkString("Solr.Fields(", ", ", ")")
+ def iterator: Iterator[Field] = list.iterator
+ }
+
+
+ /* data */
+
+ abstract class Data(val name: String) {
+ def fields: Fields
+ def more_config: Map[Path, String] = Map.empty
+
+ def stored_fields: List[Field] =
+ fields.toList.filter(_.props match {
+ case Stored(false) => false
+ case _ => true
+ })
+
+ def unique_key: Field = Library.the_single(fields.filter(_.unique_key).toList)
+
+ def solr_config: XML.Body = List(XML.elem("config", List(
+ Class("schemaFactory", "ClassicIndexSchemaFactory"),
+ XML.elem("luceneMatchVersion", XML.string(Isabelle_System.getenv("SOLR_LUCENE_VERSION"))),
+ Class("updateHandler", "DirectUpdateHandler2", body = List(
+ XML.elem("autoCommit", List(
+ XML.elem("maxDocs", XML.string("-1")),
+ XML.elem("maxTime", XML.string("-1")),
+ XML.elem("maxSize", XML.string("-1")))))),
+ Class("requestHandler", "SearchHandler", Markup.Name("/select")))))
+
+ def schema: XML.Body =
+ List(XML.Elem(Markup("schema",
+ List(
+ "name" -> "isabelle",
+ "version" -> Isabelle_System.getenv("SOLR_SCHEMA_VERSION"))),
+ List(
+ XML.elem("uniqueKey", XML.string(unique_key.name)),
+ XML.elem("fields", fields.toList.map(_.defn)),
+ XML.elem("types", fields.map(_.T).toList.distinct.map(_.defn)))))
+ }
+
+
+ /** solr operations */
+
+ /* documents */
+
+ object Document {
+ def empty: Document = new Document(new SolrInputDocument())
+ }
+
+ class Document private[Solr](val rep: SolrInputDocument) {
+ private def obj[A](a: A): Object = a.asInstanceOf[Object]
+ private def set[A](field: Field, x: A, f: A => Object = obj): Unit =
+ rep.addField(field.name, f(x))
+ private def set_option[A](field: Field, x: Option[A], f: A => Object = obj): Unit =
+ rep.addField(field.name, x.map(f).orNull)
+ private def set_list[A](field: Field, x: List[A], f: A => Object = obj): Unit =
+ rep.addField(field.name, x.map(f).toArray)
+
+ object bool {
+ def update(field: Field, x: Boolean): Unit = set(field, x)
+ def update(field: Field, x: Option[Boolean]): Unit = set_option(field, x)
+ def update(field: Field, x: List[Boolean]): Unit = set_list(field, x)
+ }
+ object int {
+ def update(field: Field, x: Int): Unit = set(field, x)
+ def update(field: Field, x: Option[Int]): Unit = set_option(field, x)
+ def update(field: Field, x: List[Int]): Unit = set_list(field, x)
+ }
+ object long {
+ def update(field: Field, x: Long): Unit = set(field, x)
+ def update(field: Field, x: Option[Long]): Unit = set_option(field, x)
+ def update(field: Field, x: List[Long]): Unit = set_list(field, x)
+ }
+ object double {
+ def update(field: Field, x: Double): Unit = set(field, x)
+ def update(field: Field, x: Option[Double]): Unit = set_option(field, x)
+ def update(field: Field, x: List[Double]): Unit = set_list(field, x)
+ }
+ object string {
+ def update(field: Field, x: String): Unit = set(field, x)
+ def update(field: Field, x: Option[String]): Unit = set_option(field, x)
+ def update(field: Field, x: List[String]): Unit = set_list(field, x)
+ }
+ object bytes {
+ private def value(bytes: Bytes): Array[Byte] =
+ if (bytes.size > Int.MaxValue) throw new IllegalArgumentException else bytes.make_array
+ def update(field: Field, x: Bytes): Unit = set(field, x, value)
+ def update(field: Field, x: Option[Bytes]): Unit = set_option(field, x, value)
+ def update(field: Field, x: List[Bytes]): Unit = set_list(field, x, value)
+ }
+ object date {
+ private def value(date: Date): java.util.Date = java.util.Date.from(date.rep.toInstant)
+ def update(field: Field, x: Date): Unit = set(field, x, value)
+ def update(field: Field, x: Option[Date]): Unit = set_option(field, x, value)
+ def update(field: Field, x: List[Date]): Unit = set_list(field, x, value)
+ }
+ }
+
+
+ /* results */
+
+ class Result private[Solr](rep: SolrDocument) {
+ private def single[A](field: Field, f: Object => A): A = {
+ val obj = rep.getFieldValue(field.name)
+ if (obj == null) error("No such field: " + field.name) else f(obj)
+ }
+ private def get[A](field: Field, f: Object => A): Option[A] = {
+ val obj = rep.getFieldValue(field.name)
+ if (obj == null) None else Some(f(obj))
+ }
+ private def list[A](field: Field, f: Object => A): List[A] = {
+ val objs = rep.getFieldValues(field.name)
+ if (objs == null) Nil else objs.iterator().asScala.toList.map(f)
+ }
+
+ def bool_value(obj: Object): Boolean = obj.asInstanceOf[Boolean]
+ def int_value(obj: Object): Int = obj.asInstanceOf[Int]
+ def long_value(obj: Object): Long = obj.asInstanceOf[Long]
+ def double_value(obj: Object): Double = obj.asInstanceOf[Double]
+ def string_value(obj: Object): String = obj.asInstanceOf[String]
+ def bytes_value(obj: Object): Bytes = Bytes(obj.asInstanceOf[Array[Byte]])
+ def date_value(obj: Object): Date = Date.instant(obj.asInstanceOf[java.util.Date].toInstant)
+
+ def bool(field: Field): Boolean = single(field, bool_value)
+ def int(field: Field): Int = single(field, int_value)
+ def long(field: Field): Long = single(field, long_value)
+ def double(field: Field): Double = single(field, double_value)
+ def string(field: Field): String = single(field, string_value)
+ def bytes(field: Field): Bytes = single(field, bytes_value)
+ def date(field: Field): Date = single(field, date_value)
+
+ def get_bool(field: Field): Option[Boolean] = get(field, bool_value)
+ def get_int(field: Field): Option[Int] = get(field, int_value)
+ def get_long(field: Field): Option[Long] = get(field, long_value)
+ def get_double(field: Field): Option[Double] = get(field, double_value)
+ def get_string(field: Field): Option[String] = get(field, string_value)
+ def get_bytes(field: Field): Option[Bytes] = get(field, bytes_value)
+ def get_date(field: Field): Option[Date] = get(field, date_value)
+
+ def list_bool(field: Field): List[Boolean] = list(field, bool_value)
+ def list_int(field: Field): List[Int] = list(field, int_value)
+ def list_long(field: Field): List[Long] = list(field, long_value)
+ def list_double(field: Field): List[Double] = list(field, double_value)
+ def list_string(field: Field): List[String] = list(field, string_value)
+ def list_bytes(field: Field): List[Bytes] = list(field, bytes_value)
+ def list_date(field: Field): List[Date] = list(field, date_value)
+ }
+
+ class Results private[Solr](
+ solr: EmbeddedSolrServer,
+ query: SolrQuery,
+ private var cursor: String,
+ private var more_chunks: Int = -1
+ ) extends Iterator[Result] {
+ private def response: QueryResponse =
+ solr.query(query.set(CursorMarkParams.CURSOR_MARK_PARAM, cursor))
+
+ private var _response = response
+ private var _iterator = _response.getResults.iterator
+
+ def num_found: Long = _response.getResults.getNumFound
+ def next_cursor: String = _response.getNextCursorMark
+
+ def hasNext: Boolean = _iterator.hasNext
+ def next(): Result = {
+ val res = new Result(_iterator.next())
+
+ if (!_iterator.hasNext && next_cursor != cursor && more_chunks != 0) {
+ cursor = next_cursor
+ more_chunks = more_chunks - 1
+ _response = response
+ _iterator = _response.getResults.iterator
+ }
+
+ res
+ }
+ }
+
+
+ /* facet results */
+
+ class Facet_Result private[Solr](rep: NestableJsonFacet) {
+ def count: Long = rep.getCount
+
+ private def get_bucket[A](bucket: BucketJsonFacet): (A, Long) =
+ bucket.getVal.asInstanceOf[A] -> bucket.getCount
+ private def get_facet[A](field: Field): Map[A, Long] =
+ rep.getBucketBasedFacets(field.name).getBuckets.asScala.map(get_bucket).toMap
+
+ def bool(field: Field): Map[Boolean, Long] = get_facet(field)
+ def int(field: Field): Map[Int, Long] = get_facet(field)
+ def long(field: Field): Map[Long, Long] = get_facet(field)
+ def string(field: Field): Map[String, Long] = get_facet(field)
+ }
+
+
+ /* stat results */
+
+ private def count_field(field: Field): String = field.name + "/count"
+
+ class Stat_Result private[Solr](rep: NestableJsonFacet) {
+ def count: Long = rep.getCount
+ def count(field: Field): Long = rep.getStatValue(count_field(field)).asInstanceOf[Long]
+ }
+
+
+ /* database */
+
+ def database_dir(database: String): Path = solr_home + Path.basic(database)
+
+ def init_database(database: String, data: Data, clean: Boolean = false): Database = {
+ val db_dir = database_dir(database)
+
+ if (clean) Isabelle_System.rm_tree(db_dir)
+
+ val conf_dir = db_dir + Path.basic("conf")
+ if (!conf_dir.is_dir) {
+ Isabelle_System.make_directory(conf_dir)
+ 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))
+ }
+
+ open_database(database)
+ }
+
+ def open_database(database: String): Database = {
+ val server = new EmbeddedSolrServer(solr_home.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)
+ }
+
+ class Database private[Solr](solr: EmbeddedSolrServer) extends AutoCloseable {
+ override def close(): Unit = solr.close()
+
+ def execute_query[A](
+ id: Field,
+ fields: List[Field],
+ cursor: Option[String],
+ chunk_size: Int,
+ make_result: Results => A,
+ q: Source = query_all,
+ fq: List[Source] = Nil,
+ more_chunks: Int = -1
+ ): A = {
+ val query = new SolrQuery(proper_string(q).getOrElse(query_all))
+ .setFields(fields.map(_.name): _*)
+ .setFilterQueries(fq.filterNot(_.isBlank): _*)
+ .setRows(chunk_size)
+ .addSort("score", SolrQuery.ORDER.desc)
+ .addSort(id.name, SolrQuery.ORDER.asc)
+
+ val cursor1 = cursor.getOrElse(CursorMarkParams.CURSOR_MARK_START)
+ make_result(new Results(solr, query, cursor1, more_chunks))
+ }
+
+ private val in_transaction = Synchronized(false)
+ def transaction[A](body: => A): A = synchronized {
+ in_transaction.change(b => { require(!b, "transaction already active"); true })
+ try {
+ val result = body
+ solr.commit()
+ result
+ }
+ catch { case exn: Throwable => solr.rollback(); throw exn }
+ finally { in_transaction.change(_ => false) }
+ }
+
+ def execute_facet_query[A](
+ fields: List[Field],
+ make_result: Facet_Result => A,
+ q: Source = query_all,
+ fq: List[Source] = Nil,
+ max_terms: Int = -1
+ ): A = {
+ val query = new JsonQueryRequest().setQuery(proper_string(q).getOrElse(query_all)).setLimit(0)
+ fq.filterNot(_.isBlank).foreach(query.withFilter)
+
+ for (field <- fields) {
+ val facet =
+ new TermsFacetMap(field.name).setLimit(max_terms).withDomain(
+ new DomainMap().withTagsToExclude(field.name))
+ query.withFacet(field.name, facet)
+ }
+
+ make_result(new Facet_Result(query.process(solr).getJsonFacetingResponse))
+ }
+
+ def execute_stats_query[A](
+ fields: List[Field],
+ make_result: Stat_Result => A,
+ q: Source = query_all,
+ fq: List[Source] = Nil
+ ): A = {
+ val query = new JsonQueryRequest().setQuery(proper_string(q).getOrElse(query_all)).setLimit(0)
+ fq.filterNot(_.isBlank).foreach(query.withFilter)
+
+ for (field <- fields) query.withStatFacet(count_field(field), "unique(" + field.name + ")")
+
+ make_result(new Stat_Result(query.process(solr).getJsonFacetingResponse))
+ }
+
+ def execute_batch_insert(batch: IterableOnce[Document => Unit]): Unit = {
+ val it =
+ batch.iterator.map { fill =>
+ val doc = Document.empty
+ fill(doc)
+ doc.rep
+ }
+ solr.add(it.asJava)
+ }
+
+ def execute_batch_delete(ids: List[String]): Unit = solr.deleteById(ids.asJava)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/src/thy_blocks.scala Sat Jan 11 23:24:32 2025 +0100
@@ -0,0 +1,143 @@
+/* Author: Fabian Huch, TU Muenchen
+
+Block structure for Isabelle theories, read from build database.
+*/
+
+package isabelle.find_facts
+
+
+import isabelle._
+
+import scala.annotation.tailrec
+
+
+object Thy_Blocks {
+ /** spans **/
+
+ val keyword_elements =
+ Markup.Elements(Markup.KEYWORD, Markup.KEYWORD1, Markup.KEYWORD2, Markup.KEYWORD3)
+
+ object Span {
+ def read_build(snapshot: Document.Snapshot): List[Span] = {
+ def is_begin(markup: Text.Markup): Boolean = markup.info match {
+ case XML.Elem(Markup(_, Markup.Kind(Markup.KEYWORD)), Nil) =>
+ XML.content(snapshot.xml_markup(markup.range)) == "begin"
+ case _ => false
+ }
+
+ def has_begin(range: Text.Range): Boolean =
+ snapshot
+ .select(range, keyword_elements, _ => markup => Some(is_begin(markup)))
+ .exists(_.info)
+
+ snapshot.select(Text.Range.full, Markup.Elements(Markup.COMMAND_SPAN), _ =>
+ {
+ case Text.Info(range, XML.Elem(Markup.Command_Span(arg), _)) =>
+ Some(Span(range, arg.name, arg.kind, has_begin(range)))
+ case _ => None
+ }).map(_.info)
+ }
+ }
+
+ case class Span(
+ override val range: Text.Range,
+ override val command: String,
+ kind: String,
+ has_begin: Boolean
+ ) extends Block {
+ def spans: List[Span] = List(this)
+
+ def is_of_kind(kinds: Set[String]): Boolean = kinds.contains(kind)
+ }
+
+
+ /** block structure **/
+
+ sealed trait Block {
+ def spans: List[Span]
+
+ def command: String = spans.head.command
+ def range: Text.Range = Text.Range(spans.head.range.start, spans.last.range.stop)
+ }
+
+ case class Single(span: Span) extends Block { def spans = List(span) }
+ case class Thy(inner: List[Block]) extends Block { def spans = inner.flatMap(_.spans) }
+ case class Prf(inner: List[Block]) extends Block { def spans = inner.flatMap(_.spans) }
+ case class Decl(inner: List[Block]) extends Block { def spans = inner.flatMap(_.spans) }
+
+
+ /** parser **/
+
+ object Parser {
+ object Blocks {
+ def empty: Blocks = new Blocks(Nil, Nil)
+ }
+
+ case class Blocks(private val stack: List[Block], private val out: List[Block]) {
+ def peek: Option[Block] = stack.headOption
+ def push(block: Block): Blocks = copy(stack = block :: stack)
+ def add(block: Block): Blocks =
+ stack match {
+ case Nil => copy(out = block :: out)
+ case head :: rest =>
+ val head1 =
+ head match {
+ case Thy(inner) => Thy(inner :+ block)
+ case Prf(inner) => Prf(inner :+ block)
+ case Decl(inner) => Decl(inner :+ block)
+ case _ => error("Cannot add to " + head)
+ }
+ copy(stack = head1 :: rest)
+ }
+
+ def pop: Blocks =
+ stack match {
+ case Nil => error("Nothing to pop")
+ case head :: rest => copy(stack = rest).add(head)
+ }
+
+ def pop_prfs: Blocks = {
+ val blocks1 = pop
+ blocks1.stack match {
+ case Prf(_) :: _ => blocks1.pop_prfs
+ case _ => blocks1
+ }
+ }
+
+ def output: List[Block] = if (stack.nonEmpty) error("Nonempty stack") else out.reverse
+ }
+
+ def parse(spans: List[Span]): List[Block] = {
+ import Keyword.*
+
+ def parse1(blocks: Blocks, span: Span): Blocks =
+ blocks.peek match {
+ case _ if span.is_of_kind(document) => blocks.add(span)
+ case None if span.is_of_kind(theory_begin) => blocks.push(Thy(List(span)))
+ case Some(_) if span.is_of_kind(diag) => blocks.add(span)
+ case Some(Thy(_)) if span.is_of_kind(theory_goal) => blocks.push(Prf(List(span)))
+ case Some(Thy(_)) if span.is_of_kind(theory_block) =>
+ (if (span.has_begin) blocks.push else blocks.add)(Decl(List(span)))
+ case Some(Thy(_)) if span.is_of_kind(theory_end) => blocks.add(span).pop
+ case Some(Thy(_)) if span.is_of_kind(theory_body) => blocks.add(span)
+ case Some(Prf(_)) if span.is_of_kind(proof_open) => blocks.push(Prf(List(span)))
+ case Some(Prf(_)) if span.is_of_kind(proof_close) => blocks.add(span).pop
+ case Some(Prf(_)) if span.is_of_kind(qed_global) => blocks.add(span).pop_prfs
+ case Some(Prf(_)) if span.is_of_kind(proof_body) => blocks.add(span)
+ case Some(Decl(_)) if span.is_of_kind(proof_open) => blocks.push(Prf(List(span)))
+ case Some(Decl(_)) if span.is_of_kind(proof_body) => blocks.add(span)
+ case Some(Decl(_)) if span.is_of_kind(theory_goal) => blocks.push(Prf(List(span)))
+ case Some(Decl(_)) if span.is_of_kind(theory_block) =>
+ (if (span.has_begin) blocks.push else blocks.add)(Decl(List(span)))
+ case Some(Decl(_)) if span.is_of_kind(theory_end) => blocks.add(span).pop
+ case Some(Decl(_)) if span.is_of_kind(theory_body) => blocks.add(span)
+ case e => error("Unexpected span " + span + " at " + e)
+ }
+
+ spans.foldLeft(Blocks.empty)(parse1).output
+ }
+ }
+
+ def read_blocks(snapshot: Document.Snapshot): List[Block] =
+ Parser.parse(Span.read_build(snapshot))
+}
--- a/src/Tools/Find_Facts/thy_blocks.scala Sat Jan 11 23:19:10 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-/* Author: Fabian Huch, TU Muenchen
-
-Block structure for Isabelle theories, read from build database.
-*/
-
-package isabelle
-
-
-import scala.annotation.tailrec
-
-
-object Thy_Blocks {
- /** spans **/
-
- val keyword_elements =
- Markup.Elements(Markup.KEYWORD, Markup.KEYWORD1, Markup.KEYWORD2, Markup.KEYWORD3)
-
- object Span {
- def read_build(snapshot: Document.Snapshot): List[Span] = {
- def is_begin(markup: Text.Markup): Boolean = markup.info match {
- case XML.Elem(Markup(_, Markup.Kind(Markup.KEYWORD)), Nil) =>
- XML.content(snapshot.xml_markup(markup.range)) == "begin"
- case _ => false
- }
-
- def has_begin(range: Text.Range): Boolean =
- snapshot
- .select(range, keyword_elements, _ => markup => Some(is_begin(markup)))
- .exists(_.info)
-
- snapshot.select(Text.Range.full, Markup.Elements(Markup.COMMAND_SPAN), _ =>
- {
- case Text.Info(range, XML.Elem(Markup.Command_Span(arg), _)) =>
- Some(Span(range, arg.name, arg.kind, has_begin(range)))
- case _ => None
- }).map(_.info)
- }
- }
-
- case class Span(
- override val range: Text.Range,
- override val command: String,
- kind: String,
- has_begin: Boolean
- ) extends Block {
- def spans: List[Span] = List(this)
-
- def is_of_kind(kinds: Set[String]): Boolean = kinds.contains(kind)
- }
-
-
- /** block structure **/
-
- sealed trait Block {
- def spans: List[Span]
-
- def command: String = spans.head.command
- def range: Text.Range = Text.Range(spans.head.range.start, spans.last.range.stop)
- }
-
- case class Single(span: Span) extends Block { def spans = List(span) }
- case class Thy(inner: List[Block]) extends Block { def spans = inner.flatMap(_.spans) }
- case class Prf(inner: List[Block]) extends Block { def spans = inner.flatMap(_.spans) }
- case class Decl(inner: List[Block]) extends Block { def spans = inner.flatMap(_.spans) }
-
-
- /** parser **/
-
- object Parser {
- object Blocks {
- def empty: Blocks = new Blocks(Nil, Nil)
- }
-
- case class Blocks(private val stack: List[Block], private val out: List[Block]) {
- def peek: Option[Block] = stack.headOption
- def push(block: Block): Blocks = copy(stack = block :: stack)
- def add(block: Block): Blocks =
- stack match {
- case Nil => copy(out = block :: out)
- case head :: rest =>
- val head1 =
- head match {
- case Thy(inner) => Thy(inner :+ block)
- case Prf(inner) => Prf(inner :+ block)
- case Decl(inner) => Decl(inner :+ block)
- case _ => error("Cannot add to " + head)
- }
- copy(stack = head1 :: rest)
- }
-
- def pop: Blocks =
- stack match {
- case Nil => error("Nothing to pop")
- case head :: rest => copy(stack = rest).add(head)
- }
-
- def pop_prfs: Blocks = {
- val blocks1 = pop
- blocks1.stack match {
- case Prf(_) :: _ => blocks1.pop_prfs
- case _ => blocks1
- }
- }
-
- def output: List[Block] = if (stack.nonEmpty) error("Nonempty stack") else out.reverse
- }
-
- def parse(spans: List[Span]): List[Block] = {
- import Keyword.*
-
- def parse1(blocks: Blocks, span: Span): Blocks =
- blocks.peek match {
- case _ if span.is_of_kind(document) => blocks.add(span)
- case None if span.is_of_kind(theory_begin) => blocks.push(Thy(List(span)))
- case Some(_) if span.is_of_kind(diag) => blocks.add(span)
- case Some(Thy(_)) if span.is_of_kind(theory_goal) => blocks.push(Prf(List(span)))
- case Some(Thy(_)) if span.is_of_kind(theory_block) =>
- (if (span.has_begin) blocks.push else blocks.add)(Decl(List(span)))
- case Some(Thy(_)) if span.is_of_kind(theory_end) => blocks.add(span).pop
- case Some(Thy(_)) if span.is_of_kind(theory_body) => blocks.add(span)
- case Some(Prf(_)) if span.is_of_kind(proof_open) => blocks.push(Prf(List(span)))
- case Some(Prf(_)) if span.is_of_kind(proof_close) => blocks.add(span).pop
- case Some(Prf(_)) if span.is_of_kind(qed_global) => blocks.add(span).pop_prfs
- case Some(Prf(_)) if span.is_of_kind(proof_body) => blocks.add(span)
- case Some(Decl(_)) if span.is_of_kind(proof_open) => blocks.push(Prf(List(span)))
- case Some(Decl(_)) if span.is_of_kind(proof_body) => blocks.add(span)
- case Some(Decl(_)) if span.is_of_kind(theory_goal) => blocks.push(Prf(List(span)))
- case Some(Decl(_)) if span.is_of_kind(theory_block) =>
- (if (span.has_begin) blocks.push else blocks.add)(Decl(List(span)))
- case Some(Decl(_)) if span.is_of_kind(theory_end) => blocks.add(span).pop
- case Some(Decl(_)) if span.is_of_kind(theory_body) => blocks.add(span)
- case e => error("Unexpected span " + span + " at " + e)
- }
-
- spans.foldLeft(Blocks.empty)(parse1).output
- }
- }
-
- def read_blocks(snapshot: Document.Snapshot): List[Block] =
- Parser.parse(Span.read_build(snapshot))
-}