Leonardo de Moura
63eafaae9a
feat(emacs): add syntax-highlight for clear and revert tactics
2014-11-26 14:33:28 -08:00
Leonardo de Moura
ea63136434
fix(src/emacs/lean-flycheck): do not report 'sorry' warnings to flycheck, this is a temporary workaround since there is an overlap between flycheck and lean-mode type info
2014-11-26 09:35:22 -08:00
Leonardo de Moura
a005c8f4d0
feat(frontends/lean): display eval/check/find_decl results using flycheck
2014-11-24 08:35:49 -08:00
Soonho Kong
fe638f0ee7
fix(emacs/lean-flycheck): fix bug in advice for lean-flycheck-try-parse-error-with-pattern
...
I provided an "advice" for 'flycheck-try-parse-error-with-pattern'
function to change its behavior, namely to increase error-columns by
one.
Bug
===
The problem is that it doesn't consider the case where the pattern is
not matched and ends up with "err = nil". For this case,
"(flycheck-error-column err)" generates an exception if executed. The
whole error parsing process stops immediately.
This causes a problem when we have more than one error-patterns, which
is the case when we enable 'error' and 'warning' patterns.
Fix
===
Fix is simple: check err before executing (flycheck-error-column err)
- (col (flycheck-error-column err)))
+ (col (and err (flycheck-error-column err))))
2014-11-24 05:06:51 -05:00
Leonardo de Moura
f1e915a188
feat(frontends/lean): add 'find_decl' command
2014-11-23 23:00:59 -08:00
Leonardo de Moura
13fba433b0
feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327
2014-11-23 17:30:22 -08:00
Leonardo de Moura
47b6cfb28d
feat(library/logic/if): add dependent if-then-else: dite
2014-11-22 09:56:32 -08:00
Leonardo de Moura
28c63e685b
feat(frontends/lean): add '[local]' notation, closes #322
2014-11-16 21:15:04 -08:00
Leonardo de Moura
50973bb4f3
feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations
...
To retrieve the previous behavior, we should use [strict] modifier
2014-11-10 12:46:04 -08:00
Leonardo de Moura
bd5f3ec572
feat(emacs/lean-syntax): highlight [decls] modifier
2014-11-10 10:35:42 -08:00
Soonho Kong
d25e74b921
fix(emacs/lean-mode): remove whitespace-cleanup-mode dependency
...
- When customization variable 'lean-delete-trailing-whitespace' is
non-nil, trailing-whitespaces are removed before save.
- It doesn't change TABs.
Close #226
2014-11-09 00:21:43 -05:00
Soonho Kong
36476b9115
fix(lean-util): handle case where incomplete hierarchical name ends with "."
...
Close #311
2014-11-08 23:46:59 -05:00
Leonardo de Moura
c7992f2cac
feat(frontends/lean): add [whnf] modifier to eval command
2014-11-08 10:19:29 -08:00
Soonho Kong
d861c78072
fix(emacs/lean-syntax): change comment symbols to be considered as punctuations
...
Please read the documentation of "modify-syntax-entry":
"The first character of NEWENTRY should be one of the following:
_ symbol constituent
. punctuation
"
Close : #306
2014-11-07 17:48:21 -05:00
Soonho Kong
18a41eb962
feat(emacs/lean-mode): bind "C-c C-k" to quail-show-key
...
- Use this to see how to type a unicode character
2014-11-07 17:28:21 -05:00
Leonardo de Moura
85d0521d48
feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305
2014-11-06 21:34:05 -08:00
Leonardo de Moura
ed83b7ff2a
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.
2014-11-06 20:59:31 -08:00
Leonardo de Moura
4650791108
feat(frontends/lean): add 'print fields' command
2014-11-05 14:06:54 -08:00
Leonardo de Moura
defc2478b5
feat(frontends/lean): add 'record' as an alias for 'structure' command
2014-11-05 12:02:52 -08:00
Soonho Kong
e71db7109d
fix(emacs/lean-mode.el): remove quotation marks in lean-execute
...
Close #294
2014-11-05 09:20:14 -05:00
Leonardo de Moura
c6c090eda6
feat(src/emacs/lean-mode): add shortcut for restarting lean server
2014-11-04 18:01:20 -08:00
Soonho Kong
2273f75e9b
fix(emacs/lean-mode): handle when there is spaces in filenames
2014-11-04 19:22:35 -05:00
Leonardo de Moura
101e9966fd
fix(emacs/lean-syntax): bug in syntax highlight, examples do not have names
2014-11-03 18:32:18 -08:00
Leonardo de Moura
1e6f7cdbb4
chore(frontends/lean/decl_cmds): add 'example' command
...
It is like a theorem, but it is discarded after checking
2014-11-01 11:37:39 -07:00
Soonho Kong
cae543e665
chore(emacs): remove unnecessary requires
2014-10-31 16:01:10 -07:00
Soonho Kong
96f620adf6
doc(README.md): add Aquamacs case, ask to update lean-rootdir
...
[skip ci]
2014-10-31 09:58:15 -07:00
Leonardo de Moura
591e566472
feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator
...
This is part of #268
2014-10-30 23:24:09 -07:00
Soonho Kong
b7d805a145
feat(emacs/lean-settings): add 'lean-follow-changes' option
2014-10-29 23:58:50 -07:00
Leonardo de Moura
9547e2d077
feat(library/tactic): add rotate_left/rotate_right tactics, closes #278
2014-10-29 19:13:55 -07:00
Soonho Kong
5ad312f6ce
test(emacs/lean-info-test): add test cases for goal visualization
...
[skip ci]
2014-10-29 17:09:08 -07:00
Soonho Kong
6973d3e7aa
feat(emacs/lean-info): add goal visualization options 'lean-proofstate-display-style'
...
lean-proofstate-display-style:
- 'show-all: Show all goals
a : Prop,
b : Prop,
c : Prop,
H_1 : a,
H_2 : b,
H_3 : c
⊢ id a
a : Prop,
b : Prop,
c : Prop,
H_1 : a,
H_2 : b,
H_3 : c
⊢ b ∧ c
- 'show-first: Show only the first
a : Prop,
b : Prop,
c : Prop,
H_1 : a,
H_2 : b,
H_3 : c
⊢ id a
- 'show-first-and-other-conclusions: Show the first goal, and the
conclusions of all other goals (DEFAULT OPTION)
a : Prop,
b : Prop,
c : Prop,
H_1 : a,
H_2 : b,
H_3 : c
⊢ id a
⊢ b ∧ c
Close #279
2014-10-29 17:08:55 -07:00
Leonardo de Moura
b0a7888346
fix(emacs/lean-flycheck): should accept error messages with empty lines
2014-10-29 16:51:06 -07:00
Soonho Kong
854e7ba1be
fix(emacs/lean-type): improve displaying proof state messages
...
- Do not repeat the same message
- Do not display the empty message
- Do not display "[stale]" for proof states
2014-10-29 16:02:48 -07:00
Soonho Kong
99f85c8dbc
fix(emacs/lean-info): proofstate display problem
2014-10-29 14:33:05 -07:00
Soonho Kong
fe710ac6d0
test(emacs/lean-info-test): add test for proofstate info
2014-10-29 14:33:05 -07:00
Soonho Kong
17455d191b
feat(emacs/lean-mode): add lean-info-mode for "*lean-info*" buffer
2014-10-29 14:33:05 -07:00
Soonho Kong
12824c3e27
fix(emacs/lean-syntax): fix Type1, Type2 highlight
2014-10-29 14:33:05 -07:00
Soonho Kong
b0e249ce63
feat(emacs/lean-type): output INFO to *lean-info* buffer in addition to minibuffer
...
Close #260
2014-10-29 14:33:05 -07:00
Soonho Kong
0d8658d762
feat(emacs/lean-settings): add lean-show-proofstate-in-minibuffer option
2014-10-29 14:33:05 -07:00
Soonho Kong
53f79ec9c2
feat(emacs): extract proof state information attached to ","
2014-10-29 14:33:05 -07:00
Soonho Kong
fdf5f3ff8a
feat(emacs/lean-info): add PROOF_STATE info
...
Close #259
2014-10-29 14:33:05 -07:00
Soonho Kong
cb83eca2f3
feat(emacs/lean-input): add lean-input-export-translations
2014-10-29 14:33:05 -07:00
Leonardo de Moura
e22eb3543c
feat(library/tactic): add whnf tactic, closes #270
2014-10-28 23:18:49 -07:00
Leonardo de Moura
08e8161243
feat(emacs/lean-syntax): add 'eassumption' highlight
2014-10-26 15:45:26 -07:00
Leonardo de Moura
50948be66b
fix(emacs/lean-syntax): syntax highlight for composite names in declarations
2014-10-26 09:27:17 -07:00
Leonardo de Moura
79d0347721
feat(library/tactic): add generalize tactic, closes #34
...
Remark: the intros tactic has been added in a different commit: 7d0100a340
2014-10-23 22:40:15 -07:00
Soonho Kong
04b4e36701
doc(emacs/README.md): fix typo
...
[skip ci]
2014-10-23 14:32:36 -07:00
Leonardo de Moura
c50227ea6e
feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included
...
This commit also adds the tactic rapply that corresponds to the previous
semantics we have been using.
2014-10-22 18:11:09 -07:00
Leonardo de Moura
e95c7c5f70
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-22 17:29:50 -07:00
Leonardo de Moura
bb953b80aa
feat(frontends/lean): reserve notation, closes #95
2014-10-21 15:39:47 -07:00