# HG changeset patch
# User wenzelm
# Date 1527861448 -7200
# Node ID 30d6ffd0ca071527903d3d413bcf7a8dfac62583
# Parent  2941e58318c728db2b7d03b6d04ea67bc2626629# Parent  2ac3a5c07dfae9c6bec3ae4088be0c00c243e975
merged

diff -r 2941e58318c7 -r 30d6ffd0ca07 NEWS
--- a/NEWS	Fri Jun 01 13:32:55 2018 +0200
+++ b/NEWS	Fri Jun 01 15:57:28 2018 +0200
@@ -380,6 +380,11 @@
 and concurrent use of theories, based on Isabelle/PIDE infrastructure.
 See also the "system" manual.
 
+* The command-line tool "dump" dumps information from the cumulative
+PIDE session database: many sessions may be loaded into a given logic
+image, results from all loaded theories are written to the output
+directory.
+
 * The command-line tool "isabelle update_comments" normalizes formal
 comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
 approximate the appearance in document output). This is more specific
diff -r 2941e58318c7 -r 30d6ffd0ca07 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Fri Jun 01 13:32:55 2018 +0200
+++ b/src/Doc/System/Sessions.thy	Fri Jun 01 15:57:28 2018 +0200
@@ -595,4 +595,85 @@
   own sub-directory hierarchy, using the session-qualified theory name.
 \<close>
 
+
+section \<open>Dump PIDE session database \label{sec:tool-dump}\<close>
+
+text \<open>
+  The @{tool_def "dump"} tool dumps information from the cumulative PIDE
+  session database (which is processed on the spot). Its command-line usage
+  is: @{verbatim [display]
+\<open>Usage: isabelle dump [OPTIONS] [SESSIONS ...]
+
+  Options are:
+    -A NAMES     dump named aspects (default: ...)
+    -B NAME      include session NAME and all descendants
+    -D DIR       include session directory and select its sessions
+    -O DIR       output directory for dumped files (default: "dump")
+    -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="HOL")
+    -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 cumulative PIDE session database, with the following aspects:
+    ...\<close>}
+
+  \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the
+  remaining command-line arguments specify sessions as in @{tool build}
+  (\secref{sec:tool-build}): the cumulative PIDE database of all their loaded
+  theories is dumped to the output directory of option \<^verbatim>\<open>-O\<close> (default: \<^verbatim>\<open>dump\<close>
+  in the current directory).
+
+  \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies a logic image for the underlying prover process:
+  its theories are not processed again, and their PIDE session database is
+  excluded from the dump. Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close> when building
+  the logic image (\secref{sec:tool-build}).
+
+  \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
+  (\secref{sec:tool-build}).
+
+  \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
+
+  \<^medskip> Option \<^verbatim>\<open>-A\<close> specifies named aspects of the dump, as a comma-separated
+  list. The default is to dump all known aspects, as given in the command-line
+  usage of the tool. The underlying Isabelle/Scala function
+  \<^verbatim>\<open>isabelle.Dump.dump()\<close> takes aspects as user-defined operations on the
+  final PIDE state and document version. This allows to imitate Prover IDE
+  rendering under program control.
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+  Dump all Isabelle/ZF sessions (which are rather small):
+  @{verbatim [display] \<open>isabelle dump -v -B ZF\<close>}
+
+  \<^smallskip>
+  Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, using main Isabelle/HOL
+  as starting point:
+  @{verbatim [display] \<open>isabelle dump -v -l HOL HOL-Analysis\<close>}
+
+  \<^smallskip>
+  Dump all sessions connected to HOL-Analysis, including a full bootstrap of
+  Isabelle/HOL from Isabelle/Pure:
+  @{verbatim [display] \<open>isabelle dump -v -l Pure -B HOL-Analysis\<close>}
+
+  This results in uniform PIDE markup for everything, except for the
+  Isabelle/Pure bootstrap process itself. Producing that on the spot requires
+  several GB of heap space, both for the Isabelle/Scala and Isabelle/ML
+  process (in 64bit mode). Here are some relevant settings (\secref{sec:boot})
+  for such ambitious applications:
+  @{verbatim [display]
+\<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
+ML_OPTIONS="--minheap 4G --maxheap 32G"
+\<close>}
+
+\<close>
+
 end
diff -r 2941e58318c7 -r 30d6ffd0ca07 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jun 01 13:32:55 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Jun 01 15:57:28 2018 +0200
@@ -22,10 +22,10 @@
   val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
     blob list * int -> Document_ID.command -> Token.T list -> eval -> eval
   type print
-  val print0: (unit -> unit) -> eval -> print
+  type print_fn = Toplevel.transition -> Toplevel.state -> unit
+  val print0: {pri: int, print_fn: print_fn} -> eval -> print
   val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
     eval -> print list -> print list option
-  type print_fn = Toplevel.transition -> Toplevel.state -> unit
   type print_function =
     {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
       {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
@@ -342,9 +342,9 @@
 
 in
 
-fun print0 e =
+fun print0 {pri, print_fn} =
   make_print ("", [serial_string ()])
-    {delay = NONE, pri = 0, persistent = true, strict = true, print_fn = fn _ => fn _ => e ()};
+    {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn};
 
 fun print command_visible command_overlays keywords command_name eval old_prints =
   let
diff -r 2941e58318c7 -r 30d6ffd0ca07 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Jun 01 13:32:55 2018 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Jun 01 15:57:28 2018 +0200
@@ -707,17 +707,20 @@
                     adjust_pos = Position.adjust_offsets adjust,
                     segments = segments};
                 in
-                  fn () =>
+                  fn _ =>
                     (Thy_Info.apply_presentation presentation_context thy;
                      commit_consolidated node)
                 end
-              else fn () => commit_consolidated node;
+              else fn _ => commit_consolidated node;
 
             val result_entry =
               (case lookup_entry node result_id of
                 NONE => err_undef "result command entry" result_id
               | SOME (eval, prints) =>
-                  (result_id, SOME (eval, Command.print0 consolidation eval :: prints)));
+                  let
+                    val print = eval |> Command.print0
+                      {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation};
+                  in (result_id, SOME (eval, print :: prints)) end);
 
             val assign_update' = assign_update |> assign_update_change result_entry;
             val node' = node |> assign_entry result_entry;
