From 9b5e7ddcdaa67e41aaf5ea0fc99d317ed372b937 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Mar 2017 11:26:41 +0100 Subject: [PATCH] feat(frontends/lean/interactive,emacs): hide colon separator in front of pretty-printed types --- src/emacs/lean-company.el | 8 +++++--- src/emacs/lean-type.el | 4 ++-- src/frontends/lean/info_manager.cpp | 4 +--- src/frontends/lean/interactive.cpp | 24 +++++++++++------------- src/frontends/lean/interactive.h | 2 +- src/frontends/lean/json.cpp | 4 +--- 6 files changed, 21 insertions(+), 25 deletions(-) diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el index 814113054c..2047018635 100644 --- a/src/emacs/lean-company.el +++ b/src/emacs/lean-company.el @@ -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 diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index f0d11db935..fa0d7b8044 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -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) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 465d1c773c..bd7b821395 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -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 }; diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index a76a297c58..dc2a04637d 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -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("(*tactic::is_exception(vm, r)) + - format(">"); + f = format("(*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) diff --git a/src/frontends/lean/interactive.h b/src/frontends/lean/interactive.h index ab68889f30..e7d6de3bef 100644 --- a/src/frontends/lean/interactive.h +++ b/src/frontends/lean/interactive.h @@ -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, diff --git a/src/frontends/lean/json.cpp b/src/frontends/lean/json.cpp index ec1dcfa51b..3553aec725 100644 --- a/src/frontends/lean/json.cpp +++ b/src/frontends/lean/json.cpp @@ -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;