class Rouge::Lexers::Coq

Public Class Methods

analyze_text(text) click to toggle source
# File lib/rouge/lexers/coq.rb, line 10
def self.analyze_text(text)
  return 0.3 if text.include? "Require"
end
classify(x) click to toggle source
# File lib/rouge/lexers/coq.rb, line 71
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() click to toggle source
# File lib/rouge/lexers/coq.rb, line 21
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
  )
end
end_sentence() click to toggle source
# File lib/rouge/lexers/coq.rb, line 67
def self.end_sentence
  @end_sentence ||= Punctuation::Indicator
end
gallina() click to toggle source
# File lib/rouge/lexers/coq.rb, line 14
def self.gallina
  @gallina ||= Set.new %w(
    as fun if in let match then else return end Type Set Prop
    forall
  )
end
keyopts() click to toggle source
# File lib/rouge/lexers/coq.rb, line 61
def self.keyopts
  @keyopts ||= Set.new %w(
    := => -> /\\ \\/ _ ; :> :
  )
end
ltac() click to toggle source
# File lib/rouge/lexers/coq.rb, line 34
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() click to toggle source
# File lib/rouge/lexers/coq.rb, line 48
def self.tacticals
  @tacticals ||= Set.new %w(
    repeat first try
  )
end
terminators() click to toggle source
# File lib/rouge/lexers/coq.rb, line 54
def self.terminators
  @terminators ||= Set.new %w(
    omega solve congruence reflexivity exact
    assumption eassumption
  )
end