Merge pull request #679 from coq-community/perf-issues

Working on performance issues of large files.

client/src/client.ts

@@ -35,7 +35,7 @@ export default class Client extends LanguageClient {
         Client._channel.appendLine(message);
     }
 
-    public saveHighlights(uri: String, parsedRange: vscode.Range[], processingRange: vscode.Range[], processedRange: vscode.Range[]) {
+    public saveHighlights(uri: String, processingRange: vscode.Range[], processedRange: vscode.Range[]) {
         this._decorations.set(uri, processedRange);
     }
 

client/src/extension.ts

@@ -233,9 +233,8 @@ Path: \`${coqTM.getVsCoqTopPath()}\`
             client.onNotification("vscoq/updateHighlights", (notification) => {
 
                 client.saveHighlights(
-                    notification.uri, 
-                    notification.parsedRange, 
-                    notification.processingRange, 
+                    notification.uri,
+                    notification.processingRange,
                     notification.processedRange
                 );
 

client/src/protocol/types.ts

@@ -54,7 +54,6 @@ export interface ProofViewNotification {
 export interface UpdateHightlightsNotification {
     uri: Uri; 
     parsedRange: Range[];
-    processingRange: Range[];
     processedRange: Range[];
 }
 

language-server/dm/documentManager.ml

@@ -52,10 +52,8 @@ let inject_em_events events = List.map inject_em_event events
 type events = event Sel.Event.t list
 
 type exec_overview = {
-  parsed : Range.t list;
-  checked : Range.t list;
-  checked_by_delegate : Range.t list;
-  legacy_highlight : Range.t list;
+  processing : Range.t list;
+  processed : Range.t list;
 }
 
 let merge_ranges doc (r1,l) r2 =
@@ -81,20 +79,11 @@ let executed_ranges doc execution_state loc =
     compress_ranges (Document.raw_document doc) @@ List.map (Document.range_of_id doc) l
   in
   let ids_before_loc = List.map (fun s -> s.Document.id) @@ Document.sentences_before doc loc in
-  let ids = List.map (fun s -> s.Document.id) @@ Document.sentences doc in
-  let executed_ids = List.filter (ExecutionManager.is_executed execution_state) ids in
-  let remotely_executed_ids = List.filter (ExecutionManager.is_remotely_executed execution_state) ids in
-  let parsed_ids = List.filter (fun x -> not (List.mem x executed_ids || List.mem x remotely_executed_ids)) ids in
-  let legacy_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: legacy: %s" (String.concat " " (List.map Stateid.to_string legacy_ids));
-  log @@ Printf.sprintf "highlight: parsed: %s" (String.concat " " (List.map Stateid.to_string parsed_ids));
-  log @@ Printf.sprintf "highlight: parsed + checked: %s" (String.concat " " (List.map Stateid.to_string executed_ids));
-  log @@ Printf.sprintf "highlight: parsed + checked_by_delegate: %s" (String.concat " " (List.map Stateid.to_string remotely_executed_ids));
+  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));
   { 
-    parsed = ranges_of parsed_ids;
-    checked = ranges_of executed_ids;
-    checked_by_delegate = ranges_of remotely_executed_ids;
-    legacy_highlight = ranges_of legacy_ids; 
+    processing = [];
+    processed = ranges_of processed_ids; 
   }
 
 let executed_ranges st =

language-server/dm/documentManager.mli

@@ -65,10 +65,8 @@ val reset : state -> state * events
 (** resets Coq *)
 
 type exec_overview = {
-  parsed : Range.t list;
-  checked : Range.t list;
-  checked_by_delegate : Range.t list;
-  legacy_highlight : Range.t list;
+  processing : Range.t list;
+  processed : Range.t list;
 }
 
 val executed_ranges : state -> exec_overview

language-server/protocol/extProtocol.ml

@@ -86,7 +86,6 @@ module Notification = struct
 
       type t = {
         uri : DocumentUri.t;
-        parsedRange : Range.t list;
         processingRange : Range.t list;
         processedRange : Range.t list;
       } [@@deriving yojson]

language-server/tests/dm_tests.ml

@@ -101,7 +101,7 @@ let%test_unit "exec.init" =
   let todo = Sel.Todo.(add empty init_events) in
   let todo = Sel.Todo.(add todo events) in
   let st = handle_events todo st in
-  let ranges = (DocumentManager.executed_ranges st).checked in
+  let ranges = (DocumentManager.executed_ranges st).processed in
   let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.character) ranges in
   [%test_eq: int list] positions [ 0 ];
   let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.end_.character) ranges in
@@ -115,7 +115,7 @@ let%test_unit "exec.require_error" =
   let todo = Sel.Todo.(add empty init_events) in
   let todo = Sel.Todo.(add todo events) in
   let st = handle_events todo st in
-  let ranges = (DocumentManager.executed_ranges st).checked in
+  let ranges = (DocumentManager.executed_ranges st).processed in
   let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.character) ranges in
   [%test_eq: int list] positions [ 19 ]
 
@@ -262,7 +262,7 @@ let%test_unit "exec.insert" =
   let st = insert_text st ~loc:0 ~text:"Definition z := 0. " in
   let st = DocumentManager.validate_document st in
   let st, events = DocumentManager.interpret_to_end st in
-  let ranges = (DocumentManager.executed_ranges st).checked in
+  let ranges = (DocumentManager.executed_ranges st).processed in
   let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.char) ranges in
   check_no_diag st;
   [%test_eq: int list] positions [ 0; 22 ]

language-server/vscoqtop/lspManager.ml

@@ -180,13 +180,12 @@ let publish_diagnostics uri doc =
   output_notification (Std diag_notification)
 
 let send_highlights uri doc =
-  let { Dm.DocumentManager.parsed; checked; checked_by_delegate; legacy_highlight } =
+  let { Dm.DocumentManager.processing;  processed } =
     Dm.DocumentManager.executed_ranges doc in
   let notification = Notification.Server.UpdateHighlights {
     uri;
-    parsedRange = parsed;
-    processingRange = checked;
-    processedRange = legacy_highlight;
+    processingRange = processing;
+    processedRange = processed;
   }
   in
   output_json @@ Jsonrpc.Notification.yojson_of_t @@ Notification.Server.to_jsonrpc notification