Coverage for /pythoncovmergedfiles/medio/medio/usr/local/lib/python3.8/site-packages/pygments/lexers/theorem.py: 97%

58 statements  

« prev     ^ index     » next       coverage.py v7.3.1, created at 2023-09-18 06:13 +0000

1""" 

2 pygments.lexers.theorem 

3 ~~~~~~~~~~~~~~~~~~~~~~~ 

4 

5 Lexers for theorem-proving languages. 

6 

7 :copyright: Copyright 2006-2023 by the Pygments team, see AUTHORS. 

8 :license: BSD, see LICENSE for details. 

9""" 

10 

11import re 

12 

13from pygments.lexer import RegexLexer, default, words, include 

14from pygments.token import Text, Comment, Operator, Keyword, Name, String, \ 

15 Number, Punctuation, Generic, Whitespace 

16 

17__all__ = ['CoqLexer', 'IsabelleLexer', 'LeanLexer'] 

18 

19 

20class CoqLexer(RegexLexer): 

21 """ 

22 For the Coq theorem prover. 

23 

24 .. versionadded:: 1.5 

25 """ 

26 

27 name = 'Coq' 

28 url = 'http://coq.inria.fr/' 

29 aliases = ['coq'] 

30 filenames = ['*.v'] 

31 mimetypes = ['text/x-coq'] 

32 

33 flags = 0 # no re.MULTILINE 

34 

35 keywords1 = ( 

36 # Vernacular commands 

37 'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Variable', 

38 'Variables', 'Parameter', 'Parameters', 'Axiom', 'Axioms', 'Hypothesis', 

39 'Hypotheses', 'Notation', 'Local', 'Tactic', 'Reserved', 'Scope', 

40 'Open', 'Close', 'Bind', 'Delimit', 'Definition', 'Example', 'Let', 

41 'Ltac', 'Fixpoint', 'CoFixpoint', 'Morphism', 'Relation', 'Implicit', 

42 'Arguments', 'Types', 'Unset', 'Contextual', 'Strict', 'Prenex', 

43 'Implicits', 'Inductive', 'CoInductive', 'Record', 'Structure', 

44 'Variant', 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Fact', 

45 'Remark', 'Corollary', 'Proposition', 'Property', 'Goal', 

46 'Proof', 'Restart', 'Save', 'Qed', 'Defined', 'Abort', 'Admitted', 

47 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', 'Compute', 'Eval', 

48 'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside', 

49 'outside', 'Check', 'Global', 'Instance', 'Class', 'Existing', 

50 'Universe', 'Polymorphic', 'Monomorphic', 'Context', 'Scheme', 'From', 

51 'Undo', 'Fail', 'Function', 

52 ) 

53 keywords2 = ( 

54 # Gallina 

55 'forall', 'exists', 'exists2', 'fun', 'fix', 'cofix', 'struct', 

56 'match', 'end', 'in', 'return', 'let', 'if', 'is', 'then', 'else', 

57 'for', 'of', 'nosimpl', 'with', 'as', 

58 ) 

59 keywords3 = ( 

60 # Sorts 

61 'Type', 'Prop', 'SProp', 'Set', 

62 ) 

63 keywords4 = ( 

64 # Tactics 

65 'pose', 'set', 'move', 'case', 'elim', 'apply', 'clear', 'hnf', 'intro', 

66 'intros', 'generalize', 'rename', 'pattern', 'after', 'destruct', 

67 'induction', 'using', 'refine', 'inversion', 'injection', 'rewrite', 

68 'congr', 'unlock', 'compute', 'ring', 'field', 'replace', 'fold', 

69 'unfold', 'change', 'cutrewrite', 'simpl', 'have', 'suff', 'wlog', 

70 'suffices', 'without', 'loss', 'nat_norm', 'assert', 'cut', 'trivial', 

71 'revert', 'bool_congr', 'nat_congr', 'symmetry', 'transitivity', 'auto', 

72 'split', 'left', 'right', 'autorewrite', 'tauto', 'setoid_rewrite', 

73 'intuition', 'eauto', 'eapply', 'econstructor', 'etransitivity', 

74 'constructor', 'erewrite', 'red', 'cbv', 'lazy', 'vm_compute', 

75 'native_compute', 'subst', 

76 ) 

