support to dump build database produced by PIDE session;
authorwenzelm
Mon May 28 22:25:10 2018 +0200 (2018-05-28)
changeset 68308119fc05f6b00
parent 68307 812546f20c5c
child 68309 ce59ab0adfdd
support to dump build database produced by PIDE session;
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/dump.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/System/isabelle_tool.scala	Mon May 28 21:29:03 2018 +0200
     1.2 +++ b/src/Pure/System/isabelle_tool.scala	Mon May 28 22:25:10 2018 +0200
     1.3 @@ -109,6 +109,7 @@
     1.4        Build_Status.isabelle_tool,
     1.5        Check_Sources.isabelle_tool,
     1.6        Doc.isabelle_tool,
     1.7 +      Dump.isabelle_tool,
     1.8        Export.isabelle_tool,
     1.9        Imports.isabelle_tool,
    1.10        Mkroot.isabelle_tool,
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Tools/dump.scala	Mon May 28 22:25:10 2018 +0200
     2.3 @@ -0,0 +1,125 @@
     2.4 +/*  Title:      Pure/Tools/dump.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Dump build database produced by PIDE session.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Dump
    2.14 +{
    2.15 +  def dump(options: Options, logic: String,
    2.16 +    consume: Thy_Resources.Theories_Result => Unit = _ => (),
    2.17 +    progress: Progress = No_Progress,
    2.18 +    log: Logger = No_Logger,
    2.19 +    dirs: List[Path] = Nil,
    2.20 +    select_dirs: List[Path] = Nil,
    2.21 +    verbose: Boolean = false,
    2.22 +    system_mode: Boolean = false,
    2.23 +    selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
    2.24 +  {
    2.25 +    if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
    2.26 +      system_mode = system_mode) != 0) error(logic + " FAILED")
    2.27 +
    2.28 +    val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false)
    2.29 +
    2.30 +    val deps =
    2.31 +      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
    2.32 +        selection_deps(selection)
    2.33 +
    2.34 +    val session =
    2.35 +      Thy_Resources.start_session(dump_options, logic, session_dirs = dirs,
    2.36 +        include_sessions = deps.sessions_structure.imports_topological_order,
    2.37 +        progress = progress, log = log)
    2.38 +
    2.39 +    val theories = deps.all_known.theory_graph.topological_order.map(_.theory)
    2.40 +    val theories_result = session.use_theories(theories, progress = progress)
    2.41 +
    2.42 +    try { consume(theories_result) }
    2.43 +    catch { case exn: Throwable => session.stop (); throw exn }
    2.44 +
    2.45 +    session.stop()
    2.46 +  }
    2.47 +
    2.48 +
    2.49 +  /* Isabelle tool wrapper */
    2.50 +
    2.51 +  val isabelle_tool =
    2.52 +    Isabelle_Tool("dump", "dump build database produced by PIDE session.", args =>
    2.53 +    {
    2.54 +      var base_sessions: List[String] = Nil
    2.55 +      var select_dirs: List[Path] = Nil
    2.56 +      var requirements = false
    2.57 +      var exclude_session_groups: List[String] = Nil
    2.58 +      var all_sessions = false
    2.59 +      var dirs: List[Path] = Nil
    2.60 +      var session_groups: List[String] = Nil
    2.61 +      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    2.62 +      var options = Options.init()
    2.63 +      var system_mode = false
    2.64 +      var verbose = false
    2.65 +      var exclude_sessions: List[String] = Nil
    2.66 +
    2.67 +      val getopts = Getopts("""
    2.68 +Usage: isabelle dump [OPTIONS] [SESSIONS ...]
    2.69 +
    2.70 +  Options are:
    2.71 +    -B NAME      include session NAME and all descendants
    2.72 +    -D DIR       include session directory and select its sessions
    2.73 +    -R           operate on requirements of selected sessions
    2.74 +    -X NAME      exclude sessions from group NAME and all descendants
    2.75 +    -a           select all sessions
    2.76 +    -d DIR       include session directory
    2.77 +    -g NAME      select session group NAME
    2.78 +    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
    2.79 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.80 +    -s           system build mode for logic image
    2.81 +    -v           verbose
    2.82 +    -x NAME      exclude session NAME and all descendants
    2.83 +
    2.84 +  Dump build database (PIDE markup etc.) based on dynamic session.""",
    2.85 +      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
    2.86 +      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    2.87 +      "R" -> (_ => requirements = true),
    2.88 +      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    2.89 +      "a" -> (_ => all_sessions = true),
    2.90 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    2.91 +      "l:" -> (arg => logic = arg),
    2.92 +      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    2.93 +      "o:" -> (arg => options = options + arg),
    2.94 +      "s" -> (_ => system_mode = true),
    2.95 +      "v" -> (_ => verbose = true),
    2.96 +      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
    2.97 +
    2.98 +      val sessions = getopts(args)
    2.99 +
   2.100 +      val progress = new Console_Progress(verbose = verbose)
   2.101 +
   2.102 +      def consume(theories_result: Thy_Resources.Theories_Result)
   2.103 +      {
   2.104 +        // FIXME
   2.105 +        for ((node, _) <- theories_result.nodes) progress.echo(node.toString)
   2.106 +      }
   2.107 +
   2.108 +      val result =
   2.109 +        dump(options, logic,
   2.110 +          consume = consume _,
   2.111 +          progress = progress,
   2.112 +          dirs = dirs,
   2.113 +          select_dirs = select_dirs,
   2.114 +          verbose = verbose,
   2.115 +          selection = Sessions.Selection(
   2.116 +            requirements = requirements,
   2.117 +            all_sessions = all_sessions,
   2.118 +            base_sessions = base_sessions,
   2.119 +            exclude_session_groups = exclude_session_groups,
   2.120 +            exclude_sessions = exclude_sessions,
   2.121 +            session_groups = session_groups,
   2.122 +            sessions = sessions))
   2.123 +
   2.124 +      progress.echo(result.timing.message_resources)
   2.125 +
   2.126 +      sys.exit(result.rc)
   2.127 +    })
   2.128 +}
     3.1 --- a/src/Pure/build-jars	Mon May 28 21:29:03 2018 +0200
     3.2 +++ b/src/Pure/build-jars	Mon May 28 22:25:10 2018 +0200
     3.3 @@ -137,6 +137,7 @@
     3.4    Thy/thy_header.scala
     3.5    Thy/thy_resources.scala
     3.6    Thy/thy_syntax.scala
     3.7 +  Tools/dump.scala
     3.8    Tools/build.scala
     3.9    Tools/build_docker.scala
    3.10    Tools/check_keywords.scala