Adding processing ranges WIP

client/src/client.ts

@@ -12,7 +12,8 @@ import {decorationsManual, decorationsContinuous} from './Decorations';
 export default class Client extends LanguageClient {
 
 	private static _channel: any = vscode.window.createOutputChannel('VsCoq');
-    private _decorations: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
+    private _decorationsProcessed: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
+    private _decorationsProcessing: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
 
 	constructor(
         serverOptions: ServerOptions,
@@ -33,17 +34,21 @@ export default class Client extends LanguageClient {
     }
 
     public saveHighlights(uri: String, processingRange: vscode.Range[], processedRange: vscode.Range[]) {
-        this._decorations.set(uri, processedRange);
+        this._decorationsProcessed.set(uri, processedRange);
+        this._decorationsProcessing.set(uri, processingRange);
     }
 
     public updateHightlights() {
-        for(let entry of this._decorations.entries()) {
+        for(let entry of this._decorationsProcessing.entries()) {
+            this.updateDocumentEditors(entry[0], entry[1], "processing");
+        }
+        for(let entry of this._decorationsProcessed.entries()) {
             this.updateDocumentEditors(entry[0], entry[1]);
         }
     };
 
     public resetHighlights() {
-        for(let entry of this._decorations.entries()) {
+        for(let entry of this._decorationsProcessed.entries()) {
             this.resetDocumentEditors(entry[0]);
         }
     }
@@ -59,17 +64,19 @@ export default class Client extends LanguageClient {
         editors.map(editor => {
             editor.setDecorations(decorationsManual.processed, []);
             editor.setDecorations(decorationsContinuous.processed, []);
+            editor.setDecorations(decorationsManual.processing, []);
+            editor.setDecorations(decorationsContinuous.processing, []);
         });
     }
 
-    private updateDocumentEditors(uri: String, ranges: vscode.Range[]) {
+    private updateDocumentEditors(uri: String, ranges: vscode.Range[], type: String = "processed") {
         const config = vscode.workspace.getConfiguration('vscoq.proof');
         const editors = this.getDocumentEditors(uri);
         editors.map(editor => {
             if(config.mode === 0) {
-                editor.setDecorations(decorationsManual.processed, ranges);
+                editor.setDecorations(type === "processed" ? decorationsManual.processed : decorationsManual.processing, ranges);
             } else {
-                editor.setDecorations(decorationsContinuous.processed, ranges);
+                editor.setDecorations(type === "processed" ? decorationsContinuous.processed : decorationsContinuous.processing, ranges);
             }
         });
     }

language-server/dm/documentManager.ml

@@ -60,34 +60,6 @@ let inject_em_event x = Sel.Event.map (fun e -> ExecutionManagerEvent e) x
 let inject_em_events events = List.map inject_em_event events
 
 type events = event Sel.Event.t list
-(* 
-let merge_adjacent_ranges (r1,l) r2 =
-  if Position.compare r1.Range.end_ r2.Range.start == 0 then
-    Range.{ start = r1.Range.start; end_ = r2.Range.end_ }, l
-  else
-    r2, r1 :: l
-
-let compress_sorted_ranges = function
-  | [] -> []
-  | range :: tl ->
-    let r, l = List.fold_left merge_adjacent_ranges (range,[]) tl in
-    r :: l
-
-let compress_ranges ranges =
-  let ranges = List.sort (fun { Range.start = s1 } { Range.start = s2 } -> Position.compare s1 s2) ranges in
-  compress_sorted_ranges ranges *)
-
-(* let executed_ranges doc execution_state loc =
-  let ranges_of l =
-    compress_ranges @@ List.map (Document.range_of_id_with_blank_space doc) l
-  in
-  let ids_before_loc = List.map (fun s -> s.Document.id) @@ Document.sentences_before doc loc in
-  let processed_ids = List.filter (fun x -> ExecutionManager.is_executed execution_state x || ExecutionManager.is_remotely_executed execution_state x) ids_before_loc in
-  log @@ Printf.sprintf "highlight: processed: %s" (String.concat " " (List.map Stateid.to_string processed_ids));
-  { 
-    processing = [];
-    processed = ranges_of processed_ids; 
-  } *)
 
 let executed_ranges st =
   match st.observe_id with
@@ -175,8 +147,9 @@ let observe ~background state id : (state * event Sel.Event.t list) =
       (state, [])
     else
       let priority = if background then None else Some PriorityManager.execution in
+      let execution_state = ExecutionManager.update_processing id state.execution_state state.document in
       let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started = Unix.gettimeofday (); background }) in
-      (state, [ event ])
+      ({state with execution_state}, [ event ])
 
 let clear_observe_id st = 
   { st with observe_id = None }

language-server/dm/executionManager.ml

@@ -248,28 +248,44 @@ let interp_qed_delayed ~proof_using ~state_id ~st =
   let st = { st with interp } in
   st, success st, assign
 
-let update_exec_overview id status state document =
-  let rec insert_or_merge_range r = function
-  | [] -> [r]
-  | r1 :: l ->
-    if Position.compare r1.Range.end_ r.Range.start == 0 then
-      Range.{ start = r1.Range.start; end_ = r.Range.end_ } :: l
-    else
-      r1 :: (insert_or_merge_range r l)
-  in
+let rec insert_or_merge_range r = function
+| [] -> [r]
+| r1 :: l ->
+  if Position.compare r1.Range.end_ r.Range.start == 0 then
+    Range.{ start = r1.Range.start; end_ = r.Range.end_ } :: l
+  else
+    r1 :: (insert_or_merge_range r l)
+
+let update_processed id status state document =
   let range = Document.range_of_id_with_blank_space document id in
   match status with
   | Success _ ->
     let {processing; processed} = state.overview in
     let processed = insert_or_merge_range range processed in
+    let included_range = List.find_opt (fun (r: Range.t) -> Range.included ~in_:r range) processing in
+    let processing = begin match included_range with
+    | None -> processing
+    | Some { end_ } ->
+      let processing = (List.filter (fun (r: Range.t) -> not @@ Range.included ~in_:r range) processing) in
+      List.append [Range.create ~start:range.start ~end_:end_] processing 
+    end 
+    in
     let overview = {processing; processed} in
     {state with overview}
   | Error _ -> state
 
+let update_processing id state document =
+  let range = Document.range_of_id_with_blank_space document id in
+  let { processing; processed } = state.overview in
+  let processing = insert_or_merge_range range processing in
+  let overview = {processing; processed} in
+  {state with overview}
+
+
 let update_all ?document id v fl state =
   let state = match v with
   | Done s ->
-    Option.cata (update_exec_overview id s state) state document
+    Option.cata (update_processed id s state) state document
   | _ -> state
   in
   { state with of_sentence = SM.add id (v, fl) state.of_sentence }

language-server/dm/executionManager.mli

@@ -48,6 +48,7 @@ val pr_event : event -> Pp.t
 
 val overview : state -> exec_overview
 val overview_until_range : state -> Range.t -> exec_overview
+val update_processing: sentence_id -> state -> Document.document -> state
 
 val init : Vernacstate.t -> state * event Sel.Event.t
 val destroy : state -> unit