src/Pure/Tools/dump.scala
author wenzelm
Mon Jun 11 15:50:28 2018 +0200 (12 months ago)
changeset 68416 33114721ac9a
parent 68365 f9379279f98c
child 68491 f0f83ce0badd
permissions -rw-r--r--
tuned signature;
wenzelm@68308
     1
/*  Title:      Pure/Tools/dump.scala
wenzelm@68308
     2
    Author:     Makarius
wenzelm@68308
     3
wenzelm@68348
     4
Dump cumulative PIDE session database.
wenzelm@68308
     5
*/
wenzelm@68308
     6
wenzelm@68308
     7
package isabelle
wenzelm@68308
     8
wenzelm@68308
     9
wenzelm@68308
    10
object Dump
wenzelm@68308
    11
{
wenzelm@68316
    12
  /* aspects */
wenzelm@68316
    13
wenzelm@68316
    14
  sealed case class Aspect_Args(
wenzelm@68355
    15
    options: Options,
wenzelm@68355
    16
    progress: Progress,
wenzelm@68365
    17
    deps: Sessions.Deps,
wenzelm@68355
    18
    output_dir: Path,
wenzelm@68365
    19
    node_name: Document.Node.Name,
wenzelm@68365
    20
    node_status: Protocol.Node_Status,
wenzelm@68365
    21
    snapshot: Document.Snapshot)
wenzelm@68319
    22
  {
wenzelm@68365
    23
    def write(file_name: Path, bytes: Bytes)
wenzelm@68319
    24
    {
wenzelm@68347
    25
      val path = output_dir + Path.basic(node_name.theory) + file_name
wenzelm@68319
    26
      Isabelle_System.mkdirs(path.dir)
wenzelm@68319
    27
      Bytes.write(path, bytes)
wenzelm@68319
    28
    }
wenzelm@68319
    29
wenzelm@68365
    30
    def write(file_name: Path, text: String): Unit =
wenzelm@68365
    31
      write(file_name, Bytes(text))
wenzelm@68332
    32
wenzelm@68365
    33
    def write(file_name: Path, body: XML.Body): Unit =
wenzelm@68365
    34
      write(file_name, Symbol.encode(YXML.string_of_body(body)))
wenzelm@68319
    35
  }
wenzelm@68316
    36
wenzelm@68347
    37
  sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
wenzelm@68347
    38
    options: List[String] = Nil)
wenzelm@68345
    39
  {
wenzelm@68345
    40
    override def toString: String = name
wenzelm@68345
    41
  }
wenzelm@68316
    42
wenzelm@68347
    43
  val known_aspects =