77 keywords5 = ( 

78 # Terminators 

79 'by', 'now', 'done', 'exact', 'reflexivity', 

80 'tauto', 'romega', 'omega', 'lia', 'nia', 'lra', 'nra', 'psatz', 

81 'assumption', 'solve', 'contradiction', 'discriminate', 

82 'congruence', 'admit' 

83 ) 

84 keywords6 = ( 

85 # Control 

86 'do', 'last', 'first', 'try', 'idtac', 'repeat', 

87 ) 

88 # 'as', 'assert', 'begin', 'class', 'constraint', 'do', 'done', 

89 # 'downto', 'else', 'end', 'exception', 'external', 'false', 

90 # 'for', 'fun', 'function', 'functor', 'if', 'in', 'include', 

91 # 'inherit', 'initializer', 'lazy', 'let', 'match', 'method', 

92 # 'module', 'mutable', 'new', 'object', 'of', 'open', 'private', 

93 # 'raise', 'rec', 'sig', 'struct', 'then', 'to', 'true', 'try', 

94 # 'type', 'val', 'virtual', 'when', 'while', 'with' 

95 keyopts = ( 

96 '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', r'-\.', 

97 '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', '<-', 

98 '<->', '=', '>', '>]', r'>\}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>', 

99 r'\[\|', ']', '_', '`', r'\{', r'\{<', r'\|', r'\|]', r'\}', '~', '=>', 

100 r'/\\', r'\\/', r'\{\|', r'\|\}', 

101 # 'Π', 'Σ', # Not defined in the standard library 

102 'λ', '¬', '∧', '∨', '∀', '∃', '→', '↔', '≠', '≤', '≥', 

103 ) 

104 operators = r'[!$%&*+\./:<=>?@^|~-]' 

105 prefix_syms = r'[!?~]' 

106 infix_syms = r'[=<>@^|&+\*/$%-]' 

107 

