MMT Online Tools (mmteditor)

Online tools for the MMT language and ecosystem.

See in action at https://comfreek.github.io/mmteditor/.

• MMT QuickEditor: Editor with syntax highlighting and abbreviation autocompletion.

  

• "How do I type X?": Find out how to type things you encountered.

  

• Abbreviation Search: Find out the abbreviation whose name you only partly remember.

  

• Bare Editor: A bare full-screen MMT editor within your browser (available at https://comfreek.github.io/mmteditor/bare.html)

  You can also use the bare editor as a "reusable component" on external sites: include an <iframe src="https://comfreek.github.io/mmteditor/bare.html"></iframe> on your site, and then via JS call postMessage() on the iframe's contentWindow property with the following event data:

  {
      "command": "set-content",
      "content": "the content you want the editor to display"
  }

  For example, the SyntaxPresenterServer within the MMT API uses the bare editor this way.

Development Notes

Testing locally

1. Get an HTTP server, e.g. http-server from NPM: npm i http-server -g.

2. Run the HTTP server, e.g. http-server ..

3. Go to http://127.0.0.1:8080/index.html and http://127.0.0.1:8080/bare.html and test things manually (type random (in)valid MMT syntax, test autocomplete).

   It is strongly recommended to open the developer tools in your browser and deactivate caching in the network tab.

Updating MMT's abbreviation map

Regularly update the raw abbreviation data in abbreviations.js by copying everything from https://github.com/UniFormal/MMT/blob/devel/src/mmt-api/resources/unicode/unicode-latex-map. Detailed instructions can be found in abbreviations.js.

Updating CodeMirror

Suppose CodeMirror releases a new version X.Y.Z. Hopefully, Renovate already filed a pull request. Then do:

1. Hopefully the codemirror/CodeMirror repository on GitHub contains a corresponding tag X.Y.Z.

2. From within this repository, cd codemirror and do:

   1. git remote add upstream https://github.com/codemirror/CodeMirror.git (if not already existing)
   2. git remote set-url origin --push git@github.com:ComFreek/CodeMirror.git (if not already done)
   3. git fetch upstream --tags
   4. git merge X.Y.Z
   5. git commit -m "..." (in case of merge conflicts) and git push origin

3. In case Renovate filed a pull request, do git fetch and git merge origin/renovate/codemirror-x.y.

   Confirm that in both files index.html and bare.html, the URIs referencing CodeMirror resources (<script src="..."> and <link href="...">) really contain the updated version. If not or if Renovate did not file a pull request at all, update these versions in the URIs manually.

4. Test whether things work locally (see above under Testing locally).

5. git add --all, git commit -m "Update CodeMirror to X.Y.Z", git push