src/Pure/Tools/dump.scala
author wenzelm
Sat, 07 Sep 2019 14:50:38 +0200
changeset 70670 a1dfd603260e
parent 70659 44588e355ca8
child 70687 086575316fd5
permissions -rw-r--r--
disable fragile options for now;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/dump.scala
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
     3
68348
2ac3a5c07dfa documentation for "isabelle dump";
wenzelm
parents: 68347
diff changeset
     4
Dump cumulative PIDE session database.
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
     5
*/
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
     6
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
     7
package isabelle
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
     8
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
     9
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
    10
object Dump
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
    11
{
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    12
  /* aspects */
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    13
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    14
  sealed case class Aspect_Args(
68355
67a4db47e4f6 more args;
wenzelm
parents: 68348
diff changeset
    15
    options: Options,
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    16
    deps: Sessions.Deps,
68355
67a4db47e4f6 more args;
wenzelm
parents: 68348
diff changeset
    17
    progress: Progress,
69896
be7243b97c41 tuned signature;
wenzelm
parents: 69857
diff changeset
    18
    output_dir: Path,
68929
10cbb5d99081 tuned signature;
wenzelm
parents: 68927
diff changeset
    19
    snapshot: Document.Snapshot,
69534
913970ae2324 tuned, according to Isabelle/MMT;
wenzelm
parents: 69533
diff changeset
    20
    status: Document_Status.Node_Status)
68319
2e168460a9c3 more operations;
wenzelm
parents: 68318
diff changeset
    21
  {
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    22
    def write(file_name: Path, bytes: Bytes)
68319
2e168460a9c3 more operations;
wenzelm
parents: 68318
diff changeset
    23
    {
68929
10cbb5d99081 tuned signature;
wenzelm
parents: 68927
diff changeset
    24
      val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name
68319
2e168460a9c3 more operations;
wenzelm
parents: 68318
diff changeset
    25
      Isabelle_System.mkdirs(path.dir)
2e168460a9c3 more operations;
wenzelm
parents: 68318
diff changeset
    26
      Bytes.write(path, bytes)
2e168460a9c3 more operations;
wenzelm
parents: 68318
diff changeset
    27
    }
2e168460a9c3 more operations;
wenzelm
parents: 68318
diff changeset
    28
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    29
    def write(file_name: Path, text: String): Unit =
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    30
      write(file_name, Bytes(text))
68332
7cb681615d0e store Isabelle symbols in canonical form;
wenzelm
parents: 68331
diff changeset
    31
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    32
    def write(file_name: Path, body: XML.Body): Unit =
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    33
      write(file_name, Symbol.encode(YXML.string_of_body(body)))
68319
2e168460a9c3 more operations;
wenzelm
parents: 68318
diff changeset
    34
  }
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    35
68347
9e6e7ab77434 more dump aspects, with options;
wenzelm
parents: 68345
diff changeset
    36
  sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
9e6e7ab77434 more dump aspects, with options;
wenzelm
parents: 68345
diff changeset
    37
    options: List[String] = Nil)
