diff --git a/src/Cornelis/Pretty.hs b/src/Cornelis/Pretty.hs index 9130ceb..b34b3a4 100644 --- a/src/Cornelis/Pretty.hs +++ b/src/Cornelis/Pretty.hs @@ -25,7 +25,7 @@ import Prettyprinter.Internal.Type -- The suffix after @Cornelis/XXX/@ matches the names as returned by Agda, contained in 'C.hl_atoms'. -- How these names are generated is not documented on Agda's side, but the implementation can be found at -- ['Agda.Interaction.Highlighting.Common.toAtoms'](https://github.com/agda/agda/src/full/Agda/Interaction/Highlighting/Common.hs). --- The correspoding Agda types are found in 'Agda.Interaction.Highlighting.Precise'. +-- The corresponding Agda types are found in 'Agda.Interaction.Highlighting.Precise'. -- -- NOTE: -- * When modifying this type, remember to sync the changes to @syntax/agda.vim@ diff --git a/src/Cornelis/Types/Agda.hs b/src/Cornelis/Types/Agda.hs index acb96ec..90afed8 100644 --- a/src/Cornelis/Types/Agda.hs +++ b/src/Cornelis/Types/Agda.hs @@ -310,6 +310,6 @@ intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a intervalsToRange _ [] = NoRange intervalsToRange f is = Range f (Seq.fromList is) -mkAbsPathRnage :: Text -> IntervalWithoutFile -> Range -mkAbsPathRnage = intervalToRange . Just . AbsolutePath . T.unpack +mkAbsPathRange :: Text -> IntervalWithoutFile -> Range +mkAbsPathRange = intervalToRange . Just . AbsolutePath . T.unpack diff --git a/src/Plugin.hs b/src/Plugin.hs index 039d115..d1c036b 100644 --- a/src/Plugin.hs +++ b/src/Plugin.hs @@ -147,7 +147,7 @@ solveOne _ ms = withNormalizationMode ms $ \mode -> Cmd_solveOne mode (ip_id ip) - (mkAbsPathRnage fp $ ip_interval' ip) + (mkAbsPathRange fp $ ip_interval' ip) "" autoOne :: CommandArguments -> Maybe String -> Neovim CornelisEnv () @@ -160,7 +160,7 @@ autoOne _ ms = withNormalizationMode ms $ \mode -> Cmd_autoOne mode (ip_id ip) - (mkAbsPathRnage fp $ ip_interval' ip) + (mkAbsPathRange fp $ ip_interval' ip) (T.unpack t) withNormalizationMode :: Maybe String -> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv () @@ -189,7 +189,7 @@ typeContext _ ms = withNormalizationMode ms $ \mode -> Cmd_goal_type_context mode (ip_id goal) - (mkAbsPathRnage fp $ ip_interval' goal) + (mkAbsPathRange fp $ ip_interval' goal) "" typeContextInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv () @@ -202,7 +202,7 @@ typeContextInfer _ ms = withNormalizationMode ms $ \mode -> $ Cmd_goal_type_context_infer mode (ip_id ip) - (mkAbsPathRnage fp $ ip_interval' ip) + (mkAbsPathRange fp $ ip_interval' ip) $ T.unpack contents doRefine :: CommandArguments -> Neovim CornelisEnv () @@ -251,7 +251,7 @@ elaborate mode = withAgda $ void $ withGoalAtCursor $ \b ip -> do $ Cmd_elaborate_give mode (ip_id ip) - (mkAbsPathRnage fp $ ip_interval' ip) + (mkAbsPathRange fp $ ip_interval' ip) $ T.unpack t doTypeInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv () @@ -292,7 +292,7 @@ doNormalize _ ms = withComputeMode ms $ \mode -> $ Cmd_compute mode (ip_id ip) - (mkAbsPathRnage fp $ ip_interval' ip) + (mkAbsPathRange fp $ ip_interval' ip) $ T.unpack t helperFunc :: Rewrite -> Text -> Neovim CornelisEnv () @@ -304,7 +304,7 @@ helperFunc mode expr = do $ Cmd_helper_function mode (ip_id ip) - (mkAbsPathRnage fp $ ip_interval' ip) + (mkAbsPathRange fp $ ip_interval' ip) $ T.unpack expr doHelperFunc :: CommandArguments -> Maybe String -> Neovim CornelisEnv () @@ -327,7 +327,7 @@ caseSplit thing = withAgda $ void $ withGoalAtCursor $ \b ip -> do flip runIOTCM agda $ Cmd_make_case (ip_id ip) - (mkAbsPathRnage fp $ ip_interval' ip) + (mkAbsPathRange fp $ ip_interval' ip) $ T.unpack thing getVersion :: Neovim CornelisEnv () diff --git a/syntax/agda.vim b/syntax/agda.vim index f51c7e4..a70019d 100644 --- a/syntax/agda.vim +++ b/syntax/agda.vim @@ -11,7 +11,7 @@ let s:cpo_save = &cpo set cpo&vim " The following sets up syntax highlighting by linking -" pluging highlight groups to default highlight groups. +" plugin highlight groups to default highlight groups. " Highlight of a hole. hi def link CornelisHole Todo