--- 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.
--- 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
--- 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,
--- 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 **/