src/Pure/Tools/dump.scala

support to dump build database produced by PIDE session;

/*  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)
    })
}