Skip to content

Commit

Permalink
more correct coq ident parser
Browse files Browse the repository at this point in the history
  • Loading branch information
cormacrelf committed Nov 14, 2021
1 parent 8ff1370 commit d3db448
Showing 1 changed file with 6 additions and 2 deletions.
8 changes: 6 additions & 2 deletions lib/rouge/lexers/coq.rb
Original file line number Diff line number Diff line change
Expand Up @@ -76,8 +76,12 @@ def self.classify(x)
end
end

id_trail = /(?:\p{L}|\p{N}|_|')/
id = /(?:\p{Ll}#{id_trail}*)|(?:(?:_|\p{Ll})#{id_trail}+)/i
# https://github.com/coq/coq/blob/110921a449fcb830ec2a1cd07e3acc32319feae6/clib/unicode.ml#L67
# https://coq.inria.fr/refman/language/core/basic.html#grammar-token-ident
id_first = /\p{L}/
id_first_underscore = /(?:\p{L}|_)/
id_subsequent = /(?:\p{L}|\p{N}|_|')/ # a few missing? some mathematical ' primes and subscripts
id = /(?:#{id_first}#{id_subsequent}*)|(?:#{id_first_underscore}#{id_subsequent}+)/i
dot_id = /\.(#{id})/i
dot_space = /\.(\s+)/
module_type = /Module(\s+)Type(\s+)/
Expand Down

0 comments on commit d3db448

Please sign in to comment.