Gaze/SpaceVim
1
0
Fork 0
mirror of https://github.com/SpaceVim/SpaceVim.git synced 2025-02-02 23:10:06 +08:00
Code Issues Projects Releases Wiki Activity

Add lang#idris layer (#3081)

Browse Source
This commit is contained in:
Wang Shidong 2019-09-24 15:59:34 +08:00 committed by GitHub
parent bce3d34b00
commit bd8f1a0c05
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 201 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
autoload/SpaceVim/layers/core/statusline.vim
View File

@ -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'

55
autoload/SpaceVim/layers/lang/idris.vim Normal file
View File

@ -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(":")<ENTER>b:call idris#addClause(0)<ENTER>w', 'add-clause-for-type-declaration', 1, 0)
" nnoremap <buffer> <silent> <LocalLeader>b 0:call IdrisAddClause(0)<ENTER>
" nnoremap <buffer> <silent> <LocalLeader>md 0:call search(":")<ENTER>b:call IdrisAddClause(1)<ENTER>w
" nnoremap <buffer> <silent> <LocalLeader>mc :call IdrisMakeCase()<ENTER>
endfunction

4
autoload/SpaceVim/plugins/runner.vim
View File

@ -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, [])

2
docs/cn/layers.md
View File

@ -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 开发提供支持，包括交互式编程和语法高亮。 |

64
docs/cn/layers/lang/idris.md Normal file
View File

@ -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
<!-- vim-markdown-toc GFM -->
- [模块简介](#模块简介)
- [启用模块](#启用模块)
- [快捷键](#快捷键)
- [交互式编程](#交互式编程)
- [运行当前脚本](#运行当前脚本)
<!-- vim-markdown-toc -->
## 模块简介
这一模块为在 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` 快速异步运行当前文件，运行结果会展示在一个独立的执行窗口内。

2
docs/layers.md
View File

@ -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. |

71
docs/layers/lang/idris.md Normal file
View File

@ -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
<!-- vim-markdown-toc GFM -->
- [Description](#description)
- [Install](#install)
- [Features](#features)
- [Key bindings](#key-bindings)
- [Running current script](#running-current-script)
- [Inferior REPL process](#inferior-repl-process)
<!-- vim-markdown-toc -->
## 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 |

2
wiki/en/programming-languages.md
View File

@ -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