# HG changeset patch
# User wenzelm
# Date 1667744936 -3600
# Node ID 1f0b2d7298d9345599733d7c5e3c6975a7cc8ae8
# Parent  f65bb0ecc7e7bc450c66926ed19aeaad421a6298
afford unconditional presentation, notably export_theory and present_thy, notably for HTML + PDF presentation within PIDE;
typical timings for big theories in HOL-Analysis: Export.make_entry < 10ms, Document_Output.present_thy < 150ms;

diff -r f65bb0ecc7e7 -r 1f0b2d7298d9 etc/options
--- a/etc/options	Sun Nov 06 12:54:46 2022 +0100
+++ b/etc/options	Sun Nov 06 15:28:56 2022 +0100
@@ -178,9 +178,6 @@
 option build_pide_reports : bool = true
   -- "report PIDE markup (in batch build)"
 
-option pide_presentation : bool = false
-  -- "presentation of consolidated theories in PIDE"
-
 
 section "Editor Session"
 
diff -r f65bb0ecc7e7 -r 1f0b2d7298d9 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Nov 06 12:54:46 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Sun Nov 06 15:28:56 2022 +0100
@@ -774,32 +774,22 @@
 fun print_consolidation options the_command_span node_name (assign_update, node) =
   timeit "Document.print_consolidation" (fn () =>
     (case finished_result_theory node of
-      SOME (result_id, thy) =>
+      SOME (id, thy) =>
         if finished_eval node then
           let
-            fun commit_consolidated () =
-              (Lazy.force (get_consolidated node);
-               Output.status [Markup.markup_only Markup.consolidated]);
-            val consolidation =
-              if Options.bool options \<^system_option>\<open>pide_presentation\<close> then
-                let val context = presentation_context options the_command_span node_name node in
-                  fn _ =>
-                    let
-                      val _ = Output.status [Markup.markup_only Markup.consolidating];
-                      val res = Exn.capture (Thy_Info.apply_presentation context) thy;
-                      val _ = commit_consolidated ();
-                    in Exn.release res end
-                end
-              else fn _ => commit_consolidated ();
-
+            val context = presentation_context options the_command_span node_name node;
+            val pr =
+              {pri = Task_Queue.urgent_pri + 1, print_fn = fn _ => fn _ =>
+                let
+                  val _ = Output.status [Markup.markup_only Markup.consolidating];
+                  val res = Exn.capture (Thy_Info.apply_presentation context) thy;
+                  val _ = Lazy.force (get_consolidated node);
+                  val _ = Output.status [Markup.markup_only Markup.consolidated];
+                in Exn.release res end};
             val result_entry =
-              (case lookup_entry node result_id of
-                NONE => err_undef "result command entry" result_id
-              | SOME (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);
+              (case lookup_entry node id of
+                NONE => err_undef "result command entry" id
+              | SOME (eval, prints) => (id, SOME (eval, Command.print0 pr eval :: prints)));
 
             val assign_update' = assign_update |> assign_update_change result_entry;
             val node' = node |> assign_entry result_entry;
diff -r f65bb0ecc7e7 -r 1f0b2d7298d9 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sun Nov 06 12:54:46 2022 +0100
+++ b/src/Pure/Tools/dump.scala	Sun Nov 06 15:28:56 2022 +0100
@@ -102,7 +102,6 @@
           options0 +
             "parallel_proofs=0" +
             "completion_limit=0" +
-            "pide_presentation" +
             "editor_tracing_messages=0"
         aspects.foldLeft(options1) { case (opts, aspect) => aspect.options.foldLeft(opts)(_ + _) }
       }