# HG changeset patch
# User wenzelm
# Date 1588103242 -7200
# Node ID e2ad50885887f8b3e17f42fc22185babb6a7bacf
# Parent  cdfa8f027bb9d0f2d1a26b44642da4b6746936aa
added "isabelle sessions" tool;

diff -r cdfa8f027bb9 -r e2ad50885887 NEWS
--- a/NEWS	Tue Apr 28 19:50:36 2020 +0200
+++ b/NEWS	Tue Apr 28 21:47:22 2020 +0200
@@ -12,6 +12,10 @@
 * The command-line tool "isabelle console" now supports interrupts
 properly (on Linux and macOS).
 
+* The command-line tool "isabelle sessions" explores the structure of
+Isabelle sessions and prints result names in topological order (on
+stdout).
+
 * The Isabelle/Scala "Progress" interface changed slightly and
 "No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
 instead.
diff -r cdfa8f027bb9 -r e2ad50885887 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Apr 28 19:50:36 2020 +0200
+++ b/src/Doc/System/Sessions.thy	Tue Apr 28 21:47:22 2020 +0200
@@ -709,4 +709,50 @@
   sessions, notably from the Archive of Formal Proofs.
 \<close>
 
+
+section \<open>Explore sessions structure\<close>
+
+text \<open>
+  The @{tool_def "sessions"} tool explores the sessions structure. Its
+  command-line usage is:
+  @{verbatim [display]
+\<open>Usage: isabelle sessions [OPTIONS] [SESSIONS ...]
+
+  Options are:
+    -B NAME      include session NAME and all descendants
+    -D DIR       include session directory and select its sessions
+    -R           refer to requirements of selected sessions
+    -X NAME      exclude sessions from group NAME and all descendants
+    -a           select all sessions
+    -d DIR       include session directory
+    -g NAME      select session group NAME
+    -x NAME      exclude session NAME and all descendants
+
+  Explore the structure of Isabelle sessions and print result names in
+  topological order (on stdout).\<close>}
+
+  Arguments and options for session selection resemble @{tool build}
+  (\secref{sec:tool-build}).
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+  All sessions of the Isabelle distribution:
+  @{verbatim [display] \<open>isabelle sessions -a\<close>}
+
+  \<^medskip>
+  Sessions that are based on \<^verbatim>\<open>ZF\<close> (and required by it):
+  @{verbatim [display] \<open>isabelle sessions -B ZF\<close>}
+
+  \<^medskip>
+  All sessions of Isabelle/AFP (based in directory \<^path>\<open>AFP\<close>):
+  @{verbatim [display] \<open>isabelle sessions -D AFP/thys\<close>}
+
+  \<^medskip>
+  Sessions required by Isabelle/AFP (based in directory \<^path>\<open>AFP\<close>):
+  @{verbatim [display] \<open>isabelle sessions -R -D AFP/thys\<close>}
+\<close>
+
 end
diff -r cdfa8f027bb9 -r e2ad50885887 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Tue Apr 28 19:50:36 2020 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Tue Apr 28 21:47:22 2020 +0200
@@ -158,6 +158,7 @@
   Present.isabelle_tool,
   Profiling_Report.isabelle_tool,
   Server.isabelle_tool,
+  Sessions.isabelle_tool,
   Scala_Project.isabelle_tool,
   Update.isabelle_tool,
   Update_Cartouches.isabelle_tool,
diff -r cdfa8f027bb9 -r e2ad50885887 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 28 19:50:36 2020 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 28 21:47:22 2020 +0200
@@ -949,6 +949,61 @@
   }
 
 
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions", args =>
+  {
+    var base_sessions: List[String] = Nil
+    var select_dirs: List[Path] = Nil
+    var requirements = false
+    var exclude_session_groups: List[String] = Nil
+    var all_sessions = false
+    var dirs: List[Path] = Nil
+    var session_groups: List[String] = Nil
+    var exclude_sessions: List[String] = Nil
+
+    val getopts = Getopts("""
+Usage: isabelle sessions [OPTIONS] [SESSIONS ...]
+
+  Options are:
+    -B NAME      include session NAME and all descendants
+    -D DIR       include session directory and select its sessions
+    -R           refer to requirements of selected sessions
+    -X NAME      exclude sessions from group NAME and all descendants
+    -a           select all sessions
+    -d DIR       include session directory
+    -g NAME      select session group NAME
+    -x NAME      exclude session NAME and all descendants
+
+  Explore the structure of Isabelle sessions and print result names in
+  topological order (on stdout).
+""",
+      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+      "R" -> (_ => requirements = true),
+      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+      "a" -> (_ => all_sessions = 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)))
+
+    val sessions = getopts(args)
+
+    val options = Options.init()
+
+    val selection =
+      Selection(requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions,
+        exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions,
+        session_groups = session_groups, sessions = sessions)
+    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)
+    }
+  })
+
+
 
   /** heap file with SHA1 digest **/