diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 5f74c37527..6dab04b184 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -760,7 +760,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
                 return elaborate_proof(decl_env, opts, header_pos, new_params_list,
                                        new_fn, val, thm_finfo, is_rfl, type,
                                        mctx, lctx, pos_provider, use_info_manager, file_name);
-            }));
+            }), log_tree::ElaborationLevel);
             env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, proof, modifiers, attrs,
                                        doc_string, header_pos);
         } else if (kind == Example) {
@@ -777,7 +777,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
                 check_example(env, opts, modifiers, lp_name_list, new_params_list, fn, val, mctx, lctx,
                               pos_provider, use_info_manager, file_name);
                 return unit();
-            });
+            }, log_tree::ElaborationLevel);
             return p.env();
         } else {
             std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index d2f9dcbc72..a7901d0da8 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2260,7 +2260,7 @@ void parser::process_imports() {
                         report_message(message(fn, pos, WARNING,
                                                (sstream() << "imported file '" << mod_name << "' uses sorry").str()));
                     return unit {};
-                }));
+                }), log_tree::CrossModuleLintLevel);
 
                 return mod;
             };
diff --git a/src/library/library_task_builder.h b/src/library/library_task_builder.h
index 12b91ba59b..24d425c49f 100644
--- a/src/library/library_task_builder.h
+++ b/src/library/library_task_builder.h
@@ -26,8 +26,9 @@ struct exception_reporter {
 };
 
 template <class Res>
