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 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.
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.
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.
There is a package called B/ProB Language Support available for the VSCode editor. It adds syntax highlighting and snippets for the specification languages B and Event-B to VSCode. It integrates with probcli to obtain error markers for syntax and type errors. It can also be used for well-definedness checking.
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. It integrates with probcli to obtain error markers for syntax and type errors.
With the Atom plugin you can now also visualize WD (well-definedness) issues in your B machines. See this small demo video.
Some BBedit Language modules for B, TLA+, CSP and Prolog are available.
A package File:B-mode.el.zip is available.