# HG changeset patch
# User wenzelm
# Date 1693332884 -7200
# Node ID 2c3a05b297f4a336594d0ac617a2d1982cb891c2
# Parent  9acd819db33ac258a891eaf01fdf8789c60bf3dc
discontinue special treatment of AFP: "isabelle dump" has been superseded by regular "isabelle build" databases;

diff -r 9acd819db33a -r 2c3a05b297f4 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Aug 29 19:20:51 2023 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Aug 29 20:14:44 2023 +0200
@@ -152,12 +152,6 @@
       val session_graph = deps.sessions_structure.build_graph
       val all_sessions = session_graph.topological_order
 
-      val afp_sessions =
-        (for (name <- all_sessions if session_info(name).is_afp) yield name).toSet
-
-      val afp_bulky_sessions =
-        (for (name <- all_sessions if session_info(name).is_afp_bulky) yield name).toList
-
       val base_sessions =
         session_graph.all_preds_rev(List(logic).filter(session_graph.defined))
 
@@ -187,25 +181,12 @@
       val main =
         make_session(
           session_graph.topological_order.filterNot(name =>
-            afp_sessions.contains(name) ||
             base_sessions.contains(name) ||
             proof_sessions.contains(name)))
 
       val proofs = make_session(proof_sessions, session_logic = PURE, record_proofs = true)
 
-      val afp =
-        if (afp_sessions.isEmpty) Nil
-        else {
-          val (part1, part2) = {
-            val graph = session_graph.restrict(afp_sessions -- afp_bulky_sessions)
-            val force_partition1 = AFP.force_partition1.filter(graph.defined)
-            val force_part1 = graph.all_preds(graph.all_succs(force_partition1)).toSet
-            graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
-          }
-          List(part1, part2, afp_bulky_sessions).flatMap(make_session(_))
-        }
-
-      proofs ::: base ::: main ::: afp
+      proofs ::: base ::: main
     }