--- a/src/Pure/PIDE/document.ML Tue Sep 26 12:46:31 2023 +0200
+++ b/src/Pure/PIDE/document.ML Tue Sep 26 13:34:04 2023 +0200
@@ -783,10 +783,10 @@
Command.print0 {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 result = 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};
+ in Exn.release result end};
val result_entry =
(case lookup_entry node id of
NONE => err_undef "result command entry" id
--- a/src/Pure/Thy/thy_info.ML Tue Sep 26 12:46:31 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Sep 26 13:34:04 2023 +0200
@@ -216,9 +216,9 @@
| consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
let
val _ = Execution.join [exec_id];
- val res = Exn.capture Thm.consolidate_theory theory;
+ val result = Exn.capture Thm.consolidate_theory theory;
val exns = maps Task_Queue.group_status (Execution.peek exec_id);
- in res :: map Exn.Exn exns end;
+ in result :: map Exn.Exn exns end;
fun present_theory (Exn.Exn exn) = [Exn.Exn exn]
| present_theory (Exn.Res (Result {theory, present, ...})) =