Editors for ProB

ProB Tcl/Tk Editor

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models. The editor of Tcl/Tk, however, has a few limitations:

• it can become very slow with long or very long lines
• the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu). You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

Launching the editor in probcli

The probcli REPL (read-eval-print-loop) supports the command :e to open the current file in the external editor, as specified in the "EDITOR" preference. You can set this preference using

probcli -repl -p EDITOR PATH

In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

External Editors

VIM

A VIM plugin for ProB is available. It shows a quick fix list of parse and type errors for classical B machines (.mch) using the command line tool probcli. VIM has builtin syntax highlighting support for B.

Atom

There is a package language-b-eventb available for the Atom editor. It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.

BBEdit

Some BBedit Language modules for B, TLA+, CSP and Prolog are available.

Emacs

A package File:B-mode.el.zip is available.