Class: Rouge::Lexers::Isabelle

Inherits:
RegexLexer show all
Defined in:
lib/rouge/lexers/isabelle.rb

Constant Summary

Constants inherited from RegexLexer

RegexLexer::MAX_NULL_SCANS

Constants included from Token::Tokens

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

Methods inherited from Rouge::Lexer

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

Methods included from Token::Tokens

token

Constructor Details

This class inherits a constructor from Rouge::Lexer

Class Method Details

.keyword_abandon_proof ⇒ Object 



127
128
129
 
# File 'lib/rouge/lexers/isabelle.rb', line 127

def self.keyword_abandon_proof
  @keyword_abandon_proof ||= Set.new %w(sorry oops)
end

.keyword_diag ⇒ Object 



29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
 
# File 'lib/rouge/lexers/isabelle.rb', line 29

def self.keyword_diag
  @keyword_diag ||= Set.new %w(
    ML_command ML_val class_deps code_deps code_thms
    display_drafts find_consts find_theorems find_unused_assms
    full_prf help locale_deps nitpick pr prf
    print_abbrevs print_antiquotations print_attributes
    print_binds print_bnfs print_bundles
    print_case_translations print_cases print_claset
    print_classes print_codeproc print_codesetup
    print_coercions print_commands print_context
    print_defn_rules print_dependencies print_facts
    print_induct_rules print_inductives print_interps
    print_locale print_locales print_methods print_options
    print_orders print_quot_maps print_quotconsts
    print_quotients print_quotientsQ3 print_quotmapsQ3
    print_rules print_simpset print_state print_statement
    print_syntax print_theorems print_theory print_trans_rules
    prop pwd quickcheck refute sledgehammer smt_status
    solve_direct spark_status term thm thm_deps thy_deps
    try try0 typ unused_thms value values welcome
    print_ML_antiquotations print_term_bindings values_prolog
  )
end

.keyword_minor ⇒ Object 



15
16
17
18
19
20
21
22
23
24
25
26
27
 
# File 'lib/rouge/lexers/isabelle.rb', line 15

def self.keyword_minor
  @keyword_minor ||= Set.new %w(
    and assumes attach avoids binder checking
    class_instance class_relation code_module congs
    constant constrains datatypes defines file fixes
    for functions hints identifier if imports in
    includes infix infixl infixr is keywords lazy
    module_name monos morphisms no_discs_sels notes
    obtains open output overloaded parametric permissive
    pervasive rep_compat shows structure type_class
    type_constructor unchecked unsafe where
  )
end

.keyword_proof_asm ⇒ Object 



150
151
152
 
# File 'lib/rouge/lexers/isabelle.rb', line 150

def self.keyword_proof_asm
  @keyword_proof_asm ||= Set.new %w(assume case def fix presume)
end

.keyword_proof_asm_goal ⇒ Object 



154
155
156
 
# File 'lib/rouge/lexers/isabelle.rb', line 154

def self.keyword_proof_asm_goal
  @keyword_proof_asm_goal ||= Set.new %w(guess obtain show thus)
end

.keyword_proof_block ⇒ Object 



135
136
137
 
# File 'lib/rouge/lexers/isabelle.rb', line 135

def self.keyword_proof_block
  @keyword_proof_block ||= Set.new %w(next proof)
end

.keyword_proof_chain ⇒ Object 



139
140
141
 
# File 'lib/rouge/lexers/isabelle.rb', line 139

def self.keyword_proof_chain
  @keyword_proof_chain ||= Set.new %w(finally from then ultimately with)
end

.keyword_proof_decl ⇒ Object 



143
144
145
146
147
148
 
# File 'lib/rouge/lexers/isabelle.rb', line 143

def self.keyword_proof_decl
  @keyword_proof_decl ||= Set.new %w(
    ML_prf also include including let moreover note
    txt txt_raw unfolding using write
  )
end

.keyword_proof_goal ⇒ Object 



131
132
133
 
# File 'lib/rouge/lexers/isabelle.rb', line 131

def self.keyword_proof_goal
  @keyword_proof_goal ||= Set.new %w(have hence interpret)
end

