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

feat(frontends/lean/interactive,emacs): hide colon separator in front of pretty-printed types

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-16 11:26:41 +01:00 • committed by Leonardo de Moura
parent c46936d180
commit 9b5e7ddcda
6 changed files with 21 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/emacs/lean-company.el
View file

@ -23,13 +23,14 @@
(setq-local company-begin-commands '(self-insert-command)) ; start autocompletion only after typing
(company-mode t))
(cl-defun company-lean--make-candidate (prefix &key text type doc source &allow-other-keys)
(cl-defun company-lean--make-candidate (prefix &key text type pretty doc source &allow-other-keys)
(destructuring-bind (&key file line column) source
(let ((source (cond
(file (cons file line))
(line (cons (current-buffer) (lean-pos-at-line-col line 0))))))
(propertize text
'type type
'pretty pretty
'doc doc
'source source
'prefix prefix))))
@ -64,9 +65,10 @@
(list :prefix prefix :candidates candidates))))
(defun company-lean--annotation (candidate)
(let ((type (get-text-property 0 'type candidate)))
(let ((type (get-text-property 0 'type candidate))
(pretty (get-text-property 0 'pretty candidate)))
(when type
(let* ((annotation-str (format " : %s" type))
(let* ((annotation-str (format (if pretty " %s" " : %s") type))
(annotation-len (length annotation-str))
(candidate-len (length candidate))
(entry-width (+ candidate-len

4
src/emacs/lean-type.el
View file

@ -40,7 +40,7 @@
(cl-defun lean-info-record-to-string (info-record)
"Given typeinfo, overload, and sym-name, compose information as a string."
(destructuring-bind (&key type doc overloads synth coercion proofstate full-id symbol extra &allow-other-keys) info-record
(destructuring-bind (&key type pretty doc overloads synth coercion proofstate full-id symbol extra &allow-other-keys) info-record
(let (name-str type-str coercion-str extra-str proofstate-str overload-str stale-str str)
(setq name-str
(cond
@ -66,7 +66,7 @@
(propertize expr 'face 'font-lock-variable-name-face)
type))))))
(when (and name-str type-str)
(setq str (format "%s : %s"
(setq str (format (if pretty "%s %s" "%s : %s")
(propertize name-str 'face 'font-lock-variable-name-face)
type-str)))
(when (and str coercion-str)

4
src/frontends/lean/info_manager.cpp
View file

@ -38,9 +38,7 @@ public:
#ifdef LEAN_JSON
virtual void report(io_state_stream const & ios, json & record) const override {
std::ostringstream ss;
ss << flatten(interactive_format_type(ios.get_environment(), ios.get_options(), m_expr));
record["type"] = ss.str();
interactive_report_type(ios.get_environment(), ios.get_options(), m_expr, record);
}
#endif
};

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

@ -17,21 +17,25 @@ Author: Sebastian Ullrich
namespace lean {
LEAN_THREAD_VALUE(break_at_pos_exception::token_context, g_context, break_at_pos_exception::token_context::none);
format interactive_format_type(environment const & env, options const & opts, expr const & e) {
void interactive_report_type(environment const & env, options const & opts, expr const & e, json & j) {
type_context tc(env);
format f;
if (g_context == break_at_pos_exception::token_context::interactive_tactic) {
vm_state vm(env, options());
tactic_state s(env, opts, "_interactive_format_type", {}, {}, mk_true(), {});
vm_obj r = vm.invoke({"interactive", "desc"}, {to_obj(s), to_obj(e)});
if (tactic::is_result_success(r))
return to_format(tactic::get_result_value(r));
f = to_format(tactic::get_result_value(r));
else
return format("<error while executing bla:") + space() + std::get<0>(*tactic::is_exception(vm, r)) +
format(">");
f = format("<error while executing bla:") + space() + std::get<0>(*tactic::is_exception(vm, r)) + format(">");
j["pretty"] = true;
} else {
return mk_pretty_formatter_factory()(env, opts, tc)(e);
f = mk_pretty_formatter_factory()(env, opts, tc)(e);
}
sstream ss;
ss << mk_pair(flatten(f), opts);
j["type"] = ss.str();
}
void report_completions(environment const & env, options const & opts, pos_info const & pos, bool skip_completions,
@ -63,14 +67,8 @@ void report_completions(environment const & env, options const & opts, pos_info
opts);
break;
case break_at_pos_exception::token_context::interactive_tactic:
if (!skip_completions) {
auto completions = get_interactive_tactic_completions(prefix, e.m_token_info.m_tac_class, env, opts);
// append regular completions
g_context = break_at_pos_exception::token_context::none;
for (auto candidate : get_decl_completions(prefix, env, opts))
completions.push_back(candidate);
j["completions"] = completions;
}
if (!skip_completions)
j["completions"] = get_interactive_tactic_completions(prefix, e.m_token_info.m_tac_class, env, opts);
break;
case break_at_pos_exception::token_context::attribute:
if (!skip_completions)

2
src/frontends/lean/interactive.h
View file

@ -9,7 +9,7 @@ Author: Sebastian Ullrich
#include "library/module_mgr.h"
#include "frontends/lean/parser.h"
namespace lean {
format interactive_format_type(environment const & env, options const & opts, expr const & e);
void interactive_report_type(environment const & env, options const & opts, expr const & e, json & j);
void report_completions(environment const & env, options const & opts, pos_info const & pos, bool skip_completions,
char const * mod_path, break_at_pos_exception const & e, json & j);
void report_info(environment const & env, options const & opts, io_state const & ios, module_info const & m_mod_info,

4
src/frontends/lean/json.cpp
View file

@ -69,9 +69,7 @@ json serialize_decl(name const & short_name, name const & long_name, environment
}
json completion;
completion["text"] = short_name.to_string();
std::ostringstream ss;
ss << mk_pair(flatten(interactive_format_type(env, o, type)), o);
completion["type"] = ss.str();
interactive_report_type(env, o, type, completion);
add_source_info(env, long_name, completion);
if (auto doc = get_doc_string(env, long_name))
completion["doc"] = *doc;