max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(shell/server): fix field completion

Browse source
This commit is contained in:
Gabriel Ebner 2017-03-20 09:00:33 +01:00
parent 5e29fe227e
commit 9dfd8e1018
3 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/interactive.cpp
View file

@ -14,7 +14,6 @@ Author: Sebastian Ullrich
#include "frontends/lean/interactive.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/tactic_notation.h"
#include "info_manager.h"
namespace lean {
LEAN_THREAD_VALUE(break_at_pos_exception::token_context, g_context, break_at_pos_exception::token_context::none);

2
src/shell/server.cpp
View file

@ -495,7 +495,7 @@ json server::autocomplete(std::shared_ptr<module_info const> const & mod_info, b
try {
parse_breaking_at_pos(mod_info->m_mod, mod_info, pos, true);
} catch (break_at_pos_exception & e) {
report_completions(snap->m_env, snap->m_options, pos, skip_completions, mod_info->m_mod.c_str(),
report_completions(snap->m_env, snap->m_options, pos0, skip_completions, mod_info->m_mod.c_str(),
e, j);
} catch (throwable & ex) {}
}

2
tests/lean/interactive/complete_field.lean.expected.out
View file

@ -6,4 +6,4 @@
{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5}
{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9}
{"completions":[{"source":,"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":145},"text":"right","type":"?a ∧ ?b → ?b"}],"prefix":"r","response":"ok","seq_num":13}
{"completions":[{"source":,"text":"assoc","type":"(?a ∧ ?b) ∧ ?c ↔ ?a ∧ ?b ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"cases_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":14,"file":"/library/init/logic.lean","line":393},"text":"comm","type":"?a ∧ ?b ↔ ?b ∧ ?a"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"dcases_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":11,"file":"/library/init/logic.lean","line":653},"text":"decidable","type":"decidable (?p ∧ ?q)"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"drec","type":"(Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → Π (n : ?a ∧ ?b), ?C n"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"drec_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":6,"file":"/library/init/logic.lean","line":201},"text":"elim","type":"?a ∧ ?b → (?a → ?b → ?c) → ?c"},{"source":{"column":4,"file":"/library/init/core.lean","line":137},"text":"elim_left","type":"?a ∧ ?b → ?a"},{"source":{"column":4,"file":"/library/init/core.lean","line":142},"text":"elim_right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":380},"text":"imp","type":"(?a → ?c) → (?b → ?d) → ?a ∧ ?b → ?c ∧ ?d"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"induction_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"intro","type":"?a → ?b → ?a ∧ ?b"},{"source":{"column":4,"file":"/library/init/core.lean","line":140},"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":145},"text":"right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":204},"text":"swap","type":"?a ∧ ?b → ?b ∧ ?a"},{"source":{"column":4,"file":"/library/init/logic.lean","line":207},"text":"symm","type":"?a ∧ ?b → ?b ∧ ?a"}],"prefix":"","response":"ok","seq_num":17}
{"completions":[{"source":,"text":"assoc","type":"(?a ∧ ?b) ∧ ?c ↔ ?a ∧ ?b ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"cases_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":14,"file":"/library/init/logic.lean","line":393},"text":"comm","type":"?a ∧ ?b ↔ ?b ∧ ?a"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"dcases_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":11,"file":"/library/init/logic.lean","line":653},"text":"decidable","type":"decidable (?p ∧ ?q)"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"drec","type":"(Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → Π (n : ?a ∧ ?b), ?C n"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"drec_on","type":"Π (n : ?a ∧ ?b), (Π (a : ?a) (a_1 : ?b), ?C (and.intro a a_1)) → ?C n"},{"source":{"column":6,"file":"/library/init/logic.lean","line":201},"text":"elim","type":"?a ∧ ?b → (?a → ?b → ?c) → ?c"},{"source":{"column":4,"file":"/library/init/core.lean","line":137},"text":"elim_left","type":"?a ∧ ?b → ?a"},{"source":{"column":4,"file":"/library/init/core.lean","line":142},"text":"elim_right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":380},"text":"imp","type":"(?a → ?c) → (?b → ?d) → ?a ∧ ?b → ?c ∧ ?d"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"intro","type":"?a → ?b → ?a ∧ ?b"},{"source":{"column":4,"file":"/library/init/core.lean","line":140},"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"rec","type":"(?a → ?b → ?C) → ?a ∧ ?b → ?C"},{"source":{"column":10,"file":"/library/init/core.lean","line":134},"text":"rec_on","type":"?a ∧ ?b → (?a → ?b → ?C) → ?C"},{"source":{"column":4,"file":"/library/init/core.lean","line":145},"text":"right","type":"?a ∧ ?b → ?b"},{"source":{"column":6,"file":"/library/init/logic.lean","line":204},"text":"swap","type":"?a ∧ ?b → ?b ∧ ?a"},{"source":{"column":4,"file":"/library/init/logic.lean","line":207},"text":"symm","type":"?a ∧ ?b → ?b ∧ ?a"}],"prefix":"","response":"ok","seq_num":17}