From fd77091a3587cb8f5fd77ab5f86c11baf8a715c4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 31 May 2024 11:32:33 +0200
Subject: [PATCH] set Qed as immediately processed, set proof body as
 processing

---
 language-server/dm/executionManager.ml | 66 ++++++++++++++------------
 1 file changed, 36 insertions(+), 30 deletions(-)

diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 825a361b7..ef0d84905 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -251,50 +251,54 @@ let rec remove_or_truncate_range r = function
   else
     r1 :: (remove_or_truncate_range r l)
 
+let update_processed_as_Done s range overview =
+  let {prepared; processing; processed} = overview in
+  match s with
+  | Success _ ->
+    log @@ "INSERTING TO PROCESSED";
+    let processed = insert_or_merge_range range processed in
+    log @@ "TRUNCATING FROM PROCESSING";
+    let processing = remove_or_truncate_range range processing in
+    log @@ "TRUNCATING FROM PREPARED";
+    let prepared = remove_or_truncate_range range prepared in
+    {prepared; processing; processed}
+  | Error _ ->
+    log @@ "TRUNCATING FROM PROCESSING";
+    let processing = remove_or_truncate_range range processing in
+    log @@ "TRUNCATING FROM PREPARED";
+    let prepared = remove_or_truncate_range range prepared in
+    {prepared; processing; processed}
+
 let update_processed id state document overview =
   log @@ "UPDATING PROCESSED";
-  let {prepared; processing; processed} = overview in
   let range = Document.range_of_id_with_blank_space document id in
   match SM.find id state.of_sentence with
   | (s, _) ->
     begin match s with
-    | Done s ->
-      begin match s with
-      | Success _ ->
-        log @@ "INSERTING TO PROCESSED";
-        let processed = insert_or_merge_range range processed in
-        log @@ "TRUNCATING FROM PROCESSING";
-        let processing = remove_or_truncate_range range processing in
-        log @@ "TRUNCATING FROM PREPARED";
-        let prepared = remove_or_truncate_range range prepared in
-        {prepared; processing; processed}
-      | Error _ ->
-        log @@ "TRUNCATING FROM PROCESSING";
-        let processing = remove_or_truncate_range range processing in
-        log @@ "TRUNCATING FROM PREPARED";
-        let prepared = remove_or_truncate_range range prepared in
-        {prepared; processing; processed}
-      end
-    | _ -> log @@ "TRYING TO UPDATE DELEGATED ID: " ^ Stateid.to_string id; {prepared; processing; processed}
+    | Done s -> update_processed_as_Done s range overview
+    | _ -> assert false (* delegated sentences born as such, cannot become it later *)
     end
   | exception Not_found ->
     log @@ "Trying to get overview with non-existing state id " ^ Stateid.to_string id;
-    {prepared; processing; processed}
+    overview
 
 let update_processing task processing prepared document =
   log @@ "UPDATING PROCESSING";
   match task with
   | PDelegate { opener_id; terminator_id; tasks } ->
-    let opener_id = begin match tasks with
-    | [] -> opener_id
-    | t :: _ -> match t with
-      | PDelegate { opener_id } -> opener_id
-      | PSkip { id } | PExec { id } | PQuery { id } -> id
-    end
+    let proof_opener_id = match tasks with
+      | [] -> opener_id
+      | (PSkip { id } | PExec { id } | PQuery { id }) :: _ -> id
+      | PDelegate _ :: _ -> assert false
+    in
+    let proof_closer_id = match List.rev tasks with
+      | [] -> terminator_id
+      | (PSkip { id } | PExec { id } | PQuery { id }) :: _ -> id
+      | PDelegate _ :: _ -> assert false
     in
-    let opener_range = Document.range_of_id_with_blank_space document opener_id in
-    let terminator_range = Document.range_of_id_with_blank_space document terminator_id in
-    let range = Range.create ~end_:terminator_range.end_ ~start:opener_range.start in
+    let proof_begin_range = Document.range_of_id_with_blank_space document proof_opener_id in
+    let proof_end_range = Document.range_of_id_with_blank_space document proof_closer_id in
+    let range = Range.create ~end_:proof_end_range.end_ ~start:proof_begin_range.start in
     log @@ "DELEGATED JOB RANGE: " ^ Range.to_string range;
     log @@ "TRUNCATING FROM PREPARED";
     (* When a job is delegated we shouldn't merge ranges (to get the proper progress report) *)
@@ -307,7 +311,9 @@ let update_processing task processing prepared document =
 let update_overview task todo state document overview =
   let {processed; processing; prepared} = 
   match task with 
-  | PDelegate _ -> overview
+  | PDelegate { terminator_id } ->
+    let range = Document.range_of_id_with_blank_space document terminator_id in
+    update_processed_as_Done (Success None) range overview
   | PSkip { id } | PExec { id } | PQuery { id } ->
     update_processed id state document overview
   in