-task<Res> add_library_task(task_builder<Res> && builder, std::string const & description, bool add_producer = true) {
-    auto lt = logtree().mk_child({}, description, logtree().get_location());
+task<Res> add_library_task(task_builder<Res> && builder, std::string const & description,
+                           bool add_producer = true, log_tree::detail_level lvl = log_tree::DefaultLevel) {
+    auto lt = logtree().mk_child({}, description, logtree().get_location(), lvl);
     auto task = builder.wrap(library_scopes(lt)).build();
     if (add_producer) lt.set_producer(task);
     return task;
@@ -39,8 +40,10 @@ task<Res> mk_library_task(task_builder<Res> && builder, std::string const & desc
 }
 
 template <class Res>
-task<Res> add_library_task(task_builder<Res> && builder, bool add_producer = true) {
-    return add_library_task(std::forward<task_builder<Res>>(builder), {}, add_producer);
+task<Res> add_library_task(task_builder<Res> && builder,
+                           log_tree::detail_level lvl = log_tree::DefaultLevel,
+                           bool add_producer = true) {
+    return add_library_task(std::forward<task_builder<Res>>(builder), {}, add_producer, lvl);
 }
 
 }
diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp
index 2978e27ffd..a8fe9a29be 100644
--- a/src/library/module_mgr.cpp
+++ b/src/library/module_mgr.cpp
@@ -155,7 +155,7 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set
         if (!existing_mod->m_out_of_date) return;
 
     scope_global_ios scope_ios(m_ios);
-    scope_log_tree lt(m_lt.mk_child(id, {}, { id, {{1, 0}, {static_cast<unsigned>(-1), 0}} }, true));
+    scope_log_tree lt(m_lt.mk_child(id, {}, { id, {{1, 0}, {static_cast<unsigned>(-1), 0}} }, log_tree::DefaultLevel, true));
     scope_traces_as_messages scope_trace_msgs(id, {1, 0});
 
     try {
diff --git a/src/library/mt_task_queue.h b/src/library/mt_task_queue.h
index 67b97d55d7..0d30c0920b 100644
--- a/src/library/mt_task_queue.h
+++ b/src/library/mt_task_queue.h
@@ -74,7 +74,7 @@ public:
     void wait_for_finish(gtask const & t) override;
     void fail_and_dispose(gtask const &t) override;
 
-    void submit(gtask const & t, unsigned prio);
+    void submit(gtask const & t, unsigned prio) override;
     void submit(gtask const & t) override;
 
     void evacuate() override;
diff --git a/src/shell/lean_js.cpp b/src/shell/lean_js.cpp
index daba5cb0a8..4b6cb55992 100644
--- a/src/shell/lean_js.cpp
+++ b/src/shell/lean_js.cpp
@@ -33,7 +33,7 @@ public:
 
     int process_request(std::string msg) {
         scope_global_ios scoped_ios(m_ios);
-        scope_log_tree lt(m_server.get_log_tree().get_root().mk_child("_server", {}, {}, true));
+        scope_log_tree lt(m_server.get_log_tree().get_root().mk_child("_server", {}, {}, log_tree::DefaultLevel, true));
         try {
             m_server.handle_request(json::parse(msg));
             return 0;
diff --git a/src/shell/server.cpp b/src/shell/server.cpp
index b0ac5228d5..d4ee41fc89 100644
--- a/src/shell/server.cpp
+++ b/src/shell/server.cpp
@@ -52,6 +52,7 @@ struct all_messages_msg {
 
 bool region_of_interest::intersects(log_tree::node const & n) const {
     if (!m_enabled) return true;
+    if (n.get_detail_level() > m_max_level) return false;
     if (n.get_location().m_file_name.empty()) return true;
     auto & l = n.get_location();
     if (auto f = m_files.find(l.m_file_name)) {
@@ -193,9 +194,8 @@ public:
     }
 
     void submit_core(log_tree::node const & n) {
-        // TODO(gabriel): priorities
         if (auto prod = n.get_producer()) {
-            taskq().submit(prod);
+            taskq().submit(prod, n.get_detail_level());
         }
     }
 
@@ -351,7 +351,14 @@ struct unrelated_error_msg {
     }
 };
 
+server * g_server = nullptr;
+
+void server_dump_log_tree() { g_server->dump_log_tree(); }
+void server::dump_log_tree() { m_lt.print_to(std::cerr); }
+
 void server::run() {
+    flet<server *> _(g_server, this);
+
     scope_global_ios scoped_ios(m_ios);
 
     /* Leo: we use std::setlocale to make sure decimal period is displayed as ".".
diff --git a/src/shell/server.h b/src/shell/server.h
index 2c83f19614..4c5e78b414 100644
--- a/src/shell/server.h
+++ b/src/shell/server.h
@@ -32,6 +32,7 @@ struct string_cmp {
 
 struct region_of_interest {
     bool m_enabled = false;
+    log_tree::detail_level m_max_level = log_tree::CrossModuleLintLevel-1;
     rb_map<std::string, line_range, string_cmp> m_files;
 
     bool intersects(log_tree::node const & n) const;
@@ -96,6 +97,9 @@ public:
     log_tree & get_log_tree() { return m_lt; }
 
     region_of_interest get_roi();
+
+    // debugging
+    void dump_log_tree();
 };
 
 void initialize_server();
diff --git a/src/util/log_tree.cpp b/src/util/log_tree.cpp
index 5289c79a06..7a5e9ad294 100644
--- a/src/util/log_tree.cpp
+++ b/src/util/log_tree.cpp
@@ -99,7 +99,7 @@ void log_tree::node::add(log_entry const & entry) const {
 }
 
 log_tree::node log_tree::node::mk_child(name n, std::string const & description, location const & loc,
-                                        bool overwrite) {
+                                        detail_level lvl, bool overwrite) {
     auto l = lock();
     std::vector<event> events;
 
@@ -123,6 +123,7 @@ log_tree::node log_tree::node::mk_child(name n, std::string const & description,
         child.m_ptr->m_tree = m_ptr->m_tree;
         child.m_ptr->m_detached = m_ptr->m_detached;
     }
+    child.m_ptr->m_detail_level = std::max(m_ptr->m_detail_level, lvl);
     child.m_ptr->m_description = description;
     child.m_ptr->m_location = loc;
     m_ptr->m_children.insert(n, child);
@@ -217,7 +218,8 @@ void log_tree::node::print_to(std::ostream & out, unsigned indent) const {
         << ": " << begin.first << ":" << begin.second << " -- " << end.first << ":" << end.second << ": "
         << m_ptr->m_description << " ("
         << m_ptr->m_entries.size()
-        << " entries, producer = "
+        << " entries, detail level = "
+        << m_ptr->m_detail_level << ", producer = "
         << std::hex << reinterpret_cast<uintptr_t>(m_ptr->m_producer.get()) << std::dec
         << ")" << std::endl;
 
diff --git a/src/util/log_tree.h b/src/util/log_tree.h
index e79dc24809..bb0027beb4 100644
--- a/src/util/log_tree.h
+++ b/src/util/log_tree.h
@@ -31,6 +31,13 @@ public:
     struct event;
     using listener = std::function<void(std::vector<event> const &)>;
 
+    using detail_level = unsigned;
+    constexpr static detail_level
+        DefaultLevel = 100,
+        ElaborationLevel = 200,
+        CrossModuleLintLevel = 1000,
+        MaxLevel = std::numeric_limits<detail_level>::max();
+
     struct node_cell {
         MK_LEAN_RC()
         void dealloc() { delete this; }
@@ -46,6 +53,7 @@ public:
         location m_location;
         std::string m_description;
         gtask m_producer;
+        detail_level m_detail_level = DefaultLevel;
 
         node_cell() : m_rc(0) {}
     };
@@ -82,12 +90,14 @@ public:
         name_map<node> get_used_children() const;
         void remove_child(name const &) const;
 
-        node mk_child(name n, std::string const & description, location const & loc, bool overwrite = false);
+        node mk_child(name n, std::string const & description, location const & loc,
+                      detail_level lvl = DefaultLevel, bool overwrite = false);
         void reuse(name const & n) const;
 
         void finish() const;
 
         void set_producer(gtask const &);
+        detail_level get_detail_level() const { return m_ptr->m_detail_level; }
         location const & get_location() const { return m_ptr->m_location; }
         std::string const & get_description() const { return m_ptr->m_description; }
         name_set get_used_names() const;
diff --git a/src/util/task.cpp b/src/util/task.cpp
index fa131a166c..7293bfacbd 100644
--- a/src/util/task.cpp
+++ b/src/util/task.cpp
@@ -69,6 +69,10 @@ void task_queue::fail(gtask const & t, gtask const & failed) {
     fail(t, failed->m_exception);
 }
 
+void task_queue::submit(gtask const & t, unsigned) {
+    return submit(t);
+}
+
 static task_queue * g_taskq = nullptr;
 
 void set_task_queue(task_queue * q) {
diff --git a/src/util/task.h b/src/util/task.h
index eee2b4890c..7a92cbffbb 100644
--- a/src/util/task.h
+++ b/src/util/task.h
@@ -145,6 +145,7 @@ public:
     virtual void join() = 0;
 
     virtual void submit(gtask const &) = 0;
+    virtual void submit(gtask const &, unsigned prio);
 };
 
 void set_task_queue(task_queue *); // NOLINT