Maybe will embrace a little bit overhead.

pending on upstream issue

microsoft/vscode#547

Note for contribution to Idris internals

sample:

module Main

import Effects
import Effect.State

TC : Type -> Type
TC a = Effects.SimpleEff.Eff a ['bindings ::: STATE (List (Pair String Int)),
                                'counter ::: STATE Int]

incrCounter : TC Int
incrCounter = do
    n <- 'counter :- get
    'counter :- put (n + 1)
    pure n

newMetaTypeVar : TC String
newMetaTypeVar = do
    n <- incrCounter
    pure ("Meta" ++ show n)


main : IO ()
main = do
    s <- runInit ['bindings := [], 'counter := 1] newMetaTypeVar
    print s

https://github.com/zjhmale/vscode-idris/blob/master/src/idris/commands.js#L41

• Linux
• Windows

• An ambitious Haskell implementation https://github.com/zjhmale/idris-lsp
• Using https://github.com/Microsoft/vscode-languageserver-node to make it easier

Initially proposed from #31, hope we will not meet any performance overhead 😅

• Note for contribution to vscode-icons vscode-icons/vscode-icons#830
• Show problems panel directly instead of output channel. Pending on microsoft/vscode#22885
• Highlight Output Channel

Highlight Output Channel is pending on upstream issues:

microsoft/vscode#586
microsoft/vscode#11005

The original approach e3a1d6c to fix this can highlight messages in output channel indeed, but it will override some default behaviors of the output channel, e.g. we can no longer click the links inside output channel, even use registerDocumentLinkProvider

Another hacky approach html_views

Thus for hover-type, if a method is called, e.g. count', rather than count, then the incorrect identifier is passed to idris-server for type identification, and the hovertext shows a "No such variable" message

The editor windows look great with the Hasklig font set up and editor.fontLigatures turned on.

One difference to the Haskell ghc-mod vscode extension is that the hover type messages in the Haskell one respect the ligature setting and show hover ligatures, but the Idris one currently doesn't.

totalscript/totalscript@f702abe

Another feature request copied from https://github.com/hoovercj/vscode-ghc-mod

It has a preference: haskell.ghcMod.onHover, which can be set to fallback mode where it does :info, then falls back to type if :info returns nothing.

My request is to have a fallback mode for vscode-idris, that shows the :doc output on type-hover.

That way the user sees the richest possible information on type hover.

When a hover range is inside a diagnostic, just show diagnostic message without hover message.

This looks like a great extension! When do you think it will be ready for publishing on the marketplace?

Like Idris:

https://code.visualstudio.com/docs/extensionAPI/vscode-api#SignatureHelpProvider

Since Haskell-like syntax does not have parenthesis and commas for functions, things may get tricky here. If use some backtracking to find the nearest function definition, a big overhead of trying to get type information of each identifier in the backtracking path stands there. This feature seems to be impossible to be implemented at present. On a second thought, if we can backtracking to find the nearest function and to match the number of arguments can still finish the job.

And the case to support signature hint for function call inside parenthesis e.g. (fun arg...) is much more straightforward.

- [ ] signature hint for open function calls There is partial evaluation stands there, e.g., map ƒ ... so it will be crazy complicate and hard to give a 100% promise of precise, support for close functions is best we can do here for parameter type hints.

• signature hint for close function calls

First of all, thanks for working on this extension. I'm just experimenting with VS Code and was happy to see some Idris support.

Unfortunately, I haven't been able to get much of anything working. After installing the extension, I opened an existing project of mine and tried to type check it. When I execute the type checking function, however, absolutely no output is shown. I added deliberate type errors and still did not see any output.

Unable to debug this, I created an idris file with the following contents:

module Junk

data Test

When I try to get your extension to type check this code, I get an error popup reading Running the contributed command:'idris.typecheck' failed with no further information. This is more than I get for my larger file, but I'm still not sure what I'm doing wrong.

Any advice would be greatly appreciated. Idris is on my $PATH installed on OSX via homebrew.

decreaseIndentPattern and increaseIndentPattern don't work as expected, any ideas about this @be5invis ?

Since other sophisticated extensions are all released without carrying any default key bindings, so I'm just seriously considering about removing all the default key bindings for actions. Any ideas about this @be5invis

Note for contribution to https://github.com/siegebell/vsc-prettify-symbols-mode.

• Note for contribution to add item kind for :repl-completions command. Also, need to eliminate some speed overhead.

Currently, it will only suggest bare strings for auto-completion without any extra information e.g. item kind which mentioned above.

{"responseType":"return","msg":[[["locMessage"],""]]}
{"responseType":"return","msg":[[["show","showArg","showCon","showLitChar","showLitString","showParens","showPrec"],""]]}
{"responseType":"return","msg":[[["show"],""]]}
{"responseType":"return","msg":[[["show","showArg","showCon","showLitChar","showLitString","showParens","showPrec"],""]]}
{"responseType":"return","msg":[[["Unknown","UnknownImplicit"],""]]}
{"responseType":"return","msg":[[["show","showArg","showCon","showLitChar","showLitString","showParens","showPrec"],""]]}

• Support auto-completion for all words in the open editor like javascript here.

For the second point, there is no external tools to analysis Idris source file currently, so a naive but straight forward way is to extract all the lexer identifier and add to the completion result list.

https://code.visualstudio.com/shortcuts/keyboard-shortcuts-macos.pdf
https://code.visualstudio.com/docs/getstarted/keybindings

In order to make this extension more robust.

https://github.com/Microsoft/vscode-go/blob/master/test/go.test.ts

Discussed at #11

• type of word
• docs for word
• case split
• add clause
• make with
• make lemma
• make case
• show holes
• proof search
• type check file
• print definition
• REPL
• apropos
• completions

Only rename function names which share the same definition location.

https://code.visualstudio.com/docs/extensionAPI/vscode-api#RenameProvider

• https://code.visualstudio.com/docs/editor/integrated-terminal
• https://code.visualstudio.com/docs/extensionAPI/vscode-api#Terminal

• Start REPL and load currently opened Idris file.
• Refresh REPL when changing opened Idris file.
• Send selected code to REPL.

Pending on upstream issues:

microsoft/vscode#586
microsoft/vscode#11005

The original approach e3a1d6c to fix this can highlight messages in output channel indeed, but it will override some default behaviors of the output channel, e.g. we can no longer click the links inside output channel, even use registerDocumentLinkProvider

Another hacky approach html_views

https://code.visualstudio.com/docs/extensionAPI/extension-points#_contributesmenus
https://code.visualstudio.com/docs/getstarted/keybindings#_when-clause-contexts

• Add executable configuration.
• When the executable path is changed, need to re-initialize.
• If the executable path is invalid, do not initialize and show a proper error message.

Highlighting docs, types, definitions etc. use infos from here and here

Possible solutions:

• highlight in output channel directly

pending on upstream issues

microsoft/vscode#5274
microsoft/vscode#571

• create a html view

pending on upstream issue

microsoft/vscode#272

Currently, the type classes and data constructors are not highlighted.

And this is highlighting with the syntax file translated directly from the atom package.

Maybe we can go back to the old highlighting style? @be5invis

I've a couple of times wanted to send a pull request, but:

1. I can't trivially see how to build and test the extension for myself. Add a document explaining this, plus any other requirements that must be met for a potential pull request to be considered
2. (related) I suspect there might be some deployment/configuration files that aren't part of the repo. If so, could they be added?

The point is to lower the barrier to sending potentially useful pull requests

Enhancement request:

To make the plugin even more amazing, it would be great if the appropriate Idris commands were exposed via right-clicking in an identifier rather than only through the control-shift-p menu.

Currently, there is a bunch of redundant new-line character \n in the documentation for an identifier read from ide-mode.

Happened when the current line is already at the last line in the opened editor. So does other commands which will generate code in the editor.

I'm running idris 0.99.1 on OSX

Extension is awesome, but after using it for 45 minutes or so running commands (exercises in TDDII) slows down dramatically and there is an idris process using most of my system's RAM.

Workaround: Closing and opening VS Code every now and again.

Show type on hover is now working (awesome!)

My issue is:

If the idris server's type-checking function fails, the error message shown in place of the hover type should show the Idris-server error message (which in my case was a warning that the .ibc files had been built with an older idris version and needed cleaning) rather than what it currently shows of "didn't load /path/to/file.idr"

• IDE-Mode

• :add-proof-clause d238beb
• :add-missing
• :who-calls
• :calls-who
• :browse-namespace 54c7eab
• :normalise-term
• :show-term-implicits
• :hide-term-implicits
• :elaborate-term

• REPL

• :search 785126b

Whenever I run the typecheck command successfully, the OUTPUT pane shows:

Idris: File loaded successfull

I assume there should be at least a trailing y there, possibly more.

https://github.com/JuliaEditorSupport/julia-vscode/wiki/Snippets#latex, Idris support unicode identifiers.

we can use https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/WhoCalls.hs command here, though it does not give any information about the line, column and file-path, but we can find all occurrences and then match the type signature to filter out all usages.

A sample result of this command:

{"responseType":"return","msg":[[[["TermLang.Unify.reifyExp",[[0,23,[[":name","TermLang.Unify.reifyExp"],[":implicit",false],[":decor",":function"],[":doc-overview",""],[":type","Int -> Val -> TC Exp"],[":namespace","TermLang.Unify"]]]]],[["TermLang.Unify.reifyEnv",[[0,23,[[":name","TermLang.Unify.reifyEnv"],[":implicit",false],[":decor",":function"],[":doc-overview",""],[":type","Int -> Env -> TC (List Exp)"],[":namespace","TermLang.Unify"]]]]],["TermLang.Unify.unify",[[0,20,[[":name","TermLang.Unify.unify"],[":implicit",false],[":decor",":function"],[":doc-overview",""],[":type","Val -> Val -> TC ()"],[":namespace","TermLang.Unify"]]]]]]]]]}

https://code.visualstudio.com/docs/extensionAPI/vscode-api#ReferenceProvider

• Go to a concrete symbol in the currently opened file: cmd + p then press @, :browse-namespace command can offer some help here, also remove shift+cmd+o shortcut.
• Search a concrete symbol across the project: cmd + p then press #

https://code.visualstudio.com/docs/extensionAPI/vscode-api#DocumentSymbolProvider
https://code.visualstudio.com/docs/extensionAPI/vscode-api#WorkspaceSymbolProvider
https://github.com/hoovercj/vscode-ghc-mod/tree/master/client
https://github.com/Microsoft/vscode-go/blob/master/src/goOutline.ts
https://github.com/Microsoft/vscode-go/blob/master/src/goSymbol.ts