# HG changeset patch # User wenzelm # Date 1527539110 -7200 # Node ID 119fc05f6b008c8091465e4d25102214f0a5d585 # Parent 812546f20c5cde45c308b2d4d789bfe00d0006bf support to dump build database produced by PIDE session; diff -r 812546f20c5c -r 119fc05f6b00 src/Pure/System/isabelle_tool.scala --- 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, diff -r 812546f20c5c -r 119fc05f6b00 src/Pure/Tools/dump.scala --- /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) + }) +} diff -r 812546f20c5c -r 119fc05f6b00 src/Pure/build-jars --- 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