Add syntax highlighting for Metamath
ClosedPublic

Authored by aaronpuchert on Aug 12 2017, 9:46 PM.

Details

Summary

Metamath is a formal language to express mathematical theorems and
proofs developed by Norman Megill. [1, 2]

The language is defined in the documentation [3, Chapter 4]. The syntax
highlighter is a bit lenient sometimes. When encountering symbols, we
highlight them as variables, because only semantic analysis could tell
if they are symbols instead.

The test is a modified version of the file demo0.mm in [4], where I
removed most of the comments.

I'm not sure if we should set a priority, because apparently Objective-
C++ files have the same extension. Right now it is a toss-up between the
two languages.

[1] http://us.metamath.org/
[2] https://en.wikipedia.org/wiki/Metamath
[3] http://us.metamath.org/downloads/metamath.pdf
[4] http://us.metamath.org/downloads/metamath.tar.bz2

Diff Detail

Repository
R216 Syntax Highlighting
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
aaronpuchert created this revision.Aug 12 2017, 9:46 PM
Restricted Application added a project: Frameworks. · View Herald TranscriptAug 12 2017, 9:46 PM

There are screenshots of other (known) syntax highlighters for Metamath on their homepage.

Looks already pretty good. But please change the license to MIT. We agreed to using MIT license for new syntax-highlighting files. Could you update the review request again?

Also can you commit yourself (i.e. Do you have a commit account? ) or shall I commit for you?

data/syntax/metamath.xml
8

Can you change the license to MIT?

aaronpuchert marked an inline comment as done.Aug 13 2017, 12:12 PM

I don't have a commit account, so I'd need you to commit the changes.

data/syntax/metamath.xml
8

No problem. I was just looking what others were using, and GPL was (still) more common.

The documentation also says: "license contains the license, usually LGPL, Artistic, GPL or others."

aaronpuchert marked an inline comment as done.

Changed license to MIT.

Fix commit message and indentation.

dhaumann accepted this revision.Aug 20 2017, 8:55 PM

Looks good to me. Will integrate this soon.

By the way, you may want to apply for a KDE contributor account to commit your changes yourself, especially since you are providing patches already since April or so, see:
https://community.kde.org/Infrastructure/Get_a_Developer_Account

This revision is now accepted and ready to land.Aug 20 2017, 8:55 PM
This revision was automatically updated to reflect the committed changes.