Commit graph

5 commits

Author SHA1 Message Date
Leonardo de Moura
f98ab2a8ff fix(src/emacs/lean-syntax.el): remove obsolete command set_opaque
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 11:16:29 -07:00
Leonardo de Moura
b3615d5c8b fix(src/emacs): add 'begin' reserved keyword
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 09:33:09 -07:00
Soonho Kong
495809d86d feat(emacs/lean-syntax): support multi-line comments /- ... -/ 2014-08-26 16:22:30 -07:00
Soonho Kong
51b86b219b feat(emacs/lean): add multi-line comments
This is related with issue #63.

There are two known issues:

 - Emacs behaves as if the multi-line comment start/end symols are "(-"
   and "-)" instead of "(--" and "--)". As a result, it shows all the
   correct lean comments as it is. However, it will show some examples
   such as "(-5)" as a part of comment even if Lean doesn't interpret it
   as it is. Technically, it's because we are using a syntax-table based
   method to define comments. For more information read a documentation
   of 'modify-syntax-entry' function.

 - Somehow, the matching parens are broken. When we type "--)" to close
   a multi-line comment. Emacs warns "Mismatched Parentheses".
2014-08-19 15:03:51 -07:00
Soonho Kong
46013b6ad2 feat(emacs): define lean-mode as a derived-mode of prog-mode
Fix #52
2014-08-18 13:32:58 -07:00