Mini hack to get right JSon fields

Author: Paul-Lez

LeanUtils/Utils.lean

@@ -42,16 +42,26 @@ def visitSorryNode {Out} (ctx : ContextInfo) (node : Info)
     else return none
   | _ => return none
 
+/-- This is a hack to get the right constructor names (to match those we get
+from using a REPL based sorry extraction). -/
+structure Location where
+  start_line : Nat
+  start_column : Nat
+deriving FromJson, ToJson, DecidableEq
+
+def Lean.Position.toLocation : Position → Location := fun pos ↦ ⟨pos.line, pos.column⟩
+
 structure ParsedSorry where
-  statement : String
-  pos : Position
+  goal : String
+  location : Location
   parentDecl : Name
   hash : UInt64
 deriving FromJson, ToJson, DecidableEq
 
-def SorryData.toParsedSorry {Out} [ToString Out] (fileMap : FileMap) : SorryData Out → ParsedSorry :=
+def SorryData.toParsedSorry {Out} [ToString Out] (fileMap : FileMap) :
+    SorryData Out → ParsedSorry :=
   fun ⟨out, stx, parentDecl⟩ =>
-    ⟨ToString.toString out, fileMap.toPosition stx.getPos?.get!, parentDecl, Hashable.hash <| ToString.toString out⟩
+    ⟨ToString.toString out, fileMap.toPosition stx.getPos?.get! |>.toLocation, parentDecl, Hashable.hash <| ToString.toString out⟩
 
 instance : ToString ParsedSorry where
   toString a := ToString.toString <| ToJson.toJson a