From ed83b7ff2afd46b302d1d80a6429f35928258fa3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Nov 2014 20:57:10 -0800 Subject: [PATCH] fix(emacs/lean-syntax): syntax highlight, issue #306 1- FIXED structure foo := (bar : Type) -- the name of structures is not highlighted 2- NOT FIXED check foo-- this comment is not highlighted 3- FIXED check Type.{5} -- Type is not highlighted 4- FIXED definition bar{thisishighlighted : Type} := foo 5- FIXED definition bar2 {thetypeofthisvariableisnothighlighted :Type} := foo Have no idea what is going on with 2. I'm not sure if this is our bug, or Emacs code we depend on. --- src/emacs/lean-syntax.el | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 4112f86d0..830494b44 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -101,14 +101,15 @@ ;; String ("\"[^\"]*\"" . 'font-lock-string-face) ;; Constants - (,(rx (or "#" "@" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨" "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/")) . 'font-lock-constant-face) - (,(rx (or "λ" "→" "∃" "∀" ":=")) . 'font-lock-constant-face ) + (,(rx symbol-start (or "#" "@" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨" "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/") symbol-end) + . 'font-lock-constant-face) + (,(rx symbol-start (or "λ" "→" "∃" "∀" ":=") symbol-end) . 'font-lock-constant-face ) ;; universe/inductive/theorem... "names" (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "lemma" "hypothesis" "definition" "constant")) word-end (zero-or-more (or whitespace "(" "{" "[")) - (group (zero-or-more (not (any " \t\n\r"))))) + (group (zero-or-more (not (any " \t\n\r{(["))))) (2 'font-lock-function-name-face)) ("\\(set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face)) ;; place holder @@ -124,7 +125,8 @@ word-end) . 'font-lock-constant-face) ;; Types - (,(rx symbol-start (or "Prop" "Type" "Type'" "Type₊" "Type₁" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face) + (,(rx word-start (or "Prop" "Type" "Type'" "Type₊" "Type₁" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face) + (,(rx word-start (group "Type") ".") (1 'font-lock-type-face)) ;; sorry (,(rx word-start "sorry" word-end) . 'font-lock-warning-face) ;; extra-keywords