Skip to content

Commit

Permalink
Use showInfoError from EmacsTop rather than duplicating it here
Browse files Browse the repository at this point in the history
  • Loading branch information
andreasabel committed Nov 27, 2023
1 parent a317504 commit da1d928
Showing 1 changed file with 1 addition and 32 deletions.
33 changes: 1 addition & 32 deletions src/Agda/Convert.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import qualified Agda.IR as IR
import Agda.Interaction.Base
import Agda.Interaction.BasicOps as B
import Agda.Interaction.EmacsCommand (Lisp)
import Agda.Interaction.EmacsTop (showInfoError)
import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms)
import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..))
import qualified Agda.Interaction.Highlighting.Range as Highlighting
Expand Down Expand Up @@ -351,38 +352,6 @@ lispifyGoalSpecificDisplayInfo ii kind = localTCState $

--------------------------------------------------------------------------------

-- | Serializing Info_Error
showInfoError :: Info_Error -> TCM String
showInfoError (Info_GenericError err) = do
e <- prettyError err
w <- prettyTCWarnings' =<< getAllWarningsOfTCErr err

let errorMsg =
if null w
then e
else delimiter "Error" ++ "\n" ++ e
let warningMsg =
List.intercalate "\n" $
delimiter "Warning(s)" :
filter (not . null) w
return $
if null w
then errorMsg
else errorMsg ++ "\n\n" ++ warningMsg
showInfoError (Info_CompilationError warnings) = do
s <- prettyTCWarnings warnings
return $
unlines
[ "You need to fix the following errors before you can compile",
"the module:",
"",
s
]
showInfoError (Info_HighlightingParseError ii) =
return $ "Highlighting failed to parse expression in " ++ show ii
showInfoError (Info_HighlightingScopeCheckError ii) =
return $ "Highlighting failed to scope check expression in " ++ show ii

#if !MIN_VERSION_Agda(2,6,3)
explainWhyInScope ::
String ->
Expand Down

0 comments on commit da1d928

Please sign in to comment.