diff -r 2941e58318c7 -r 30d6ffd0ca07 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Jun 01 13:32:55 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Jun 01 15:57:28 2018 +0200
@@ -60,6 +60,8 @@
 
   /** theory content **/
 
+  val export_prefix: String = "theory/"
+
   sealed case class Theory(name: String, parents: List[String],
     types: List[Type],
     consts: List[Const],
@@ -100,7 +102,7 @@
     cache: Option[Term.Cache] = None): Theory =
   {
     val parents =
-      Export.read_entry(db, session_name, theory_name, "theory/parents") match {
+      Export.read_entry(db, session_name, theory_name, export_prefix + "parents") match {
         case Some(entry) => split_lines(entry.uncompressed().text)
         case None =>
           error("Missing theory export in session " + quote(session_name) + ": " +
@@ -147,7 +149,7 @@
   def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
     export_name: String, decode: XML.Body => List[A]): List[A] =
   {
-    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
+    Export.read_entry(db, session_name, theory_name, export_prefix + export_name) match {
       case Some(entry) => decode(entry.uncompressed_yxml())
       case None => Nil
     }
diff -r 2941e58318c7 -r 30d6ffd0ca07 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Jun 01 13:32:55 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Jun 01 15:57:28 2018 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Tools/dump.scala
     Author:     Makarius
 
-Dump build database produced by PIDE session.
+Dump cumulative PIDE session database.
 */
 
 package isabelle
@@ -14,41 +14,62 @@
   sealed case class Aspect_Args(
     options: Options, progress: Progress, output_dir: Path, result: Thy_Resources.Theories_Result)
   {
-    def write(node_name: Document.Node.Name, file_name: String, bytes: Bytes)
+    def write(node_name: Document.Node.Name, file_name: Path, bytes: Bytes)
     {
-      val path = output_dir + Path.basic(node_name.theory) + Path.basic(file_name)
+      val path = output_dir + Path.basic(node_name.theory) + file_name
       Isabelle_System.mkdirs(path.dir)
       Bytes.write(path, bytes)
     }
 
-    def write(node_name: Document.Node.Name, file_name: String, text: String): Unit =
+    def write(node_name: Document.Node.Name, file_name: Path, text: String): Unit =
       write(node_name, file_name, Bytes(text))
 
-    def write(node_name: Document.Node.Name, file_name: String, body: XML.Body): Unit =
+    def write(node_name: Document.Node.Name, file_name: Path, body: XML.Body): Unit =
       write(node_name, file_name, Symbol.encode(YXML.string_of_body(body)))
   }
 
-  sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit)
+  sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
+    options: List[String] = Nil)
+  {
+    override def toString: String = name
+  }
 
-  private val known_aspects =
+  val known_aspects =
     List(
       Aspect("messages", "output messages (YXML format)",
         { case args =>
             for (node_name <- args.result.node_names) {
-              args.write(node_name, "messages.yxml",
+              args.write(node_name, Path.explode("messages.yxml"),
                 args.result.messages(node_name).iterator.map(_._1).toList)
             }
         }),
       Aspect("markup", "PIDE markup (YXML format)",
         { case args =>
             for (node_name <- args.result.node_names) {
-              args.write(node_name, "markup.yxml", args.result.markup_to_XML(node_name))
+              args.write(node_name, Path.explode("markup.yxml"),
+                args.result.markup_to_XML(node_name))
             }
-        })
-    )
+        }),
+      Aspect("latex", "generated LaTeX source",
+        { case args =>
+            for {
+              node_name <- args.result.node_names
+              entry <- args.result.exports(node_name)
+              if entry.name == "document.tex"
+            } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
+        }, options = List("editor_presentation")),
+      Aspect("theory", "foundational theory content",
+        { case args =>
+            for {
+              node_name <- args.result.node_names
+              entry <- args.result.exports(node_name)
+              if entry.name.startsWith(Export_Theory.export_prefix)
+            } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
+        }, options = List("editor_presentation", "export_theory"))
+    ).sortBy(_.name)
 
   def show_aspects: String =
-    cat_lines(known_aspects.sortBy(_.name).map(aspect => aspect.name + " - " + aspect.description))
+    cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
 
   def the_aspect(name: String): Aspect =
     known_aspects.find(aspect => aspect.name == name) getOrElse
@@ -73,7 +94,9 @@
     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 dump_options =
+      (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
+        { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
 
 
     /* dependencies */
@@ -112,9 +135,9 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("dump", "dump build database produced by PIDE session.", args =>
+    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
     {
-      var aspects: List[Aspect] = Nil
+      var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
       var output_dir = default_output_dir
@@ -133,7 +156,7 @@
 Usage: isabelle dump [OPTIONS] [SESSIONS ...]
 
   Options are:
-    -A NAMES     dump named aspects (comma-separated list, see below)
+    -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
@@ -148,8 +171,7 @@
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
-  Dump build database produced by PIDE session. The following dump aspects
-  are known (option -A):
+  Dump cumulative PIDE session database, with the following aspects:
 
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),