emvscode-web (Under development)

• VSCode for the Web Extension for Mizar

Note

• This extension only works on the web.
• Mizar Server must be running for the extension to function properly.

Demo

Command execution

Syntax highlight & Auto indent

Hover information

Features

• Mizar commands
  • Mizar Compile
  • Irrelevant Theorems
  • Irrelevant Iterative Steps
  • Irrelevant Inferences
  • Irrelevant Premises
  • Inaccessible Items
  • Trivial Proofs
  • Irrelevant Vocabularie
  • Irrelevant Label
• Syntax highlight
• Auto indent
• Hover information
• Go to definition
• Formatter
• Linter

Installation

1. Open VSCode for the Web and type "Ctrl+Shift+X".
2. Type "mizar" in the search box and click to install.

Usage

1. Fork mizar-server-contents
2. Start VSCode for the Web in the forked repository
3. Input the "Mizar.OAuthToken" field in the extension settings

Command Execution

• Type "Ctrl+Shift+P" (or click title bar icon) and choose a command.

Development

• Clone this repositry

  git clone https://github.com/mimosa-project/emvscode-web
  

• Change the current directory to emvscode directory

  cd emvscode-web
  

• Run "npm install"

  npm install
  

• reference
  • https://code.visualstudio.com/api/get-started/your-first-extension

Author

• Ryutaro Matsumoto

License

This project is licensed under the MIT License - see the LICENSE file for details.