From ca60a816c61d58f73e520397781cbe427294440f Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 22 Jun 2021 13:15:01 -0700
Subject: [PATCH] Add the correct file offset to metaprogram parse errors

---
 .../src/Wingman/LanguageServer/Metaprogram.hs |  5 +++--
 .../src/Wingman/Metaprogramming/Parser.hs     | 21 ++++++++++++++++---
 2 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
index 6b924a8060..915724f1aa 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
@@ -22,7 +22,7 @@ import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
-import           GhcPlugins (containsSpan, realSrcLocSpan)
+import           GhcPlugins (containsSpan, realSrcLocSpan, realSrcSpanStart)
 import           Ide.Types
 import           Language.LSP.Types
 import           Prelude hiding (span)
@@ -50,8 +50,9 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr
           case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of
             Just (trss, program) -> do
               let tr_range = fmap realSrcSpanToRange trss
+                  rsl = realSrcSpanStart $ unTrack trss
               HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
-              z <- liftIO $ attempt_it ctx jdg $ T.unpack program
+              z <- liftIO $ attempt_it rsl ctx jdg $ T.unpack program
               pure $ Hover
                 { _contents = HoverContents
                             $ MarkupContent MkMarkdown
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index b03ea3f0e0..8ebf7a9d15 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -21,6 +21,8 @@ import           Wingman.Metaprogramming.Parser.Documentation
 import           Wingman.Metaprogramming.ProofState (proofState, layout)
 import           Wingman.Tactics
 import           Wingman.Types
+import Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)
+import FastString (unpackFS)
 
 
 nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
@@ -421,17 +423,30 @@ wrapError :: String -> String
 wrapError err = "```\n" <> err <> "\n```\n"
 
 
+fixErrorOffset :: RealSrcLoc -> P.ParseErrorBundle a b -> P.ParseErrorBundle a b
+fixErrorOffset rsl (P.ParseErrorBundle ne (P.PosState a n (P.SourcePos _ line col) pos s))
+  = P.ParseErrorBundle ne
+  $ P.PosState a n
+      (P.SourcePos
+        (unpackFS $ srcLocFile rsl)
+        ((<>) line $ P.mkPos $ srcLocLine rsl - 1)
+        ((<>) col  $ P.mkPos $ srcLocCol  rsl - 1 + length @[] "[wingman|")
+      )
+      pos
+      s
+
 ------------------------------------------------------------------------------
 -- | Attempt to run a metaprogram tactic, returning the proof state, or the
 -- errors.
 attempt_it
-    :: Context
+    :: RealSrcLoc
+    -> Context
     -> Judgement
     -> String
     -> IO (Either String String)
-attempt_it ctx jdg program =
+attempt_it rsl ctx jdg program =
   case P.runParser tacticProgram "<splice>" (T.pack program) of
-    Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty peb
+    Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb
     Right tt -> do
       res <- runTactic
             ctx