support to dump build database produced by PIDE session;

--- a/src/Pure/System/isabelle_tool.scala	Mon May 28 21:29:03 2018 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Mon May 28 22:25:10 2018 +0200
@@ -109,6 +109,7 @@
       Build_Status.isabelle_tool,
       Check_Sources.isabelle_tool,
       Doc.isabelle_tool,
+      Dump.isabelle_tool,
       Export.isabelle_tool,
       Imports.isabelle_tool,
       Mkroot.isabelle_tool,

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/dump.scala	Mon May 28 22:25:10 2018 +0200
@@ -0,0 +1,125 @@
+/*  Title:      Pure/Tools/dump.scala
+    Author:     Makarius
+
+Dump build database produced by PIDE session.
+*/
+
+package isabelle
+
+
+object Dump
+{
+  def dump(options: Options, logic: String,
+    consume: Thy_Resources.Theories_Result => Unit = _ => (),
+    progress: Progress = No_Progress,
+    log: Logger = No_Logger,
+    dirs: List[Path] = Nil,
+    select_dirs: List[Path] = Nil,
+    verbose: Boolean = false,
+    system_mode: Boolean = false,
+    selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
+  {
+    if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
+      system_mode = system_mode) != 0) error(logic + " FAILED")
+
+    val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false)
+
+    val deps =
+      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
+        selection_deps(selection)
+
+    val session =
+      Thy_Resources.start_session(dump_options, logic, session_dirs = dirs,
+        include_sessions = deps.sessions_structure.imports_topological_order,
+        progress = progress, log = log)
+
+    val theories = deps.all_known.theory_graph.topological_order.map(_.theory)
+    val theories_result = session.use_theories(theories, progress = progress)
+
+    try { consume(theories_result) }
+    catch { case exn: Throwable => session.stop (); throw exn }
+
+    session.stop()
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("dump", "dump build database produced by PIDE session.", 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 logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+      var options = Options.init()
+      var system_mode = false
+      var verbose = false
+      var exclude_sessions: List[String] = Nil
+
+      val getopts = Getopts("""
+Usage: isabelle dump [OPTIONS] [SESSIONS ...]
+
+  Options are:
+    -B NAME      include session NAME and all descendants
+    -D DIR       include session directory and select its sessions
+    -R           operate on 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
+    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -s           system build mode for logic image
+    -v           verbose
+    -x NAME      exclude session NAME and all descendants
+
+  Dump build database (PIDE markup etc.) based on dynamic session.""",
+      "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))),
+      "l:" -> (arg => logic = arg),
+      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+      "o:" -> (arg => options = options + arg),
+      "s" -> (_ => system_mode = true),
+      "v" -> (_ => verbose = true),
+      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+
+      val sessions = getopts(args)
+
+      val progress = new Console_Progress(verbose = verbose)
+
+      def consume(theories_result: Thy_Resources.Theories_Result)
+      {
+        // FIXME
+        for ((node, _) <- theories_result.nodes) progress.echo(node.toString)
+      }
+
+      val result =
+        dump(options, logic,
+          consume = consume _,
+          progress = progress,
+          dirs = dirs,
+          select_dirs = select_dirs,
+          verbose = verbose,
+          selection = Sessions.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))
+
+      progress.echo(result.timing.message_resources)
+
+      sys.exit(result.rc)
+    })
+}

--- a/src/Pure/build-jars	Mon May 28 21:29:03 2018 +0200
+++ b/src/Pure/build-jars	Mon May 28 22:25:10 2018 +0200
@@ -137,6 +137,7 @@
   Thy/thy_header.scala
   Thy/thy_resources.scala
   Thy/thy_syntax.scala
+  Tools/dump.scala
   Tools/build.scala
   Tools/build_docker.scala
   Tools/check_keywords.scala