From bd8f1a0c054c13ad807f8e63fcaf483cdc737341 Mon Sep 17 00:00:00 2001 From: Wang Shidong Date: Tue, 24 Sep 2019 15:59:34 +0800 Subject: [PATCH] Add lang#idris layer (#3081) --- autoload/SpaceVim/layers/core/statusline.vim | 2 + autoload/SpaceVim/layers/lang/idris.vim | 55 +++++++++++++++ autoload/SpaceVim/plugins/runner.vim | 4 ++ docs/cn/layers.md | 2 + docs/cn/layers/lang/idris.md | 64 ++++++++++++++++++ docs/layers.md | 2 + docs/layers/lang/idris.md | 71 ++++++++++++++++++++ wiki/en/programming-languages.md | 2 +- 8 files changed, 201 insertions(+), 1 deletion(-) create mode 100644 autoload/SpaceVim/layers/lang/idris.vim create mode 100644 docs/cn/layers/lang/idris.md create mode 100644 docs/layers/lang/idris.md diff --git a/autoload/SpaceVim/layers/core/statusline.vim b/autoload/SpaceVim/layers/core/statusline.vim index 3192b18f3..6c0954743 100644 --- a/autoload/SpaceVim/layers/core/statusline.vim +++ b/autoload/SpaceVim/layers/core/statusline.vim @@ -411,6 +411,8 @@ function! SpaceVim#layers#core#statusline#get(...) abort \ . '%#SpaceVim_statusline_b# LayerManager %#SpaceVim_statusline_b_SpaceVim_statusline_c#' . s:lsep elseif &filetype ==# 'SpaceVimGitLogPopup' return '%#SpaceVim_statusline_a# Git log popup %#SpaceVim_statusline_a_SpaceVim_statusline_b#' . s:lsep + elseif &filetype ==# 'respones.idris' + return '%#SpaceVim_statusline_a# Idris Response %#SpaceVim_statusline_a_SpaceVim_statusline_b#' . s:lsep elseif &filetype ==# 'SpaceVimWinDiskManager' return '%#SpaceVim_statusline_a# WinDisk %#SpaceVim_statusline_a_SpaceVim_statusline_b#' . s:lsep elseif &filetype ==# 'SpaceVimTodoManager' diff --git a/autoload/SpaceVim/layers/lang/idris.vim b/autoload/SpaceVim/layers/lang/idris.vim new file mode 100644 index 000000000..e8798d510 --- /dev/null +++ b/autoload/SpaceVim/layers/lang/idris.vim @@ -0,0 +1,55 @@ +"============================================================================= +" idris.vim --- idris language support +" Copyright (c) 2016-2019 Wang Shidong & Contributors +" Author: Wang Shidong < wsdjeg@outlook.com > +" URL: https://spacevim.org +" License: GPLv3 +"============================================================================= + + +function! SpaceVim#layers#lang#idris#plugins() abort + let plugins = [] + call add(plugins, ['wsdjeg/vim-idris', { 'merged' : 0}]) + return plugins +endfunction + +function! SpaceVim#layers#lang#idris#config() abort + call SpaceVim#plugins#repl#reg('idris', 'idris --nobanner') + call SpaceVim#plugins#runner#reg_runner('idris', ['idris %s -o #TEMP#', '#TEMP#']) + call SpaceVim#mapping#space#regesit_lang_mappings('idris', function('s:language_specified_mappings')) +endfunction + +function! s:language_specified_mappings() abort + call SpaceVim#mapping#space#langSPC('nmap', ['l','r'], 'call SpaceVim#plugins#runner#open()', 'execute current file', 1) + let g:_spacevim_mappings_space.l.s = {'name' : '+Send'} + call SpaceVim#mapping#space#langSPC('nmap', ['l','s', 'i'], + \ 'call SpaceVim#plugins#repl#start("idris")', + \ 'start REPL process', 1) + call SpaceVim#mapping#space#langSPC('nmap', ['l','s', 'l'], + \ 'call SpaceVim#plugins#repl#send("line")', + \ 'send line and keep code buffer focused', 1) + call SpaceVim#mapping#space#langSPC('nmap', ['l','s', 'b'], + \ 'call SpaceVim#plugins#repl#send("buffer")', + \ 'send buffer and keep code buffer focused', 1) + call SpaceVim#mapping#space#langSPC('nmap', ['l','s', 's'], + \ 'call SpaceVim#plugins#repl#send("selection")', + \ 'send selection and keep code buffer focused', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','w'], 'call idris#makeWith()', 'add-with-clause', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','t'], 'call idris#showType()', 'show-type', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','p'], 'call idris#proofSearch(1)', 'proof-search', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','o'], 'call idris#proofSearch(1)', 'obvious-proof-search', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','a'], 'call idris#reload(0)', 'reload-file', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','c'], 'call idris#caseSplit()', 'case-split', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','f'], 'call idris#refine()', 'refine-item', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','l'], 'call idris#makeLemma()', 'make lemma', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','h'], 'call idris#showDoc()', 'show doc', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','m'], 'call idris#addMissing()', 'add missing', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','e'], 'call idris#eval()', 'idris eval', 1) + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','i'], 'call idris#responseWin()', 'open-response-win', 1) + let g:_spacevim_mappings_space.l.d = {'name' : '+Add clause'} + call SpaceVim#mapping#space#langSPC('nnoremap', ['l','d', 'f'], '0:call search(":")b:call idris#addClause(0)w', 'add-clause-for-type-declaration', 1, 0) + + " nnoremap b 0:call IdrisAddClause(0) + " nnoremap md 0:call search(":")b:call IdrisAddClause(1)w + " nnoremap mc :call IdrisMakeCase() +endfunction diff --git a/autoload/SpaceVim/plugins/runner.vim b/autoload/SpaceVim/plugins/runner.vim index e8131098b..d73a95be3 100644 --- a/autoload/SpaceVim/plugins/runner.vim +++ b/autoload/SpaceVim/plugins/runner.vim @@ -72,6 +72,10 @@ function! s:async_run(runner) abort " the runner is a list " the first item is compile cmd, and the second one is running cmd. let s:target = s:FILE.unify_path(tempname(), ':p') + let dir = fnamemodify(s:target, ':h') + if isdirectory(dir) + call mkdir(dir, 'p') + endif if type(a:runner[0]) == type({}) if type(a:runner[0].exe) == 2 let exe = call(a:runner[0].exe, []) diff --git a/docs/cn/layers.md b/docs/cn/layers.md index 3aa708b3c..ae1dfbc59 100644 --- a/docs/cn/layers.md +++ b/docs/cn/layers.md @@ -87,6 +87,7 @@ Vim 插件以及相关配置。而 SpaceVim 是以模块的方式来组织和管 | [lang#asciidoc](lang/asciidoc/) | 这一模块为 SpaceVim 提供了 AsciiDoc 的编辑支持，包括格式化、自动生成文章目录、代码块等特性。 | | [lang#assembly](lang/assembly/) | 该模块为 SpaceVim 提供了 Assembly 语言开发支持，包括语法高亮。 | | [lang#autohotkey](lang/autohotkey/) | 这一模块为 SpaceVim 提供了 Autohotkey 的开发支持，包括语法高亮和自动补全等功能。 | +| [lang#batch](lang/batch/) | 这一模块为 batch 开发提供支持，包括交互式编程、一键运行等特性。 | | [lang#c](lang/c/) | 这一模块为 SpaceVim 提供了 C/C++/Object-C 的开发支持，包括代码补全、语法检查等特性。 | | [lang#clojure](lang/clojure/) | 这一模块为 SpaceVim 提供了 Clojure 的开发支持，包括代码补全、语法检查、代码格式化等特性。 | | [lang#crystal](lang/crystal/) | 这一模块为 crystal 开发提供支持，包括交互式编程、一键运行等特性。 | @@ -106,6 +107,7 @@ Vim 插件以及相关配置。而 SpaceVim 是以模块的方式来组织和管 | [lang#haskell](lang/haskell/) | 这一模块为 SpaceVim 提供了 Haskell 的开发支持，包括代码补全、语法检查、代码格式化等特性。 | | [lang#html](lang/html/) | 这一模块为 SpaceVim 提供了 HTML 的开发支持，包括代码补全、语法检查、代码格式化等特性。 | | [lang#hy](lang/hy/) | 这一模块为 hy 开发提供支持，包括交互式编程、一键运行等特性。 | +| [lang#idris](lang/idris/) | 这一模块为 idris 开发提供支持，包括交互式编程、一键运行等特性。 | | [lang#io](lang/io/) | 这一模块为 io 开发提供支持，包括交互式编程、一键运行等特性。 | | [lang#ipynb](lang/ipynb/) | 该模块为 SpaceVim 添加了 Jupyter Notebook 支持，包括语法高亮、代码折叠等特点。 | | [lang#j](lang/j/) | 这一模块为 j 开发提供支持，包括交互式编程和语法高亮。 | diff --git a/docs/cn/layers/lang/idris.md b/docs/cn/layers/lang/idris.md new file mode 100644 index 000000000..7dfb794db --- /dev/null +++ b/docs/cn/layers/lang/idris.md @@ -0,0 +1,64 @@ +--- +title: "SpaceVim lang#idris 模块" +description: "这一模块为 idris 开发提供支持，包括交互式编程、一键运行等特性。" +image: https://user-images.githubusercontent.com/13142418/65492491-9dece000-dee3-11e9-8eda-7d41a6c1ee79.png +lang: cn +--- + +# [可用模块](../../) >> lang#idris + + + +- [模块简介](#模块简介) +- [启用模块](#启用模块) +- [快捷键](#快捷键) + - [交互式编程](#交互式编程) + - [运行当前脚本](#运行当前脚本) + + + +## 模块简介 + +这一模块为在 SpaceVim 中进行 idris 开发提供了支持，该模块主要基于插件：[wsdjeg/vim-idris](https://github.com/wsdjeg/vim-idris)。 + +## 启用模块 + +可通过在配置文件内加入如下配置来启用该模块： + +```toml +[[layers]] + name = "lang#idris" +``` + +## 快捷键 + +| 快捷键 | 功能描述 | +| --------- | -------------------- | +| `SPC l a` | 重新载入当前文件 | +| `SPC l w` | add with clause | +| `SPC l t` | 显示光标变量类型 | +| `SPC l p` | proof search | +| `SPC l o` | obvious proof search | +| `SPC l c` | case split | +| `SPC l f` | refine item | +| `SPC l l` | make lemma | +| `SPC l m` | add missing | +| `SPC l h` | 显示光标函数文档 | +| `SPC l e` | idris 求值 | +| `SPC l i` | 打开应答窗口 | + +### 交互式编程 + +启动 `idris --nobanner` 交互进程，快捷键为： `SPC l s i`。 + +将代码传输给 REPL 进程执行： + +| 快捷键 | 功能描述 | +| ----------- | ----------------------- | +| `SPC l s b` | 发送整个文件内容至 REPL | +| `SPC l s l` | 发送当前行内容至 REPL | +| `SPC l s s` | 发送已选中的内容至 REPL | + +### 运行当前脚本 + +在编辑 idris 文件时，可通过快捷键 `SPC l r` 快速异步运行当前文件，运行结果会展示在一个独立的执行窗口内。 diff --git a/docs/layers.md b/docs/layers.md index 5a2e1e6e9..f6f1acdd7 100644 --- a/docs/layers.md +++ b/docs/layers.md @@ -93,6 +93,7 @@ Some layers are enabled by default. The following example shows how to disable ` | [lang#asciidoc](lang/asciidoc/) | Edit AsciiDoc within vim, autopreview AsciiDoc in the default browser, with this layer you can also format AsciiDoc file. | | [lang#assembly](lang/assembly/) | This layer adds Assembly language support to SpaceVim, including syntax highlighting. | | [lang#autohotkey](lang/autohotkey/) | This layer adds AutohotKey language support to SpaceVim. | +| [lang#batch](lang/batch/) | This layer is for DOS batch file development, provide syntax highlighting, code runner and repl support for batch file. | | [lang#c](lang/c/) | C/C++/Object-C language support for SpaceVim, include code completion, jump to definition, quick runner. | | [lang#clojure](lang/clojure/) | This layer is for Clojure development, provide autocompletion, syntax checking, code format for Clojure file. | | [lang#coffeescript](lang/coffeescript/) | This layer is for CoffeeScript development, provide autocompletion, syntax checking, code format for CoffeeScript file. | @@ -114,6 +115,7 @@ Some layers are enabled by default. The following example shows how to disable ` | [lang#haskell](lang/haskell/) | Haskell language support for SpaceVim, includes code completion, syntax checking, jumping to definition, also provides language server protocol support for Haskell | | [lang#html](lang/html/) | Edit html in SpaceVim, with this layer, this layer provides code completion, syntax checking and code formatting for html. | | [lang#hy](lang/hy/) | This layer is for hy development, provide syntax checking, code runner and repl support for hy file. | +| [lang#idris](lang/idris/) | This layer is for idris development, provide syntax checking, code runner and repl support for idris file. | | [lang#io](lang/io/) | This layer is for io development, provide code runner and repl support for io file. | | [lang#ipynb](lang/ipynb/) | This layer adds Jupyter Notebook support to SpaceVim | | [lang#j](lang/j/) | This layer is for j development, provide syntax checking and repl support for j file. | diff --git a/docs/layers/lang/idris.md b/docs/layers/lang/idris.md new file mode 100644 index 000000000..b0f8f4db4 --- /dev/null +++ b/docs/layers/lang/idris.md @@ -0,0 +1,71 @@ +--- +title: "SpaceVim lang#idris layer" +description: "This layer is for idris development, provide syntax checking, code runner and repl support for idris file." +image: https://user-images.githubusercontent.com/13142418/65492491-9dece000-dee3-11e9-8eda-7d41a6c1ee79.png +--- + +# [Available Layers](../../) >> lang#idris + + + +- [Description](#description) +- [Install](#install) +- [Features](#features) +- [Key bindings](#key-bindings) + - [Running current script](#running-current-script) + - [Inferior REPL process](#inferior-repl-process) + + + +## Description + +This layer is for idris development, which is based on [wsdjeg/vim-idris](https://github.com/wsdjeg/vim-idris). + +## Install + +To use this configuration layer, update custom configuration file with: + +```toml +[[layers]] + name = "lang#idris" +``` + +## Features + +- repl support +- code runner +- show symbol doc +- show symbol type + +## Key bindings + +| Key Bindings | Descriptions | +| ------------ | -------------------- | +| `SPC l a` | reload current file | +| `SPC l w` | add with clause | +| `SPC l t` | show type | +| `SPC l p` | proof search | +| `SPC l o` | obvious proof search | +| `SPC l c` | case split | +| `SPC l f` | refine item | +| `SPC l l` | make lemma | +| `SPC l m` | add missing | +| `SPC l h` | show doc | +| `SPC l e` | idris eval | +| `SPC l i` | open response win | + +### Running current script + +To running a idris file, you can press `SPC l r` to run current file without loss focus, and the result will be shown in a runner buffer. + +### Inferior REPL process + +Start a `idris --nobanner` inferior REPL process with `SPC l s i`. + +Send code to inferior process commands: + +| Key Bindings | Descriptions | +| ------------ | ------------------------------------------------ | +| `SPC l s b` | send buffer and keep code buffer focused | +| `SPC l s l` | send line and keep code buffer focused | +| `SPC l s s` | send selection text and keep code buffer focused | diff --git a/wiki/en/programming-languages.md b/wiki/en/programming-languages.md index 1fdf94df0..a2c4758af 100644 --- a/wiki/en/programming-languages.md +++ b/wiki/en/programming-languages.md @@ -39,6 +39,7 @@ | Rust | lang#rust | | Scala | lang#scala | | Scheme | lang#scheme | +| idris | lang#idris | | Swift | lang#swift | | TypeScript | lang#typescript | | clojure | [lang#clojure](https://spacevim.org/layers/lang/clojure/) | @@ -270,7 +271,6 @@ - micropython/micropython - AssemblyScript/assemblyscript - Frege/frege -- idris-lang/Idris-dev - typelead/eta - programming-nu/nu - zdevito/terra