# HG changeset patch
# User wenzelm
# Date 1662819172 -7200
# Node ID 4dedb6e2dac25ec2f208a44954aa529e1b8107c4
# Parent  7ce11c135dad6a419c3198d304979d72d28f31e9
more command-line options;

diff -r 7ce11c135dad -r 4dedb6e2dac2 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Sep 10 15:48:36 2022 +0200
+++ b/src/Doc/System/Sessions.thy	Sat Sep 10 16:12:52 2022 +0200
@@ -865,6 +865,7 @@
     -R           refer to requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
+    -b           follow session build dependencies (default: source imports)
     -d DIR       include session directory
     -g NAME      select session group NAME
     -x NAME      exclude session NAME and all descendants
@@ -884,7 +885,15 @@
   @{verbatim [display] \<open>  isabelle sessions -a\<close>}
 
   \<^medskip>
-  Sessions that are based on \<^verbatim>\<open>ZF\<close> (and required by it):
+  Sessions that are imported by \<^verbatim>\<open>ZF\<close>:
+  @{verbatim [display] \<open>  isabelle sessions ZF\<close>}
+
+  \<^medskip>
+  Sessions that are required to build \<^verbatim>\<open>ZF\<close>:
+  @{verbatim [display] \<open>  isabelle sessions -b ZF\<close>}
+
+  \<^medskip>
+  Sessions that are based on \<^verbatim>\<open>ZF\<close> (and imported by it):
   @{verbatim [display] \<open>  isabelle sessions -B ZF\<close>}
 
   \<^medskip>
diff -r 7ce11c135dad -r 4dedb6e2dac2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Sep 10 15:48:36 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Sep 10 16:12:52 2022 +0200
@@ -1167,6 +1167,7 @@
       var requirements = false
       var exclude_session_groups: List[String] = Nil
       var all_sessions = false
+      var build_graph = false
       var dirs: List[Path] = Nil
       var session_groups: List[String] = Nil
       var exclude_sessions: List[String] = Nil
@@ -1180,6 +1181,7 @@
     -R           refer to requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
+    -b           follow session build dependencies (default: source imports)
     -d DIR       include session directory
     -g NAME      select session group NAME
     -x NAME      exclude session NAME and all descendants
@@ -1192,6 +1194,7 @@
         "R" -> (_ => requirements = true),
         "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
         "a" -> (_ => all_sessions = true),
+        "b" -> (_ => build_graph = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "g:" -> (arg => session_groups = session_groups ::: List(arg)),
         "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
@@ -1207,9 +1210,10 @@
       val sessions_structure =
         load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
 
-      for (name <- sessions_structure.imports_topological_order) {
-        Output.writeln(name, stdout = true)
-      }
+      val order =
+        if (build_graph) sessions_structure.build_topological_order
+        else sessions_structure.imports_topological_order
+      for (name <- order) Output.writeln(name, stdout = true)
     })