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;
--- 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"
--- 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;
--- 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)(_ + _) }
}