tuned;
authorwenzelm
Tue, 26 Sep 2023 13:34:04 +0200
changeset 78717 1eca7abaa015
parent 78716 97dfba4405e3
child 78718 f34a451f7b5b
tuned;
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
--- 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, ...})) =