108 tokens = { 

109 'root': [ 

110 (r'\s+', Text), 

111 (r'false|true|\(\)|\[\]', Name.Builtin.Pseudo), 

112 (r'\(\*', Comment, 'comment'), 

113 (r'\b(?:[^\W\d][\w\']*\.)+[^\W\d][\w\']*\b', Name), 

114 (r'\bEquations\b\??', Keyword.Namespace), 

115 # Very weak heuristic to distinguish the Set vernacular from the Set sort 

116 (r'\bSet(?=[ \t]+[A-Z][a-z][^\n]*?\.)', Keyword.Namespace), 

117 (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), 

118 (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), 

119 (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), 

120 (words(keywords4, prefix=r'\b', suffix=r'\b'), Keyword), 

121 (words(keywords5, prefix=r'\b', suffix=r'\b'), Keyword.Pseudo), 

122 (words(keywords6, prefix=r'\b', suffix=r'\b'), Keyword.Reserved), 

123 # (r'\b([A-Z][\w\']*)(\.)', Name.Namespace, 'dotted'), 

124 (r'\b([A-Z][\w\']*)', Name), 

125 (r'(%s)' % '|'.join(keyopts[::-1]), Operator), 

126 (r'(%s|%s)?%s' % (infix_syms, prefix_syms, operators), Operator), 

127 

128 (r"[^\W\d][\w']*", Name), 

129 

130 (r'\d[\d_]*', Number.Integer), 

131 (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex), 

132 (r'0[oO][0-7][0-7_]*', Number.Oct), 

133 (r'0[bB][01][01_]*', Number.Bin), 

134 (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float), 

135 

136 (r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'", String.Char), 

137 

138 (r"'.'", String.Char), 

139 (r"'", Keyword), # a stray quote is another syntax element 

140 

141 (r'"', String.Double, 'string'), 

142 

143 (r'[~?][a-z][\w\']*:', Name), 

144 (r'\S', Name.Builtin.Pseudo), 

145 ], 

146 'comment': [ 

147 (r'[^(*)]+', Comment), 

148 (r'\(\*', Comment, '#push'), 

149 (r'\*\)', Comment, '#pop'), 

150 (r'[(*)]', Comment), 

151 ], 

152 'string': [ 

153 (r'[^"]+', String.Double), 

154 (r'""', String.Double), 

155 (r'"', String.Double, '#pop'), 

156 ], 

157 'dotted': [ 

158 (r'\s+', Text), 

159 (r'\.', Punctuation), 

160 (r'[A-Z][\w\']*(?=\s*\.)', Name.Namespace), 

161 (r'[A-Z][\w\']*', Name.Class, '#pop'), 

162 (r'[a-z][a-z0-9_\']*', Name, '#pop'), 

163 default('#pop') 

164 ], 

165 } 

166 

167 def analyse_text(text): 

168 if 'Qed' in text and 'Proof' in text: 

169 return 1 

170 

171 

172class IsabelleLexer(RegexLexer): 

173 """ 

174 For the Isabelle proof assistant. 

175 

176 .. versionadded:: 2.0 

177 """ 

178 

179 name = 'Isabelle' 

180 url = 'https://isabelle.in.tum.de/' 

181 aliases = ['isabelle'] 

182 filenames = ['*.thy'] 

183 mimetypes = ['text/x-isabelle'] 

184 

185 keyword_minor = ( 

186 'and', 'assumes', 'attach', 'avoids', 'binder', 'checking', 

187 'class_instance', 'class_relation', 'code_module', 'congs', 

188 'constant', 'constrains', 'datatypes', 'defines', 'file', 'fixes', 

189 'for', 'functions', 'hints', 'identifier', 'if', 'imports', 'in', 

190 'includes', 'infix', 'infixl', 'infixr', 'is', 'keywords', 'lazy', 

191 'module_name', 'monos', 'morphisms', 'no_discs_sels', 'notes', 

192 'obtains', 'open', 'output', 'overloaded', 'parametric', 'permissive', 

193 'pervasive', 'rep_compat', 'shows', 'structure', 'type_class', 

194 'type_constructor', 'unchecked', 'unsafe', 'where', 

195 ) 

196 

197 keyword_diag = ( 

198 'ML_command', 'ML_val', 'class_deps', 'code_deps', 'code_thms', 

199 'display_drafts', 'find_consts', 'find_theorems', 'find_unused_assms', 

200 'full_prf', 'help', 'locale_deps', 'nitpick', 'pr', 'prf', 

201 'print_abbrevs', 'print_antiquotations', 'print_attributes', 

202 'print_binds', 'print_bnfs', 'print_bundles', 

203 'print_case_translations', 'print_cases', 'print_claset', 

204 'print_classes', 'print_codeproc', 'print_codesetup', 

205 'print_coercions', 'print_commands', 'print_context', 

206 'print_defn_rules', 'print_dependencies', 'print_facts', 

207 'print_induct_rules', 'print_inductives', 'print_interps', 

208 'print_locale', 'print_locales', 'print_methods', 'print_options', 

209 'print_orders', 'print_quot_maps', 'print_quotconsts', 

210 'print_quotients', 'print_quotientsQ3', 'print_quotmapsQ3', 

211 'print_rules', 'print_simpset', 'print_state', 'print_statement', 

212 'print_syntax', 'print_theorems', 'print_theory', 'print_trans_rules', 

213 'prop', 'pwd', 'quickcheck', 'refute', 'sledgehammer', 'smt_status', 

214 'solve_direct', 'spark_status', 'term', 'thm', 'thm_deps', 'thy_deps', 

215 'try', 'try0', 'typ', 'unused_thms', 'value', 'values', 'welcome', 

216 'print_ML_antiquotations', 'print_term_bindings', 'values_prolog', 

217 ) 

218 

219 keyword_thy = ('theory', 'begin', 'end') 

220 

221 keyword_section = ('header', 'chapter') 

222 

223 keyword_subsection = ( 

224 'section', 'subsection', 'subsubsection', 'sect', 'subsect', 

225 'subsubsect', 

226 ) 

227 

228 keyword_theory_decl = ( 

229 'ML', 'ML_file', 'abbreviation', 'adhoc_overloading', 'arities', 

230 'atom_decl', 'attribute_setup', 'axiomatization', 'bundle', 

231 'case_of_simps', 'class', 'classes', 'classrel', 'codatatype', 

232 'code_abort', 'code_class', 'code_const', 'code_datatype', 

233 'code_identifier', 'code_include', 'code_instance', 'code_modulename', 

234 'code_monad', 'code_printing', 'code_reflect', 'code_reserved', 

235 'code_type', 'coinductive', 'coinductive_set', 'consts', 'context', 

236 'datatype', 'datatype_new', 'datatype_new_compat', 'declaration', 

237 'declare', 'default_sort', 'defer_recdef', 'definition', 'defs', 

238 'domain', 'domain_isomorphism', 'domaindef', 'equivariance', 

239 'export_code', 'extract', 'extract_type', 'fixrec', 'fun', 

240 'fun_cases', 'hide_class', 'hide_const', 'hide_fact', 'hide_type', 

241 'import_const_map', 'import_file', 'import_tptp', 'import_type_map', 

242 'inductive', 'inductive_set', 'instantiation', 'judgment', 'lemmas', 

243 'lifting_forget', 'lifting_update', 'local_setup', 'locale', 

244 'method_setup', 'nitpick_params', 'no_adhoc_overloading', 

245 'no_notation', 'no_syntax', 'no_translations', 'no_type_notation', 

246 'nominal_datatype', 'nonterminal', 'notation', 'notepad', 'oracle', 

247 'overloading', 'parse_ast_translation', 'parse_translation', 

248 'partial_function', 'primcorec', 'primrec', 'primrec_new', 

249 'print_ast_translation', 'print_translation', 'quickcheck_generator', 

250 'quickcheck_params', 'realizability', 'realizers', 'recdef', 'record', 

251 'refute_params', 'setup', 'setup_lifting', 'simproc_setup', 

252 'simps_of_case', 'sledgehammer_params', 'spark_end', 'spark_open', 

253 'spark_open_siv', 'spark_open_vcg', 'spark_proof_functions', 

254 'spark_types', 'statespace', 'syntax', 'syntax_declaration', 'text', 

255 'text_raw', 'theorems', 'translations', 'type_notation', 

256 'type_synonym', 'typed_print_translation', 'typedecl', 'hoarestate', 

257 'install_C_file', 'install_C_types', 'wpc_setup', 'c_defs', 'c_types', 

258 'memsafe', 'SML_export', 'SML_file', 'SML_import', 'approximate', 

259 'bnf_axiomatization', 'cartouche', 'datatype_compat', 

260 'free_constructors', 'functor', 'nominal_function', 

261 'nominal_termination', 'permanent_interpretation', 

262 'binds', 'defining', 'smt2_status', 'term_cartouche', 

263 'boogie_file', 'text_cartouche', 

264 ) 

265 

266 keyword_theory_script = ('inductive_cases', 'inductive_simps') 

267 

268 keyword_theory_goal = ( 

269 'ax_specification', 'bnf', 'code_pred', 'corollary', 'cpodef', 

270 'crunch', 'crunch_ignore', 

271 'enriched_type', 'function', 'instance', 'interpretation', 'lemma', 

272 'lift_definition', 'nominal_inductive', 'nominal_inductive2', 

273 'nominal_primrec', 'pcpodef', 'primcorecursive', 

274 'quotient_definition', 'quotient_type', 'recdef_tc', 'rep_datatype', 

275 'schematic_corollary', 'schematic_lemma', 'schematic_theorem', 

276 'spark_vc', 'specification', 'subclass', 'sublocale', 'termination', 

277 'theorem', 'typedef', 'wrap_free_constructors', 

278 ) 

279 

280 keyword_qed = ('by', 'done', 'qed') 

281 keyword_abandon_proof = ('sorry', 'oops') 

282 

283 keyword_proof_goal = ('have', 'hence', 'interpret') 

284 

285 keyword_proof_block = ('next', 'proof') 

286 

287 keyword_proof_chain = ( 

288 'finally', 'from', 'then', 'ultimately', 'with', 

289 ) 

290 

291 keyword_proof_decl = ( 

292 'ML_prf', 'also', 'include', 'including', 'let', 'moreover', 'note', 

293 'txt', 'txt_raw', 'unfolding', 'using', 'write', 

294 ) 

295 

296 keyword_proof_asm = ('assume', 'case', 'def', 'fix', 'presume') 

297 

298 keyword_proof_asm_goal = ('guess', 'obtain', 'show', 'thus') 

299 

300 keyword_proof_script = ( 

301 'apply', 'apply_end', 'apply_trace', 'back', 'defer', 'prefer', 

302 ) 

303 

304 operators = ( 

305 '::', ':', '(', ')', '[', ']', '_', '=', ',', '|', 

306 '+', '-', '!', '?', 

307 ) 

308 

309 proof_operators = ('{', '}', '.', '..') 

310 

311 tokens = { 

312 'root': [ 

313 (r'\s+', Whitespace), 

314 (r'\(\*', Comment, 'comment'), 

315 (r'\\<open>', String.Symbol, 'cartouche'), 

316 (r'\{\*|‹', String, 'cartouche'), 

317 

318 (words(operators), Operator), 

319 (words(proof_operators), Operator.Word), 

320 

321 (words(keyword_minor, prefix=r'\b', suffix=r'\b'), Keyword.Pseudo), 

322 

323 (words(keyword_diag, prefix=r'\b', suffix=r'\b'), Keyword.Type), 

324 

325 (words(keyword_thy, prefix=r'\b', suffix=r'\b'), Keyword), 

326 (words(keyword_theory_decl, prefix=r'\b', suffix=r'\b'), Keyword), 

327 

328 (words(keyword_section, prefix=r'\b', suffix=r'\b'), Generic.Heading), 

329 (words(keyword_subsection, prefix=r'\b', suffix=r'\b'), Generic.Subheading), 

330 

331 (words(keyword_theory_goal, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), 

332 (words(keyword_theory_script, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), 

333 

334 (words(keyword_abandon_proof, prefix=r'\b', suffix=r'\b'), Generic.Error), 

335 

336 (words(keyword_qed, prefix=r'\b', suffix=r'\b'), Keyword), 

337 (words(keyword_proof_goal, prefix=r'\b', suffix=r'\b'), Keyword), 

338 (words(keyword_proof_block, prefix=r'\b', suffix=r'\b'), Keyword), 

339 (words(keyword_proof_decl, prefix=r'\b', suffix=r'\b'), Keyword), 

340 

341 (words(keyword_proof_chain, prefix=r'\b', suffix=r'\b'), Keyword), 

342 (words(keyword_proof_asm, prefix=r'\b', suffix=r'\b'), Keyword), 

343 (words(keyword_proof_asm_goal, prefix=r'\b', suffix=r'\b'), Keyword), 

344 

345 (words(keyword_proof_script, prefix=r'\b', suffix=r'\b'), Keyword.Pseudo), 

346 

347 (r'\\<(\w|\^)*>', Text.Symbol), 

348 

349 (r"'[^\W\d][.\w']*", Name.Type), 

350 

351 (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex), 

352 (r'0[oO][0-7][0-7_]*', Number.Oct), 

353 (r'0[bB][01][01_]*', Number.Bin), 

354 

355 (r'"', String, 'string'), 

356 (r'`', String.Other, 'fact'), 

357 (r'[^\s:|\[\]\-()=,+!?{}._][^\s:|\[\]\-()=,+!?{}]*', Name), 

358 ], 

359 'comment': [ 

360 (r'[^(*)]+', Comment), 

361 (r'\(\*', Comment, '#push'), 

362 (r'\*\)', Comment, '#pop'), 

363 (r'[(*)]', Comment), 

364 ], 

365 'cartouche': [ 

366 (r'[^{*}\\‹›]+', String), 

367 (r'\\<open>', String.Symbol, '#push'), 

368 (r'\{\*|‹', String, '#push'), 

369 (r'\\<close>', String.Symbol, '#pop'), 

370 (r'\*\}|›', String, '#pop'), 

371 (r'\\<(\w|\^)*>', String.Symbol), 

372 (r'[{*}\\]', String), 

373 ], 

374 'string': [ 

375 (r'[^"\\]+', String), 

376 (r'\\<(\w|\^)*>', String.Symbol), 

377 (r'\\"', String), 

378 (r'\\', String), 

379 (r'"', String, '#pop'), 

380 ], 

381 'fact': [ 

382 (r'[^`\\]+', String.Other), 

383 (r'\\<(\w|\^)*>', String.Symbol), 

384 (r'\\`', String.Other), 

385 (r'\\', String.Other), 

386 (r'`', String.Other, '#pop'), 

387 ], 

388 } 

389 

390 

391class LeanLexer(RegexLexer): 

392 """ 

393 For the Lean theorem prover. 

394 

395 .. versionadded:: 2.0 

396 """ 

397 name = 'Lean' 

398 url = 'https://github.com/leanprover/lean' 

399 aliases = ['lean'] 

400 filenames = ['*.lean'] 

401 mimetypes = ['text/x-lean'] 

402 

403 tokens = { 

404 'expression': [ 

405 (r'\s+', Text), 

406 (r'/--', String.Doc, 'docstring'), 

407 (r'/-', Comment, 'comment'), 

408 (r'--.*?$', Comment.Single), 

409 (words(( 

410 'forall', 'fun', 'Pi', 'from', 'have', 'show', 'assume', 'suffices', 

411 'let', 'if', 'else', 'then', 'in', 'with', 'calc', 'match', 

412 'do' 

413 ), prefix=r'\b', suffix=r'\b'), Keyword), 

414 (words(('sorry', 'admit'), prefix=r'\b', suffix=r'\b'), Generic.Error), 

415 (words(('Sort', 'Prop', 'Type'), prefix=r'\b', suffix=r'\b'), Keyword.Type), 

416 (words(( 

417 '(', ')', ':', '{', '}', '[', ']', '⟨', '⟩', '‹', '›', '⦃', '⦄', ':=', ',', 

418 )), Operator), 

419 (r'[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]' 

420 r'[.A-Za-z_\'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079' 

421 r'\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*', Name), 

422 (r'0x[A-Za-z0-9]+', Number.Integer), 

423 (r'0b[01]+', Number.Integer), 

424 (r'\d+', Number.Integer), 

425 (r'"', String.Double, 'string'), 

426 (r"'(?:(\\[\\\"'nt])|(\\x[0-9a-fA-F]{2})|(\\u[0-9a-fA-F]{4})|.)'", String.Char), 

427 (r'[~?][a-z][\w\']*:', Name.Variable), 

428 (r'\S', Name.Builtin.Pseudo), 

429 ], 

430 'root': [ 

431 (words(( 

432 'import', 'renaming', 'hiding', 

433 'namespace', 

434 'local', 

435 'private', 'protected', 'section', 

436 'include', 'omit', 'section', 

437 'protected', 'export', 

438 'open', 

439 'attribute', 

440 ), prefix=r'\b', suffix=r'\b'), Keyword.Namespace), 

441 (words(( 

442 'lemma', 'theorem', 'def', 'definition', 'example', 

443 'axiom', 'axioms', 'constant', 'constants', 

444 'universe', 'universes', 

445 'inductive', 'coinductive', 'structure', 'extends', 

446 'class', 'instance', 

447 'abbreviation', 

448 

449 'noncomputable theory', 

450 

451 'noncomputable', 'mutual', 'meta', 

452 

453 'attribute', 

454 

455 'parameter', 'parameters', 

456 'variable', 'variables', 

457 

458 'reserve', 'precedence', 

459 'postfix', 'prefix', 'notation', 'infix', 'infixl', 'infixr', 

460 

461 'begin', 'by', 'end', 

462 

463 'set_option', 

464 'run_cmd', 

465 ), prefix=r'\b', suffix=r'\b'), Keyword.Declaration), 

466 (r'@\[', Keyword.Declaration, 'attribute'), 

467 (words(( 

468 '#eval', '#check', '#reduce', '#exit', 

469 '#print', '#help', 

470 ), suffix=r'\b'), Keyword), 

471 include('expression') 

472 ], 

473 'attribute': [ 

474 (r'\]', Keyword.Declaration, '#pop'), 

475 include('expression'), 

476 ], 

477 'comment': [ 

478 (r'[^/-]', Comment.Multiline), 

479 (r'/-', Comment.Multiline, '#push'), 

480 (r'-/', Comment.Multiline, '#pop'), 

481 (r'[/-]', Comment.Multiline) 

482 ], 

483 'docstring': [ 

484 (r'[^/-]', String.Doc), 

485 (r'-/', String.Doc, '#pop'), 

486 (r'[/-]', String.Doc) 

487 ], 

488 'string': [ 

489 (r'[^\\"]+', String.Double), 

490 (r"(?:(\\[\\\"'nt])|(\\x[0-9a-fA-F]{2})|(\\u[0-9a-fA-F]{4}))", String.Escape), 

491 ('"', String.Double, '#pop'), 

492 ], 

493 }