Fix error location calculation

Co-Authored-By: Laurent Théry <[email protected]>

Author: 2 people

server/src/stm/STM.ts

@@ -16,6 +16,7 @@ import * as server from '../server';
 import {AnnotatedText} from '../util/AnnotatedText'
 import * as text from '../util/AnnotatedText'
 import {GoalsCache} from './GoalsCache';
+import * as semver from 'semver';
 
 import {Settings} from '../protocol';
 export {StateStatus} from './State';
@@ -802,11 +803,19 @@ private routeId = 1;
    */
   private async handleCallFailure(error: coqtop.CallFailure, command: {range: Range, text: string}) : Promise<proto.FailValue> {
     let errorRange : Range = undefined;
-    if(error.range)
-      errorRange = vscode.Range.create(
-        textUtil.positionAtRelativeCNL(command.range.start, command.text, error.range.start)
-      , textUtil.positionAtRelativeCNL(command.range.start, command.text, error.range.stop)
-      );
+    if(error.range) {
+      const version = this.coqtop.getVersion();
+      let start : Position;
+      let end : Position;
+      if (semver.satisfies(version, ">= 8.15")) {
+        start = textUtil.positionAtRelative(command.range.start, command.text, error.range.start)
+        end = textUtil.positionAtRelative(command.range.start, command.text, error.range.stop)
+      } else {
+        start = textUtil.positionAtRelativeCNL(command.range.start, command.text, error.range.start)
+        end = textUtil.positionAtRelativeCNL(command.range.start, command.text, error.range.stop)
+      }
+      errorRange = vscode.Range.create(start, end);
+    }
 
     const diffError = errorParsing.parseError(error.message);
     const prettyError = server.project.getPrettifySymbols().prettify(diffError)

server/src/util/text-util.ts

@@ -3,6 +3,7 @@ import {Position, Range} from 'vscode-languageserver';
 
 // 'sticky' flag is not yet supported :()
 const lineEndingRE = /([^\r\n]*)(\r\n|\r|\n)?/;
+const lineEndingRE1 = /([^\r\n]*)((\r\n)*|\r|\n)?/;
 
 export interface RangeDelta {
   start: Position;
@@ -223,16 +224,17 @@ export function positionAtRelativeCNL(start: Position, text: string, offset: num
   let currentOffset = 0;  // offset into text we are current at; <= `offset`
   let lineOffset = start.character;
   while(true) {
-    const match = lineEndingRE.exec(text.substring(currentOffset));
+    const match = lineEndingRE1.exec(text.substring(currentOffset));
     // match[0] -- characters plus newline
     // match[1] -- characters up to newline
     // match[2] -- newline (\n, \r, or \r\n)
+    const value = match[0].length - match[1].length;
     if(!match || match[0].length === 0 || match[1].length >= offset)
       return Position.create(line, lineOffset + offset)
     currentOffset+= match[0].length;
-    offset -= match[1].length + (match[2]===undefined ? 0 : 1);
+    offset -= match[1].length + (Math.floor(value / 2)  + 1);
     lineOffset = 0;
-    ++line;
+    line += Math.floor((value + 1) / 2);
   }
 }