.keyword_proof_script ⇒ Object 



158
159
160
 
# File 'lib/rouge/lexers/isabelle.rb', line 158

def self.keyword_proof_script
  @keyword_proof_script ||= Set.new %w(apply apply_end apply_trace back defer prefer)
end

.keyword_qed ⇒ Object 



123
124
125
 
# File 'lib/rouge/lexers/isabelle.rb', line 123

def self.keyword_qed
  @keyword_qed ||= Set.new %w(by done qed)
end

.keyword_section ⇒ Object 



57
58
59
 
# File 'lib/rouge/lexers/isabelle.rb', line 57

def self.keyword_section
  @keyword_section ||= Set.new %w(header chapter)
end

.keyword_subsection ⇒ Object 



61
62
63
 
# File 'lib/rouge/lexers/isabelle.rb', line 61

def self.keyword_subsection
  @keyword_subsection ||= Set.new %w(section subsection subsubsection sect subsect subsubsect)
end

.keyword_theory_decl ⇒ Object 



65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
 
# File 'lib/rouge/lexers/isabelle.rb', line 65

def self.keyword_theory_decl
  @keyword_theory_decl ||= Set.new %w(
    ML ML_file abbreviation adhoc_overloading arities
    atom_decl attribute_setup axiomatization bundle
    case_of_simps class classes classrel codatatype
    code_abort code_class code_const code_datatype
    code_identifier code_include code_instance code_modulename
    code_monad code_printing code_reflect code_reserved
    code_type coinductive coinductive_set consts context
    datatype datatype_new datatype_new_compat declaration
    declare default_sort defer_recdef definition defs
    domain domain_isomorphism domaindef equivariance
    export_code extract extract_type fixrec fun
    fun_cases hide_class hide_const hide_fact hide_type
    import_const_map import_file import_tptp import_type_map
    inductive inductive_set instantiation judgment lemmas
    lifting_forget lifting_update local_setup locale
    method_setup nitpick_params no_adhoc_overloading
    no_notation no_syntax no_translations no_type_notation
    nominal_datatype nonterminal notation notepad oracle
    overloading parse_ast_translation parse_translation
    partial_function primcorec primrec primrec_new
    print_ast_translation print_translation quickcheck_generator
    quickcheck_params realizability realizers recdef record
    refute_params setup setup_lifting simproc_setup
    simps_of_case sledgehammer_params spark_end spark_open
    spark_open_siv spark_open_vcg spark_proof_functions
    spark_types statespace syntax syntax_declaration text
    text_raw theorems translations type_notation
    type_synonym typed_print_translation typedecl hoarestate
    install_C_file install_C_types wpc_setup c_defs c_types
    memsafe SML_export SML_file SML_import approximate
    bnf_axiomatization cartouche datatype_compat
    free_constructors functor nominal_function
    nominal_termination permanent_interpretation
    binds defining smt2_status term_cartouche
    boogie_file text_cartouche
  )
end

.keyword_theory_goal ⇒ Object 



109
110
111
112
113
114
115
116
117
118
119
120
121
 
# File 'lib/rouge/lexers/isabelle.rb', line 109

def self.keyword_theory_goal
  @keyword_theory_goal ||= Set.new %w(
    ax_specification bnf code_pred corollary cpodef
    crunch crunch_ignore
    enriched_type function instance interpretation lemma
    lift_definition nominal_inductive nominal_inductive2
    nominal_primrec pcpodef primcorecursive
    quotient_definition quotient_type recdef_tc rep_datatype
    schematic_corollary schematic_lemma schematic_theorem
    spark_vc specification subclass sublocale termination
    theorem typedef wrap_free_constructors
  )
end

.keyword_theory_script ⇒ Object 



105
106
107
 
# File 'lib/rouge/lexers/isabelle.rb', line 105

def self.keyword_theory_script
  @keyword_theory_script ||= Set.new %w(inductive_cases inductive_simps)
end

.keyword_thy ⇒ Object 



53
54
55
 
# File 'lib/rouge/lexers/isabelle.rb', line 53

def self.keyword_thy
  @keyword_thy ||= Set.new %w(theory begin end)
end