starry-night/lang/source.lp.js at main · wooorm/starry-night · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
// This is a TextMate grammar distributed by `starry-night`.
// This grammar is developed at
// <https://github.com/Deducteam/sublime-lambdapi>
// and licensed `mit`.
// See <https://github.com/wooorm/starry-night> for more info.
/**
 * @import {Grammar} from '@wooorm/starry-night'
 */

/** @type {Grammar} */
const grammar = {
  extensions: [],
  names: ['lambdapi'],
  patterns: [
    {include: '#comments'},
    {include: '#tactics'},
    {include: '#signature-commands'},
    {include: '#warning'},
    {include: '#misc'},
    {include: '#keywords'},
    {include: '#external'}
  ],
  repository: {
    comments: {
      patterns: [
        {begin: '//', end: '$', name: 'comment.line.double-slash.lp'},
        {begin: '/\\*', end: '\\*/', name: 'comment.block.lp'}
      ]
    },
    external: {
      captures: {
        1: {name: 'storage.type.lp'},
        2: {name: 'entity.name.function.theorem.lp'}
      },
      match: '(open|require)\\s+(([^\\s+]*\\s+)*$)'
    },
    keywords: {
      match:
        '\\b(as|associative|begin|builtin|coerce_rule|commutative|constant|debug|end|flag|in|infix|injective|left|notation|off|on|opaque|postfix|prefix|private|protected|prover|prover_timeout|quantifier|right|sequential|TYPE|unif_rule)\\b',
      name: 'storage.modifier.lp'
    },
    misc: {
      match: '\\b(assert|assertnot|compute|print|proofterm|search|type)\\b',
      name: 'keyword.control.query.lp'
    },
    'signature-commands': {
      captures: {
        1: {name: 'storage.type.lp'},
        2: {name: 'entity.name.function.theorem.lp'}
      },
      match: '(coerce_rule|inductive|rule|symbol|unif_rule|with)\\s+([^\\s+]*)'
    },
    tactics: {
      match:
        '\\b(apply|assume|change|eval|focus|generalize|have|induction|orelse|refine|reflexivity|remove|repeat|rewrite|set|simplify|solve|symmetry|try|why3)\\b',
      name: 'keyword.control.tactics.lp'
    },
    warning: {
      match: '\\b(abort|admit|admitted|fail)\\b',
      name: 'keyword.control.warning.lp'
    }
  },
  scopeName: 'source.lp'
}

export default grammar