wenzelm@68316
    44
    List(
wenzelm@68365
    45
      Aspect("markup", "PIDE markup (YXML format)",
wenzelm@68365
    46
        { case args =>
wenzelm@68365
    47
            args.write(Path.explode("markup.yxml"),
wenzelm@68365
    48
              args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
wenzelm@68365
    49
        }),
wenzelm@68319
    50
      Aspect("messages", "output messages (YXML format)",
wenzelm@68319
    51
        { case args =>
wenzelm@68365
    52
            args.write(Path.explode("messages.yxml"),
wenzelm@68365
    53
              args.snapshot.messages.iterator.map(_._1).toList)
wenzelm@68347
    54
        }),
wenzelm@68347
    55
      Aspect("latex", "generated LaTeX source",
wenzelm@68347
    56
        { case args =>
wenzelm@68365
    57
            for (entry <- args.snapshot.exports if entry.name == "document.tex")
wenzelm@68365
    58
              args.write(Path.explode(entry.name), entry.uncompressed())
wenzelm@68347
    59
        }, options = List("editor_presentation")),
wenzelm@68347
    60
      Aspect("theory", "foundational theory content",
wenzelm@68347
    61
        { case args =>
wenzelm@68347
    62
            for {
wenzelm@68365
    63
              entry <- args.snapshot.exports
wenzelm@68347
    64
              if entry.name.startsWith(Export_Theory.export_prefix)
wenzelm@68365
    65
            } args.write(Path.explode(entry.name), entry.uncompressed())
wenzelm@68347
    66
        }, options = List("editor_presentation", "export_theory"))
wenzelm@68345
    67
    ).sortBy(_.name)
wenzelm@68316
    68
wenzelm@68316
    69
  def show_aspects: String =
wenzelm@68345
    70
    cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
wenzelm@68316
    71
wenzelm@68316
    72
  def the_aspect(name: String): Aspect =
wenzelm@68316
    73
    known_aspects.find(aspect => aspect.name == name) getOrElse
wenzelm@68316
    74
      error("Unknown aspect " + quote(name))
wenzelm@68316
    75
wenzelm@68316
    76
wenzelm@68316
    77
  /* dump */
wenzelm@68316
    78
wenzelm@68316
    79
  val default_output_dir = Path.explode("dump")
wenzelm@68316
    80
wenzelm@68416
    81
  def make_options(options: Options, aspects: List[Aspect]): Options =
wenzelm@68416
    82
    (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
wenzelm@68416
    83
      { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
wenzelm@68416
    84
wenzelm@68308
    85
  def dump(options: Options, logic: String,
wenzelm@68316
    86
    aspects: List[Aspect] = Nil,
wenzelm@68308
    87
    progress: Progress = No_Progress,
wenzelm@68308
    88
    log: Logger = No_Logger,
wenzelm@68308
    89
    dirs: List[Path] = Nil,
wenzelm@68308
    90
    select_dirs: List[Path] = Nil,
wenzelm@68316
    91
    output_dir: Path = default_output_dir,
wenzelm@68308
    92
    verbose: Boolean = false,
wenzelm@68308
    93
    system_mode: Boolean = false,
wenzelm@68308
    94
    selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
wenzelm@68308
    95
  {
wenzelm@68308
    96
    if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
wenzelm@68308
    97
      system_mode = system_mode) != 0) error(logic + " FAILED")
wenzelm@68308
    98
wenzelm@68416
    99
    val dump_options = make_options(options, aspects)
wenzelm@68308
   100
wenzelm@68318
   101
wenzelm@68318
   102
    /* dependencies */
wenzelm@68318
   103
wenzelm@68308
   104
    val deps =
wenzelm@68308
   105
      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
wenzelm@68308
   106
        selection_deps(selection)
wenzelm@68308
   107
wenzelm@68318
   108
    val include_sessions =
wenzelm@68318
   109
      deps.sessions_structure.imports_topological_order
wenzelm@68318
   110
wenzelm@68318
   111
    val use_theories =
wenzelm@68318
   112
      deps.sessions_structure.build_topological_order.
wenzelm@68318
   113
        flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
wenzelm@68318
   114
wenzelm@68318
   115
wenzelm@68318
   116
    /* session */
wenzelm@68318
   117
wenzelm@68308
   118
    val session =
wenzelm@68308
   119
      Thy_Resources.start_session(dump_options, logic, session_dirs = dirs,
wenzelm@68318
   120
        include_sessions = include_sessions, progress = progress, log = log)
wenzelm@68308
   121
wenzelm@68320
   122
    val theories_result = session.use_theories(use_theories, progress = progress)
wenzelm@68320
   123
    val session_result = session.stop()
wenzelm@68320
   124
wenzelm@68320
   125
wenzelm@68320
   126
    /* dump aspects */
wenzelm@68320
   127
wenzelm@68365
   128
    for ((node_name, node_status) <- theories_result.nodes) {
wenzelm@68365
   129
      val snapshot = theories_result.snapshot(node_name)
wenzelm@68365
   130
      val aspect_args =
wenzelm@68365
   131
        Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot)
wenzelm@68365
   132
      aspects.foreach(_.operation(aspect_args))
wenzelm@68365
   133
    }
wenzelm@68320
   134
wenzelm@68320
   135
    session_result
wenzelm@68308
   136
  }
wenzelm@68308
   137
wenzelm@68308
   138
wenzelm@68308
   139
  /* Isabelle tool wrapper */
wenzelm@68308
   140
wenzelm@68308
   141
  val isabelle_tool =
wenzelm@68348
   142
    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
wenzelm@68308
   143
    {
wenzelm@68345
   144
      var aspects: List[Aspect] = known_aspects
wenzelm@68308
   145
      var base_sessions: List[String] = Nil
wenzelm@68308
   146
      var select_dirs: List[Path] = Nil
wenzelm@68316
   147
      var output_dir = default_output_dir
wenzelm@68308
   148
      var requirements = false
wenzelm@68308
   149
      var exclude_session_groups: List[String] = Nil
wenzelm@68308
   150
      var all_sessions = false
wenzelm@68308
   151
      var dirs: List[Path] = Nil
wenzelm@68308
   152
      var session_groups: List[String] = Nil
wenzelm@68308
   153
      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
wenzelm@68308
   154
      var options = Options.init()
wenzelm@68308
   155
      var system_mode = false
wenzelm@68308
   156
      var verbose = false
wenzelm@68308
   157
      var exclude_sessions: List[String] = Nil
wenzelm@68308
   158
wenzelm@68308
   159
      val getopts = Getopts("""
wenzelm@68308
   160
Usage: isabelle dump [OPTIONS] [SESSIONS ...]
wenzelm@68308
   161
wenzelm@68308
   162
  Options are:
wenzelm@68345
   163
    -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
wenzelm@68308
   164
    -B NAME      include session NAME and all descendants
wenzelm@68308
   165
    -D DIR       include session directory and select its sessions
wenzelm@68316
   166
    -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
wenzelm@68308
   167
    -R           operate on requirements of selected sessions
wenzelm@68308
   168
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@68308
   169
    -a           select all sessions
wenzelm@68308
   170
    -d DIR       include session directory
wenzelm@68308
   171
    -g NAME      select session group NAME
wenzelm@68308
   172
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
wenzelm@68308
   173
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@68308
   174
    -s           system build mode for logic image
wenzelm@68308
   175
    -v           verbose
wenzelm@68308
   176
    -x NAME      exclude session NAME and all descendants
wenzelm@68308
   177
wenzelm@68348
   178
  Dump cumulative PIDE session database, with the following aspects:
wenzelm@68316
   179
wenzelm@68316
   180
""" + Library.prefix_lines("    ", show_aspects) + "\n",
wenzelm@68316
   181
      "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
wenzelm@68308
   182
      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
wenzelm@68308
   183
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
wenzelm@68316
   184
      "O:" -> (arg => output_dir = Path.explode(arg)),
wenzelm@68308
   185
      "R" -> (_ => requirements = true),
wenzelm@68308
   186
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
wenzelm@68308
   187
      "a" -> (_ => all_sessions = true),
wenzelm@68308
   188
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@68308
   189
      "l:" -> (arg => logic = arg),
wenzelm@68308
   190
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
wenzelm@68308
   191
      "o:" -> (arg => options = options + arg),
wenzelm@68308
   192
      "s" -> (_ => system_mode = true),
wenzelm@68308
   193
      "v" -> (_ => verbose = true),
wenzelm@68308
   194
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
wenzelm@68308
   195
wenzelm@68308
   196
      val sessions = getopts(args)
wenzelm@68308
   197
wenzelm@68308
   198
      val progress = new Console_Progress(verbose = verbose)
wenzelm@68308
   199
wenzelm@68308
   200
      val result =
wenzelm@68331
   201
        progress.interrupt_handler {
wenzelm@68331
   202
          dump(options, logic,
wenzelm@68331
   203
            aspects = aspects,
wenzelm@68331
   204
            progress = progress,
wenzelm@68331
   205
            dirs = dirs,
wenzelm@68331
   206
            select_dirs = select_dirs,
wenzelm@68331
   207
            output_dir = output_dir,
wenzelm@68331
   208
            verbose = verbose,
wenzelm@68331
   209
            selection = Sessions.Selection(
wenzelm@68331
   210
              requirements = requirements,
wenzelm@68331
   211
              all_sessions = all_sessions,
wenzelm@68331
   212
              base_sessions = base_sessions,
wenzelm@68331
   213
              exclude_session_groups = exclude_session_groups,
wenzelm@68331
   214
              exclude_sessions = exclude_sessions,
wenzelm@68331
   215
              session_groups = session_groups,
wenzelm@68331
   216
              sessions = sessions))
wenzelm@68331
   217
        }
wenzelm@68308
   218
wenzelm@68308
   219
      progress.echo(result.timing.message_resources)
wenzelm@68308
   220
wenzelm@68308
   221
      sys.exit(result.rc)
wenzelm@68308
   222
    })
wenzelm@68308
   223
}