[ fix ] Handle different format of output from Agda-2.8.0

Author: banacorn

lib/js/src/Agda.bs.js

@@ -118,7 +118,7 @@ module Output = {
         })
       , ...))
   let parse = raw => {
-    let locRe = %re("/\[ at (\S+\:(?:\d+\,\d+\-\d+\,\d+|\d+\,\d+\-\d+|\d+\,\d+)) \]$/")
+    let locRe = %re("/\[ at (\S+\:(?:\d+[,\.]\d+\-\d+[,\.]\d+|\d+[,\.]\d+\-\d+|\d+[,\.]\d+)) \]$/")
     let hasLocation = RegExp.test(locRe, raw)
     if hasLocation {
       parseOutputWithLocation(raw)

lib/js/src/View/Common.bs.js

@@ -88,14 +88,14 @@ module AgdaRange = {
     | Range(option<string>, array<AgdaInterval.t>)
 
   let parse = %re(
-    // Regex updated to v10.1.4
-    // There are 3 types of range:
-    //  type 1: filepath:line,col-line,col
-    //  type 2: filepath:line,col-col
-    //  type 3: filepath:line,col
+    // Regex updated for Agda 2.8.0 compatibility
+    // There are 3 types of range, each supporting both comma and dot separators:
+    //  type 1: filepath:line,col-line,col OR filepath:line.col-line.col
+    //  type 2: filepath:line,col-col OR filepath:line.col-col
+    //  type 3: filepath:line,col OR filepath:line.col
 
-    /* filepath  | line,col-line,col       |    line,col-col   |   line,col | */
-    "/^(\S+)\:(?:(\d+)\,(\d+)\-(\d+)\,(\d+)|(\d+)\,(\d+)\-(\d+)|(\d+)\,(\d+))$/"
+    /* filepath  | line[,.]col-line[,.]col       |    line[,.]col-col   |   line[,.]col | */
+    "/^(\S+)\:(?:(\d+)[,\.](\d+)\-(\d+)[,\.](\d+)|(\d+)[,\.](\d+)\-(\d+)|(\d+)[,\.](\d+))$/"
   )->(Emacs__Parser.captures(captured => {
       open Option
       let flatten = xs => xs->flatMap(x => x)

lib/js/src/View/Component/RichText.bs.js

@@ -172,11 +172,11 @@ module Module = {
     //  tokens captured by the regex will be placed at odd indices
     //  and the rest will be placed at even indices
     // 3 kinds of tokens are captured as AgdaRange:
-    //  1. filepath:line,column-line,column
-    //  2. filepath:line,column-column
-    //  3. filepath:line,column
+    //  1. filepath:line,column-line,column OR filepath:line.column-line.column
+    //  2. filepath:line,column-column OR filepath:line.column-column
+    //  3. filepath:line,column OR filepath:line.column
     raw
-    ->String.splitByRegExp(%re("/([^\(\)\s]+\:(?:\d+\,\d+\-\d+\,\d+|\d+\,\d+\-\d+|\d+\,\d+))/"))
+    ->String.splitByRegExp(%re("/([^\(\)\s]+\:(?:\d+[,\.]\d+\-\d+[,\.]\d+|\d+[,\.]\d+\-\d+|\d+[,\.]\d+))/"))
     ->Array.filterMap(x => x)
     ->Array.mapWithIndex((token, i) =>
       switch mod(i, 2) {

lib/js/test/tests/Test__ShowGoals.bs.js

@@ -20,11 +20,14 @@ let run = normalization => {
 
     switch ctx.state.agdaVersion {
     | Some(version) =>
-      let expectedAllGoalsWarningsBody = if Util.Version.gte(version, "2.7.0") {
-        // Agda 2.7.0+ uses singular "Error" and no trailing newline
+      let expectedAllGoalsWarningsBody = if Util.Version.gte(version, "2.8.0") {
+        // Agda 2.8.0+ uses dot format for positions and includes error codes
+        `?0 : ℕ\n?1 : ℕ\n?2 : ℕ\n?3 : _11\nSort _10  [ at ${filepath}:11.19-31 ]\n_11 : _10  [ at ${filepath}:11.19-31 ]\n_14 : ℕ  [ at ${filepath}:11.19-31 ]\n\n———— Error —————————————————————————————————————————————————\nerror: [UnsolvedConstraints]\nUnsolved constraints`
+      } else if Util.Version.gte(version, "2.7.0") {
+        // Agda 2.7.0+ uses comma format and singular "Error" and no trailing newline
         `?0 : ℕ\n?1 : ℕ\n?2 : ℕ\n?3 : _11\nSort _10  [ at ${filepath}:11,19-31 ]\n_11 : _10  [ at ${filepath}:11,19-31 ]\n_14 : ℕ  [ at ${filepath}:11,19-31 ]\n\n———— Error —————————————————————————————————————————————————\nUnsolved constraints`
       } else {
-        // Agda < 2.7.0 uses plural "Errors" and has trailing newline
+        // Agda < 2.7.0 uses comma format and plural "Errors" and has trailing newline
         `?0 : ℕ\n?1 : ℕ\n?2 : ℕ\n?3 : _11\nSort _10  [ at ${filepath}:11,19-31 ]\n_11 : _10  [ at ${filepath}:11,19-31 ]\n_14 : ℕ  [ at ${filepath}:11,19-31 ]\n\n———— Errors ————————————————————————————————————————————————\nUnsolved constraints\n`
       }
 

lib/js/test/tests/Test__WhyInScope.bs.js

@@ -23,17 +23,30 @@ describe("agda-mode.why-in-scope", () => {
 
     let filteredResponses = responses->Array.filter(filteredResponse)
     let dependencyFilepath = Path.asset("Lib.agda")
-    Assert.deepStrictEqual(
-      filteredResponses,
-      [
-        DisplayInfo(
-          WhyInScope(
-            "Lib.true is in scope as\n  * a constructor Lib.Bool.true brought into scope by\n    - its definition at " ++
-            dependencyFilepath ++ ":4,3-7",
+    
+    switch ctx.state.agdaVersion {
+    | Some(version) =>
+      let positionFormat = if Util.Version.gte(version, "2.8.0") {
+        // Agda 2.8.0+ uses dot format for WhyInScope
+        ":4.3-7"
+      } else {
+        // Pre-2.8.0 uses comma format
+        ":4,3-7"
+      }
+      
+      Assert.deepStrictEqual(
+        filteredResponses,
+        [
+          DisplayInfo(
+            WhyInScope(
+              "Lib.true is in scope as\n  * a constructor Lib.Bool.true brought into scope by\n    - its definition at " ++
+              dependencyFilepath ++ positionFormat,
+            ),
           ),
-        ),
-      ],
-    )
+        ],
+      )
+    | None => Assert.fail("No Agda version found")
+    }
   })
 
   Async.it("should be responded with correct responses (global)", async () => {
@@ -45,16 +58,29 @@ describe("agda-mode.why-in-scope", () => {
 
     let filteredResponses = responses->Array.filter(filteredResponse)
     let dependencyFilepath = Path.asset("Lib.agda")
-    Assert.deepStrictEqual(
-      filteredResponses,
-      [
-        DisplayInfo(
-          WhyInScope(
-            "Lib.true is in scope as\n  * a constructor Lib.Bool.true brought into scope by\n    - its definition at " ++
-            dependencyFilepath ++ ":4,3-7",
+    
+    switch ctx.state.agdaVersion {
+    | Some(version) =>
+      let positionFormat = if Util.Version.gte(version, "2.8.0") {
+        // Agda 2.8.0+ uses dot format for WhyInScope
+        ":4.3-7"
+      } else {
+        // Pre-2.8.0 uses comma format
+        ":4,3-7"
+      }
+      
+      Assert.deepStrictEqual(
+        filteredResponses,
+        [
+          DisplayInfo(
+            WhyInScope(
+              "Lib.true is in scope as\n  * a constructor Lib.Bool.true brought into scope by\n    - its definition at " ++
+              dependencyFilepath ++ positionFormat,
+            ),
           ),
-        ),
-      ],
-    )
+        ],
+      )
+    | None => Assert.fail("No Agda version found")
+    }
   })
 })