# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1742564111 -3600
# Node ID c6193fc5ea3c17c0500861bdb2488c63b99be0bd
# Parent  a3b556a235410fdc49b03de4f746f0199a556934
proper deletion: use facet fields that are not tokenized;

diff -r a3b556a23541 -r c6193fc5ea3c src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Fri Mar 21 10:48:48 2025 +0000
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Fri Mar 21 14:35:11 2025 +0100
@@ -306,8 +306,8 @@
 
     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)
+        val domain = read_domain(db, Solr.filter(Fields.theory_facet, Solr.phrase(theory_name)))
+        val delete = domain -- blocks.map(_.id)
 
         if (delete.nonEmpty) db.execute_batch_delete(delete.toList)
 
@@ -352,7 +352,7 @@
 
     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)))
+        val delete = read_domain(db, Solr.filter(Fields.session_facet, Solr.phrase(session_name)))
         if (delete.nonEmpty) db.execute_batch_delete(delete.toList)
       }