Class: Rouge::Lexers::Coq
Constant Summary
Constants inherited
from RegexLexer
RegexLexer::MAX_NULL_SCANS
Token::Tokens::Num, Token::Tokens::Str
Instance Attribute Summary
Attributes inherited from Rouge::Lexer
#options
Class Method Summary
collapse
Methods inherited from RegexLexer
append, #delegate, get_state, #get_state, #goto, #group, #groups, #in_state?, #pop!, prepend, #push, #recurse, replace_state, #reset!, #reset_stack, #stack, start, start_procs, #state, state, #state?, state_definitions, states, #step, #stream_tokens, #token
aliases, all, #as_bool, #as_lexer, #as_list, #as_string, #as_token, assert_utf8!, #bool_option, #continue_lex, continue_lex, debug_enabled?, demo, demo_file, desc, detect?, detectable?, disable_debug!, enable_debug!, filenames, find, find_fancy, guess, guess_by_filename, guess_by_mimetype, guess_by_source, guesses, #hash_option, #initialize, lex, #lex, #lexer_option, #list_option, lookup_fancy, mimetypes, option, option_docs, #reset!, #stream_tokens, #string_option, tag, #tag, title, #token_option, #with
token
Constructor Details
This class inherits a constructor from Rouge::Lexer
Class Method Details
.classify(x) ⇒ Object
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
# File 'lib/rouge/lexers/coq.rb', line 59
def self.classify(x)
if self.coq.include? x
return Keyword
elsif self.gallina.include? x
return Keyword::Reserved
elsif self.ltac.include? x
return Keyword::Pseudo
elsif self.terminators.include? x
return Name::Exception
elsif self.tacticals.include? x
return Keyword::Pseudo
else
return Name::Constant
end
end
|
.coq ⇒ Object
19
20
21
22
23
24
25
26
27
28
29
30
|
# File 'lib/rouge/lexers/coq.rb', line 19
def self.coq
@coq ||= Set.new %w(
Definition Theorem Lemma Remark Example Fixpoint CoFixpoint
Record Inductive CoInductive Corollary Goal Proof
Ltac Require Import Export Module Section End Variable
Context Polymorphic Monomorphic Universe Universes
Variables Class Instance Global Local Include
Printing Notation Infix Arguments Hint Rewrite Immediate
Qed Defined Opaque Transparent Existing
Compute Eval Print SearchAbout Search About Check Admitted
)
end
|
.gallina ⇒ Object
12
13
14
15
16
17
|
# File 'lib/rouge/lexers/coq.rb', line 12
def self.gallina
@gallina ||= Set.new %w(
as fun if in let match then else return end Type Set Prop
forall
)
end
|
.ltac ⇒ Object
32
33
34
35
36
37
38
39
40
41
42
43
44
|
# File 'lib/rouge/lexers/coq.rb', line 32
def self.ltac
@ltac ||= Set.new %w(
apply eapply auto eauto rewrite setoid_rewrite
with in as at destruct split inversion injection
intro intros unfold fold cbv cbn lazy subst
clear symmetry transitivity etransitivity erewrite
edestruct constructor econstructor eexists exists
f_equal refine instantiate revert simpl
specialize generalize dependent red induction
beta iota zeta delta exfalso autorewrite setoid_rewrite
compute vm_compute native_compute
)
end
|
.tacticals ⇒ Object
46
47
48
49
50
|
# File 'lib/rouge/lexers/coq.rb', line 46
def self.tacticals
@tacticals ||= Set.new %w(
repeat first try
)
end
|
.terminators ⇒ Object
52
53
54
55
56
57
|
# File 'lib/rouge/lexers/coq.rb', line 52
def self.terminators
@terminators ||= Set.new %w(
omega solve congruence reflexivity exact
assumption eassumption
)
end
|