-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(Handler2.AutoCompletion): add digHole
- Loading branch information
Vince
committed
Feb 27, 2024
1 parent
5a3cfd7
commit 7102674
Showing
3 changed files
with
248 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,233 @@ | ||
{-# LANGUAGE OverloadedStrings #-} | ||
|
||
{-# LANGUAGE TypeOperators #-} | ||
module Server.Handler2.AutoCompletion where | ||
|
||
import Data.Text ( Text ) | ||
import Language.LSP.Types | ||
import Server.Monad | ||
|
||
-- To control the behaviour of autocomplete | ||
-- see https://github.com/haskell/lsp/blob/bf95cd94f3301fe391093912e6156de7cb5c1289/lsp-types/src/Language/LSP/Types/Completion.hs | ||
handler :: Position -> Maybe CompletionContext -> ServerM CompletionList | ||
handler position completionContext | ||
| shouldTriggerUnicodeCompletion completionContext | ||
= return $ CompletionList True (List (unicodeCompletionItems position)) | ||
| shouldTriggerDighole completionContext | ||
= return $ CompletionList False (List [specBracketsCompletionItem]) | ||
| otherwise | ||
= return $ CompletionList True (List []) | ||
|
||
-- https://github.com/haskell/lsp/blob/bf95cd94f3301fe391093912e6156de7cb5c1289/lsp-types/src/Language/LSP/Types/Completion.hs#L360-L371 | ||
-- trigger Unicode symbol completion when: | ||
-- 1. a backslash "\" is being typed | ||
-- 2. current completion is incomplete | ||
shouldTriggerUnicodeCompletion :: Maybe CompletionContext -> Bool | ||
shouldTriggerUnicodeCompletion (Just (CompletionContext CtTriggerCharacter (Just "\\"))) | ||
= True | ||
shouldTriggerUnicodeCompletion (Just (CompletionContext CtTriggerForIncompleteCompletions _)) | ||
= True | ||
shouldTriggerUnicodeCompletion _ | ||
= False | ||
|
||
-- turn '?' into spec brackets '[! !]' | ||
shouldTriggerDighole :: Maybe CompletionContext -> Bool | ||
shouldTriggerDighole (Just (CompletionContext CtTriggerCharacter (Just "?"))) | ||
= True | ||
shouldTriggerDighole _ | ||
= False | ||
|
||
-- list of `CompletionItem`s for unicode symbols | ||
unicodeCompletionItems :: Position -> [CompletionItem] | ||
unicodeCompletionItems position = mconcat | ||
[ makeItems position | ||
[" "] | ||
(Just CiOperator) | ||
"\\" | ||
"\"\\\" Backward slash" | ||
"Inserting \"\\\"" | ||
, makeItems position | ||
["->", "rightarrow", "r", "to"] | ||
(Just CiOperator) | ||
"→" | ||
"\"→\" Rightwards Arrow" | ||
"The Unicode variant of \"->\"" | ||
, makeItems position | ||
["/=", "neq", "!="] | ||
(Just CiOperator) | ||
"≠" | ||
"\"≠\" Not Equal To" | ||
"The Unicode variant of \"/=\"" | ||
, makeItems position | ||
[">=", "ge", "gte"] | ||
(Just CiOperator) | ||
"≥" | ||
"\"≥\" Greater-Than or Equal To" | ||
"The Unicode variant of \">=\"" | ||
, makeItems position | ||
["<=", "le", "lte"] | ||
(Just CiOperator) | ||
"≤" | ||
"\"≤\" Less-Than or Equal To" | ||
"The Unicode variant of \"<=\"" | ||
, makeItems position | ||
["==>", "Rightarrow", "implies", "R"] | ||
(Just CiOperator) | ||
"⇒" | ||
"\"⇒\" Rightwards Double Arrow" | ||
"The Unicode variant of \"=>\"" | ||
, makeItems position | ||
["<==", "Leftarrow", "ffrom", "L"] | ||
(Just CiOperator) | ||
"⇐" | ||
"\"⇐\" Leftwards Double Arrow" | ||
"The Unicode variant of \"<=\"" | ||
, makeItems position | ||
["&&", "wedge", "and"] | ||
(Just CiOperator) | ||
"∧" | ||
"\"∧\" Logical And" | ||
"The Unicode variant of \"&&\"" | ||
, makeItems position | ||
["||", "vee", "or"] | ||
(Just CiOperator) | ||
"∨" | ||
"\"∨\" Logical Or" | ||
"The Unicode variant of \"||\"" | ||
, makeItems position | ||
["~", "neg", "-"] | ||
(Just CiOperator) | ||
"¬" | ||
"\"¬\" Not Sign" | ||
"The Unicode variant of \"~\"" | ||
, makeItems position | ||
["<|", "langle", "<"] | ||
(Just CiValue) | ||
"⟨" | ||
"\"⟨\" Left Angle Bracket" | ||
"The Unicode variant of \"<|\"" | ||
, makeItems position | ||
["|>", "rangle", ">"] | ||
(Just CiValue) | ||
"⟩" | ||
"\"⟩\" Right Angle Bracket" | ||
"The Unicode variant of \"|>\"" | ||
, makeItems position | ||
["min", "downarrow", "d"] | ||
(Just CiValue) | ||
"↓" | ||
"\"↓\" Downwards Arrow" | ||
"The Unicode variant of \"min\"" | ||
, makeItems position | ||
["max", "uparrow", "u"] | ||
(Just CiValue) | ||
"↑" | ||
"\"↑\" Upwards Arrow" | ||
"The Unicode variant of \"max\"" | ||
, makeItems position | ||
["sum", "Sigma", "sigma", "Gs"] | ||
(Just CiValue) | ||
"Σ" | ||
"\"Σ\" Sum" | ||
"The Unicode variant of \"sum\"" | ||
, makeItems position | ||
["product", "Pi", "pi", "Gp"] | ||
(Just CiValue) | ||
"∏" | ||
"\"∏\" Product" | ||
"The Unicode variant of \"product\"" | ||
, makeItems position | ||
["forall", "all", "A"] | ||
(Just CiValue) | ||
"∀" | ||
"\"∀\" Forall" | ||
"The Unicode variant of \"forall\"" | ||
, makeItems position | ||
["exists", "ex", "E"] | ||
(Just CiValue) | ||
"∃" | ||
"\"∃\" Exists" | ||
"The Unicode variant of \"exists\"" | ||
, makeItems position | ||
["<=>", "equiv", "iff", "==="] | ||
(Just CiOperator) | ||
"≡" | ||
"\"≡\" If and only if" | ||
"The Unicode variant of \"<=>\"" | ||
, makeItems position | ||
["sconj"] | ||
(Just CiOperator) | ||
"٭" | ||
"\"٭\" SConj" | ||
"SConj" | ||
] | ||
|
||
-- See https://github.com/haskell/lsp/blob/bf95cd94f3301fe391093912e6156de7cb5c1289/lsp-types/src/Language/LSP/Types/Completion.hs#L288 | ||
makeItems | ||
:: Position | ||
-> [Text] | ||
-> Maybe CompletionItemKind | ||
-> Text | ||
-> Text | ||
-> Text | ||
-> [CompletionItem] | ||
makeItems position labels kind symbol detail doc = flip map labels $ \label -> | ||
CompletionItem | ||
label -- The label of this completion item. | ||
-- By default also the text that is inserted when selecting this completion. | ||
kind -- could be CIOperator, CiValue or whatever | ||
Nothing -- for marking deprecated stuff | ||
(Just detail) -- human-readable string | ||
(Just $ CompletionDocString doc) -- also human-readable string | ||
Nothing -- deprecated | ||
Nothing -- select thie item when showing | ||
Nothing -- how to sort completion items | ||
Nothing -- how to filter completion items | ||
(Just symbol) -- the symbol we wanna insert | ||
(Just PlainText) -- could be a "Snippet" (with holes) or just plain text | ||
Nothing -- how whitespace and indentation is handled during completion | ||
Nothing -- TextEdit to be applied when this item has been selected (but not completed yet) | ||
removeSlash -- TextEdit to be applied when this item has been completed | ||
(Just (List [" ", "\\"])) -- commit characters | ||
Nothing -- command to be executed after completion | ||
Nothing -- ??? | ||
where | ||
Position ln col = position | ||
removeSlash = | ||
Just $ List [TextEdit (Range (Position ln (col - 1)) position) ""] | ||
-- tempReplaceWithSymbol = Just $ CompletionEditText $ TextEdit (Range position (Position ln (col + 1 ))) "symbol" | ||
|
||
specBracketsCompletionItem :: CompletionItem | ||
specBracketsCompletionItem = | ||
CompletionItem | ||
{ _label = "?" | ||
, _kind = Just CiSnippet | ||
, _tags = Nothing -- ^ Tags for this completion item. | ||
, _detail = Nothing -- ^ A human-readable string with additional | ||
-- information about this item, like type or | ||
-- symbol information. | ||
, _documentation = Just (CompletionDocString "Type \"?\" and a space to insert a spec.") | ||
, _deprecated = Nothing | ||
, _preselect = Just True | ||
-- ^ Select this item when showing. | ||
-- *Note* that only one completion item can be selected and that the | ||
-- tool / client decides which item that is. The rule is that the *first* | ||
-- item of those that match best is selected. | ||
, _sortText = Nothing | ||
, _filterText = Nothing | ||
, _insertText = Just "[! !]" | ||
, _insertTextFormat = Just PlainText | ||
, _insertTextMode = Nothing | ||
-- ^ How whitespace and indentation is handled during completion | ||
-- item insertion. If not provided the client's default value depends on | ||
-- the @textDocument.completion.insertTextMode@ client capability. | ||
, _textEdit = removeQuestionMark | ||
, _additionalTextEdits = Nothing | ||
, _commitCharacters = Just (List [" "]) | ||
, _command = Nothing | ||
, _xdata = Nothing | ||
} deriving (Read,Show,Eq) | ||
where | ||
Position line column = position | ||
removeQuestionMark = | ||
Just $ List [TextEdit (Range (Position line (column - 1)) position) ""] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
|
||
import qualified Data.Aeson.Types as JSON | ||
import Server.Monad (ServerM) | ||
|
||
handler :: JSON.Value -> (Response -> ServerM ()) -> ServerM () | ||
handler params responder = do | ||
-- TODO: | ||
return () |