File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed
Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change 1717 "infix|infixl|infixr|instance|let|macro|module|mutual|no-eta-equality|" +
1818 "open|overlap|pattern|postulate|primitive|private|public|quote|" +
1919 "quoteContext|quoteGoal|quoteTerm|record|renaming|rewrite|" +
20- "syntax|tactic|unquote|unquoteDecl|unquoteDef|using|where|with|" +
20+ "syntax|tactic|to| unquote|unquoteDecl|unquoteDef|using|variable |where|with|" +
2121 'Set(?:\\d+|[₀₁₂₃₄₅₆₇₈₉]+)?)(?=[.;{}()@"\\s]|$)' ,
2222 "u"
2323 ) ;
Original file line number Diff line number Diff line change @@ -10,7 +10,7 @@ const keywordsRegex = new RegExp(
1010 "infix|infixl|infixr|instance|let|macro|module|mutual|no-eta-equality|" +
1111 "open|overlap|pattern|postulate|primitive|private|public|quote|" +
1212 "quoteContext|quoteGoal|quoteTerm|record|renaming|rewrite|" +
13- "syntax|tactic|unquote|unquoteDecl|unquoteDef|using|where|with|" +
13+ "syntax|tactic|to| unquote|unquoteDecl|unquoteDef|using|variable |where|with|" +
1414 'Set(?:\\d+|[₀₁₂₃₄₅₆₇₈₉]+)?)(?=[.;{}()@"\\s]|$)' ,
1515 "u"
1616) ;
You can’t perform that action at this time.
0 commit comments