68345
5bc1e1ac7955 clarified default: all aspects;
wenzelm
parents: 68332
diff changeset
    38
  {
5bc1e1ac7955 clarified default: all aspects;
wenzelm
parents: 68332
diff changeset
    39
    override def toString: String = name
5bc1e1ac7955 clarified default: all aspects;
wenzelm
parents: 68332
diff changeset
    40
  }
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    41
69521
wenzelm
parents: 69520
diff changeset
    42
  val known_aspects: List[Aspect] =
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    43
    List(
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    44
      Aspect("markup", "PIDE markup (YXML format)",
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    45
        { case args =>
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    46
            args.write(Path.explode("markup.yxml"),
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    47
              args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    48
        }),
68319
2e168460a9c3 more operations;
wenzelm
parents: 68318
diff changeset
    49
      Aspect("messages", "output messages (YXML format)",
2e168460a9c3 more operations;
wenzelm
parents: 68318
diff changeset
    50
        { case args =>
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    51
            args.write(Path.explode("messages.yxml"),
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    52
              args.snapshot.messages.iterator.map(_._1).toList)
68347
9e6e7ab77434 more dump aspects, with options;
wenzelm
parents: 68345
diff changeset
    53
        }),
9e6e7ab77434 more dump aspects, with options;
wenzelm
parents: 68345
diff changeset
    54
      Aspect("latex", "generated LaTeX source",
9e6e7ab77434 more dump aspects, with options;
wenzelm
parents: 68345
diff changeset
    55
        { case args =>
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    56
            for (entry <- args.snapshot.exports if entry.name == "document.tex")
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    57
              args.write(Path.explode(entry.name), entry.uncompressed())
69533
1d2e6a4e073f clarified options: ensure consolidated Node_Status and thus percentage = 100% for progress;
wenzelm
parents: 69532
diff changeset
    58
        }, options = List("export_document")),
68347
9e6e7ab77434 more dump aspects, with options;
wenzelm
parents: 68345
diff changeset
    59
      Aspect("theory", "foundational theory content",
9e6e7ab77434 more dump aspects, with options;
wenzelm
parents: 68345
diff changeset
    60
        { case args =>
9e6e7ab77434 more dump aspects, with options;
wenzelm
parents: 68345
diff changeset
    61
            for {
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    62
              entry <- args.snapshot.exports
68347
9e6e7ab77434 more dump aspects, with options;
wenzelm
parents: 68345
diff changeset
    63
              if entry.name.startsWith(Export_Theory.export_prefix)
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68355
diff changeset
    64
            } args.write(Path.explode(entry.name), entry.uncompressed())
69533
1d2e6a4e073f clarified options: ensure consolidated Node_Status and thus percentage = 100% for progress;
wenzelm
parents: 69532
diff changeset
    65
        }, options = List("export_theory"))
68345
5bc1e1ac7955 clarified default: all aspects;
wenzelm
parents: 68332
diff changeset
    66
    ).sortBy(_.name)
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    67
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    68
  def show_aspects: String =
68345
5bc1e1ac7955 clarified default: all aspects;
wenzelm
parents: 68332
diff changeset
    69
    cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    70
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    71
  def the_aspect(name: String): Aspect =
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    72
    known_aspects.find(aspect => aspect.name == name) getOrElse
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    73
      error("Unknown aspect " + quote(name))
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    74
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
    75
69538
faf547d2834c clarified signature, notably cascade of dump_options, deps, resources, session;
wenzelm
parents: 69537
diff changeset
    76
  /* session */
faf547d2834c clarified signature, notably cascade of dump_options, deps, resources, session;
wenzelm
parents: 69537
diff changeset
    77
69896
be7243b97c41 tuned signature;
wenzelm
parents: 69857
diff changeset
    78
  sealed case class Args(
69897
a9849222844d tuned signature;
wenzelm
parents: 69896
diff changeset
    79
    session: Headless.Session,
a9849222844d tuned signature;
wenzelm
parents: 69896
diff changeset
    80
    snapshot: Document.Snapshot,
a9849222844d tuned signature;
wenzelm
parents: 69896
diff changeset
    81
    status: Document_Status.Node_Status)
69896
be7243b97c41 tuned signature;
wenzelm
parents: 69857
diff changeset
    82
  {
be7243b97c41 tuned signature;
wenzelm
parents: 69857
diff changeset
    83
    def print_node: String = snapshot.node_name.toString
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    84
  }
69896
be7243b97c41 tuned signature;
wenzelm
parents: 69857
diff changeset
    85
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    86
  object Session
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    87
  {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    88
    def apply(
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    89
      options: Options,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    90
      logic: String,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    91
      aspects: List[Aspect] = Nil,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    92
      progress: Progress = No_Progress,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    93
      log: Logger = No_Logger,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    94
      dirs: List[Path] = Nil,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    95
      select_dirs: List[Path] = Nil,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    96
      selection: Sessions.Selection = Sessions.Selection.empty): Session =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    97
    {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    98
      new Session(options, logic, aspects, progress, log, dirs, select_dirs, selection)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
    99
    }
69896
be7243b97c41 tuned signature;
wenzelm
parents: 69857
diff changeset
   100
  }
be7243b97c41 tuned signature;
wenzelm
parents: 69857
diff changeset
   101
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   102
  class Session private(
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   103
    options: Options,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   104
    logic: String,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   105
    aspects: List[Aspect],
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   106
    progress: Progress,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   107
    log: Logger,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   108
    dirs: List[Path],
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   109
    select_dirs: List[Path],
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   110
    selection: Sessions.Selection)
69538
faf547d2834c clarified signature, notably cascade of dump_options, deps, resources, session;
wenzelm
parents: 69537
diff changeset
   111
  {
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   112
    /* context */
69897
a9849222844d tuned signature;
wenzelm
parents: 69896
diff changeset
   113
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   114
    Build.build_logic(options, logic, build_heap = true, progress = progress,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   115
      dirs = dirs ::: select_dirs, strict = true)
68926
5129fcc1b6c0 dump aspects asynchronously;
wenzelm
parents: 68899
diff changeset
   116
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   117
    val dump_options: Options =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   118
    {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   119
      val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   120
      val options1 =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   121
        options0 +
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   122
          "completion_limit=0" +
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   123
          "ML_statistics=false" +
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   124
          "parallel_proofs=0" +
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   125
          "editor_tracing_messages=0" +
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   126
          "editor_presentation" +
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   127
          "execution_eager"
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   128
      (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   129
    }
68926
5129fcc1b6c0 dump aspects asynchronously;
wenzelm
parents: 68899
diff changeset
   130
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   131
    val deps: Sessions.Deps =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   132
      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   133
        selection_deps(dump_options, selection, progress = progress,
70659
44588e355ca8 more robust;
wenzelm
parents: 70655
diff changeset
   134
          uniform_session = true, loading_sessions = true).check_errors
68926
5129fcc1b6c0 dump aspects asynchronously;
wenzelm
parents: 68899
diff changeset
   135
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   136
    val resources: Headless.Resources =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   137
      Headless.Resources.make(dump_options, logic, progress = progress, log = log,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   138
        session_dirs = dirs ::: select_dirs,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   139
        include_sessions = deps.sessions_structure.imports_topological_order)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   140
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   141
    val used_theories: List[Document.Node.Name] =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   142
    {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   143
      for {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   144
        name <- deps.used_theories_condition(dump_options, progress = progress).topological_order
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   145
        if !resources.session_base.loaded_theory(name.theory)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   146
      } yield name
68926
5129fcc1b6c0 dump aspects asynchronously;
wenzelm
parents: 68899
diff changeset
   147
    }
5129fcc1b6c0 dump aspects asynchronously;
wenzelm
parents: 68899
diff changeset
   148
5129fcc1b6c0 dump aspects asynchronously;
wenzelm
parents: 68899
diff changeset
   149
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   150
    /* run */
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   151
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   152
    def run(process_theory: Args => Unit, unicode_symbols: Boolean = false)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   153
    {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   154
      val session = resources.start_session(progress = progress)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   155
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   156
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   157
      // asynchronous consumer
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   158
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   159
      object Consumer
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   160
      {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   161
        sealed case class Bad_Theory(
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   162
          name: Document.Node.Name,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   163
          status: Document_Status.Node_Status,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   164
          errors: List[String])
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   165
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   166
        private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory])
68318
5971199863ea more accurate dependencies;
wenzelm
parents: 68316
diff changeset
   167
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   168
        private val consumer =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   169
          Consumer_Thread.fork(name = "dump")(
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   170
            consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   171
              {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   172
                val (snapshot, status) = args
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   173
                val name = snapshot.node_name
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   174
                if (status.ok) {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   175
                  try { process_theory(Args(session, snapshot, status)) }
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   176
                  catch {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   177
                    case exn: Throwable if !Exn.is_interrupt(exn) =>
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   178
                    val msg = Exn.message(exn)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   179
                    progress.echo("FAILED to process theory " + name)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   180
                    progress.echo_error_message(msg)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   181
                    consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   182
                  }
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   183
                }
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   184
                else {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   185
                  val msgs =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   186
                    for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   187
                    yield {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   188
                      "Error" + Position.here(pos) + ":\n" +
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   189
                        XML.content(Pretty.formatted(List(tree)))
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   190
                    }
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   191
                  progress.echo("FAILED to process theory " + name)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   192
                  msgs.foreach(progress.echo_error_message)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   193
                  consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   194
                }
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   195
                true
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   196
              })
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   197
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   198
        def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   199
          consumer.send((snapshot, status))
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   200
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   201
        def shutdown(): List[Bad_Theory] =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   202
        {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   203
          consumer.shutdown()
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   204
          consumer_bad_theories.value.reverse
70634
0f8742b5a9e8 more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
wenzelm
parents: 70626
diff changeset
   205
        }
0f8742b5a9e8 more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
wenzelm
parents: 70626
diff changeset
   206
      }
0f8742b5a9e8 more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
wenzelm
parents: 70626
diff changeset
   207
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   208
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70645
diff changeset
   209
      // synchronous body
68320
1d33697199c1 shutdown ML process before output: Theories_Result is timeless/stateless;
wenzelm
parents: 68319
diff changeset
   210
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   211
      try {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   212
        val use_theories_result =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   213
          session.use_theories(used_theories.map(_.theory),
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   214
            unicode_symbols = unicode_symbols,
70670
a1dfd603260e disable fragile options for now;
wenzelm
parents: 70659
diff changeset
   215
            share_common_data = false /* FIXME true */,
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   216
            progress = progress,
70670
a1dfd603260e disable fragile options for now;
wenzelm
parents: 70659
diff changeset
   217
            checkpoints = Set.empty /* FIXME deps.dump_checkpoints */,
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70645
diff changeset
   218
            commit = Some(Consumer.apply _))
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   219
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   220
        val bad_theories = Consumer.shutdown()
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   221
        val bad_msgs =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   222
          bad_theories.map(bad =>
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   223
            Output.clean_yxml(
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   224
              "FAILED theory " + bad.name +
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   225
                (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") +
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   226
                (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", ""))))
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   227
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   228
        val pending_msgs =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   229
          use_theories_result.nodes_pending match {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   230
            case Nil => Nil
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   231
            case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString)))
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   232
          }
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   233
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   234
        val errors = bad_msgs ::: pending_msgs
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   235
        if (errors.nonEmpty) error(errors.mkString("\n\n"))
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   236
      }
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   237
      finally { session.stop() }
69032
90bb4cabe1e8 clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents: 69026
diff changeset
   238
    }
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   239
  }
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   240
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   241
69523
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   242
  /* dump */
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   243
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   244
  val default_output_dir: Path = Path.explode("dump")
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   245
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   246
  def dump(
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   247
    options: Options,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   248
    logic: String,
69523
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   249
    aspects: List[Aspect] = Nil,
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   250
    progress: Progress = No_Progress,
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   251
    log: Logger = No_Logger,
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   252
    dirs: List[Path] = Nil,
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   253
    select_dirs: List[Path] = Nil,
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   254
    output_dir: Path = default_output_dir,
69535
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   255
    selection: Sessions.Selection = Sessions.Selection.empty)
69523
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   256
  {
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   257
    val session =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   258
      Session(options, logic, aspects = aspects, progress = progress, log = log,
69856
bb41977edb7e tuned signature;
wenzelm
parents: 69854
diff changeset
   259
        dirs = dirs, select_dirs = select_dirs, selection = selection)
69523
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   260
70640
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   261
    session.run((args: Args) =>
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   262
      {
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   263
        progress.echo("Processing theory " + args.print_node + " ...")
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   264
        val aspect_args =
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   265
          Aspect_Args(session.dump_options, session.deps, progress, output_dir,
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   266
            args.snapshot, args.status)
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   267
        aspects.foreach(_.operation(aspect_args))
5f4b8a505090 more explicit type Dump.Session, with context information;
wenzelm
parents: 70634
diff changeset
   268
      })
69523
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   269
  }
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   270
9403ff523825 tuned signature: for other dump-like tools;
wenzelm
parents: 69522
diff changeset
   271
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   272
  /* Isabelle tool wrapper */
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   273
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   274
  val isabelle_tool =
68348
2ac3a5c07dfa documentation for "isabelle dump";
wenzelm
parents: 68347
diff changeset
   275
    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   276
    {
68345
5bc1e1ac7955 clarified default: all aspects;
wenzelm
parents: 68332
diff changeset
   277
      var aspects: List[Aspect] = known_aspects
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   278
      var base_sessions: List[String] = Nil
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   279
      var select_dirs: List[Path] = Nil
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
   280
      var output_dir = default_output_dir
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   281
      var requirements = false
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   282
      var exclude_session_groups: List[String] = Nil
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   283
      var all_sessions = false
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   284
      var dirs: List[Path] = Nil
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   285
      var session_groups: List[String] = Nil
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   286
      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   287
      var options = Options.init()
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   288
      var verbose = false
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   289
      var exclude_sessions: List[String] = Nil
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   290
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   291
      val getopts = Getopts("""
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   292
Usage: isabelle dump [OPTIONS] [SESSIONS ...]
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   293
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   294
  Options are:
68345
5bc1e1ac7955 clarified default: all aspects;
wenzelm
parents: 68332
diff changeset
   295
    -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   296
    -B NAME      include session NAME and all descendants
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   297
    -D DIR       include session directory and select its sessions
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
   298
    -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   299
    -R           operate on requirements of selected sessions
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   300
    -X NAME      exclude sessions from group NAME and all descendants
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   301
    -a           select all sessions
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   302
    -d DIR       include session directory
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   303
    -g NAME      select session group NAME
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   304
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   305
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   306
    -v           verbose
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   307
    -x NAME      exclude session NAME and all descendants
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   308
68348
2ac3a5c07dfa documentation for "isabelle dump";
wenzelm
parents: 68347
diff changeset
   309
  Dump cumulative PIDE session database, with the following aspects:
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
   310
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
   311
""" + Library.prefix_lines("    ", show_aspects) + "\n",
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
   312
      "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   313
      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   314
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
68316
a1e5de3681f0 more formal dump aspects;
wenzelm
parents: 68308
diff changeset
   315
      "O:" -> (arg => output_dir = Path.explode(arg)),
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   316
      "R" -> (_ => requirements = true),
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   317
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   318
      "a" -> (_ => all_sessions = true),
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   319
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
68741
wenzelm
parents: 68557
diff changeset
   320
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   321
      "l:" -> (arg => logic = arg),
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   322
      "o:" -> (arg => options = options + arg),
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   323
      "v" -> (_ => verbose = true),
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   324
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   325
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   326
      val sessions = getopts(args)
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   327
68951
a7b1fe2d30ad more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session;
wenzelm
parents: 68948
diff changeset
   328
      val progress = new Console_Progress(verbose = verbose)
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   329
69535
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   330
      progress.interrupt_handler {
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   331
        dump(options, logic,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   332
          aspects = aspects,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   333
          progress = progress,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   334
          dirs = dirs,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   335
          select_dirs = select_dirs,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   336
          output_dir = output_dir,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   337
          selection = Sessions.Selection(
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   338
            requirements = requirements,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   339
            all_sessions = all_sessions,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   340
            base_sessions = base_sessions,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   341
            exclude_session_groups = exclude_session_groups,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   342
            exclude_sessions = exclude_sessions,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   343
            session_groups = session_groups,
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   344
            sessions = sessions))
e3a9680d9ed8 clarified errors, according to Isabelle/MMT;
wenzelm
parents: 69534
diff changeset
   345
      }
68308
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   346
    })
119fc05f6b00 support to dump build database produced by PIDE session;
wenzelm
parents:
diff changeset
   347
}