Differential D27797

Agda: keywords updated to 2.6.0 and fix float points
ClosedPublic
Actions

Authored by nibags on Mar 3 2020, 6:38 AM.

Details

Reviewers
dhaumann
cullmann
Group Reviewers
Framework: Syntax Highlighting
Commits
R216:6903aff4ef92: Agda: keywords updated to 2.6.0 and fix float points
Summary

New keywords are added, this corresponds to the pull request:
https://github.com/KDE/syntax-highlighting/pull/23

I also added a test file, which I obtained from: https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda

When I saw the test file, I noticed some problems in the highlighting of floating point. So I fixed this, according to the lexical described in the Agda documentation: https://agda.readthedocs.io/en/latest/language/lexical-structure.html#literals

In addition, I added folded and ##Alerts in the comments.

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.
nibags created this revision.Mar 3 2020, 6:38 AM
Restricted Application added projects: Kate, Frameworks. · View Herald TranscriptMar 3 2020, 6:38 AM
Restricted Application added subscribers: kde-frameworks-devel, kwrite-devel. · View Herald Transcript
nibags requested review of this revision.Mar 3 2020, 6:38 AM
cullmann accepted this revision.Mar 7 2020, 4:11 PM

Thanks for taking care of this!
Let's get that in.

This revision is now accepted and ready to land.Mar 7 2020, 4:11 PM
Closed by commit R216:6903aff4ef92: Agda: keywords updated to 2.6.0 and fix float points (authored by nibags, committed by cullmann). · Explain WhyMar 7 2020, 4:12 PM
This revision was automatically updated to reflect the committed changes.

Showing Only Differences

This revision modifies 5 more files that are hidden because they were not modified between selected diffs and they have no inline comments.

Revision Contents
Changeset List

Path
No data available.

Diff 77175