---

Ⅰ. 插件描述

Vim plugin for TLA+ and PlusCal

Ⅱ. 基本信息

创建日期：  2016-11-03 使用用户：  10 Github星：  15 插件作者：  Hillel Wayne

Ⅲ. 安装方法

使用Vundle管理器安装

在你的.vimrc下添加:

Plugin 'hwayne/tla-vim-hands-off'

… 然后在Vim中运行以下命令:

:source %
:PluginInstall

对于Vundle版本 < 0.10.2，请用上面的Bundle替换Plugin。

使用NeoBundle管理器安装

在你的.vimrc下添加:

NeoBundle 'hwayne/tla-vim-hands-off'

… 然后在Vim中运行以下命令:

:source %
:NeoBundleInstall

使用VimPlug管理器安装

在你的.vimrc下添加:

Plug 'hwayne/tla-vim-hands-off'

… 然后在Vim中运行以下命令:

:source %
:PlugInstall

使用Pathogen管理器安装

在终端中运行以下命令:

cd ~/.vim/bundle
git clone https://github.com/hwayne/tla.vim

Ⅳ. 文档说明

# tla.vim

Vim plugin for TLA+ and PlusCal. Helps with writing specs. Since there's no official TLA+ styleguide, it currently just implements my preferences. The plugin makes the following assumptions:

• You're using p-syntax. I prefer that to c-syntax because it doesn't overload the meaning of {} and makes the indentation file not hair-pullingly impossible.
• You're only using vim to write your spec, not to typeset or run models. Modelling is waaaaaay too complicated to be part of a text editor. Use the TLA+ Toolbox for that instead.

Current Functionality

• Some syntax highlighting
• Handles \* as a comment
• Autofolds PlusCal translations
• Functions for SANY and PlusCal translation
• Some indentation logic

Planned Functionality

• Command line options for PlusCal translation
• Documentation
• More indentation
• More syntax highlighting
• Better handling of editing PlusCal algorithms
• Vim Definitions

Pie-In-The-Sky Functionality

• Dumping SANY errors into a quickfix list
• A way to highlight expressions that are valid but not TLC-compatible
• Tags
• Rewrite in something that isn't Vimscript
• Making sure it plays nice with TLA+2