Skip to content

doc: run spellchecker on project #183

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
4e554c4c merged 2 commits into from
Oct 31, 2025
Merged

doc: run spellchecker on project #183

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5a468e2
doc: run spellchecker on project
foxyseta Oct 31, 2025
076facd
doc: run spellchecker on project
foxyseta Oct 31, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/Cornelis/Pretty.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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@
Expand Down
4 changes: 2 additions & 2 deletions src/Cornelis/Types/Agda.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

16 changes: 8 additions & 8 deletions src/Plugin.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand All @@ -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 ()
Expand Down Expand Up @@ -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 ()
Expand All @@ -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 ()
Expand Down Expand Up @@ -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 ()
Expand Down Expand Up @@ -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 ()
Expand All @@ -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 ()
Expand All @@ -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 ()
Expand Down
2 changes: 1 addition & 1 deletion syntax/agda.vim
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading