diff --git a/src/Init/Lean/Elab/Frontend.lean b/src/Init/Lean/Elab/Frontend.lean
index a0dc89cccd..fdc0fa6d15 100644
--- a/src/Init/Lean/Elab/Frontend.lean
+++ b/src/Init/Lean/Elab/Frontend.lean
@@ -91,6 +91,11 @@ IO.processCommands parserCtx parserStateRef cmdStateRef;
 cmdState ← cmdStateRef.get;
 pure (cmdState.env, cmdState.messages)
 
+@[export lean_process_input]
+def processExport (env : Environment) (input : String) (opts : Options) (fileName : String) : IO (Environment × List Message) := do
+(env, messages) ← process input env opts fileName;
+pure (env, messages.toList)
+
 def runFrontend (env : Environment) (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) := do
 let fileName := fileName.getD "<input>";
 let parserCtx := Parser.mkParserContextCore env input fileName;
diff --git a/src/Init/Lean/Parser/Module.lean b/src/Init/Lean/Parser/Module.lean
index 3a6c8d0f92..f9dda147bd 100644
--- a/src/Init/Lean/Parser/Module.lean
+++ b/src/Init/Lean/Parser/Module.lean
@@ -72,6 +72,7 @@ partial def parseCommand (env : Environment) (c : ParserContextCore) : ModulePar
   else
     let c  := c.toParserContext env;
     let s  := { ParserState . cache := initCacheForInput c.input, pos := pos };
+    let s  := whitespace c s;
     let s  := (commandParser : Parser).fn (0:Nat) c s;
     match s.errorMsg with
     | none =>
diff --git a/src/Init/Lean/Util/Message.lean b/src/Init/Lean/Util/Message.lean
index 6e7e5b9531..b75975e5b1 100644
--- a/src/Init/Lean/Util/Message.lean
+++ b/src/Init/Lean/Util/Message.lean
@@ -123,11 +123,17 @@ mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column
    | MessageSeverity.error => "error: ") ++
   (if msg.caption == "" then "" else msg.caption ++ ":\n") ++ toString (fmt msg.data))
 
+
 instance : Inhabited Message :=
 ⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary _}⟩
 
 instance : HasToString Message :=
 ⟨Message.toString⟩
+
+@[export lean_message_pos] def getPostEx (msg : Message) : Position := msg.pos
+@[export lean_message_severity] def getSeverityEx (msg : Message) : MessageSeverity := msg.severity
+@[export lean_message_string] def getMessageStringEx (msg : Message) : String := toString (fmt msg.data)
+
 end Message
 
 structure MessageLog :=
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index bf0690779e..3b1a3e8a31 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "runtime/flet.h"
 #include "runtime/utf8.h"
 #include "util/option_declarations.h"
+#include "util/io.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
 #include "kernel/find_fn.h"
@@ -1959,7 +1960,7 @@ unsigned parser::curr_lbp() const {
         return get_token_info().expr_precedence();
     case token_kind::CommandKeyword: case token_kind::Eof:
     case token_kind::QuotedSymbol:   case token_kind::DocBlock:
-    case token_kind::ModDocBlock:
+    case token_kind::ModDocBlock:    case token_kind::NewFrontend:
         return 0;
     case token_kind::Identifier:     case token_kind::Numeral:
     case token_kind::Decimal:        case token_kind::String:
@@ -2103,6 +2104,49 @@ void parser::parse_mod_doc_block() {
     next();
 }
 
+extern "C" object * lean_process_input(object * env, object * input, object * opts, object * filename, object * w);
+
+typedef list_ref<object_ref> messages;
+
+pair_ref<environment, messages> process_input(environment const & env, std::string const & input, options const & opts, std::string const & file_name) {
+    return get_io_result<pair_ref<environment, messages>>(lean_process_input(env.to_obj_arg(), mk_string(input), opts.to_obj_arg(), mk_string(file_name), io_mk_world()));
+}
+
+extern "C" object * lean_message_pos(object * msg);
+extern "C" uint8 lean_message_severity(object * msg);
+extern "C" object * lean_message_string(object * msg);
+
+static pos_info get_message_pos(object_ref const & msg) {
+    auto p = pair_ref<nat, nat>(lean_message_pos(msg.to_obj_arg()));
+    return pos_info(p.fst().get_small_value(), p.snd().get_small_value());
+}
+
+static message_severity get_message_severity(object_ref const & msg) {
+    return static_cast<message_severity>(lean_message_severity(msg.to_obj_arg()));
+}
+
+static std::string get_message_string(object_ref const & msg) {
+    string_ref r(lean_message_string(msg.to_obj_arg()));
+    return r.to_std_string();
+}
+
+void parser::parse_new_frontend_cmd() {
+    auto curr_pos = pos();
+    std::string input = m_scanner.get_str_val();
+    next();
+    pair_ref<environment, messages> result = process_input(m_env, input, get_options(), m_file_name);
+    set_env(result.fst());
+    for (auto msg : result.snd()) {
+        pos_info pos = get_message_pos(msg);
+        pos.first += curr_pos.first;
+        message_severity sev = get_message_severity(msg);
+        std::string str = get_message_string(msg);
+        auto builder = mk_message(pos, sev);
+        builder << str;
+        builder.report();
+    }
+}
+
 #if defined(__GNUC__) && !defined(__CLANG__)
 #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
 #endif
@@ -2146,6 +2190,9 @@ bool parser::parse_command_like() {
         case token_kind::ModDocBlock:
             parse_mod_doc_block();
             break;
+        case token_kind::NewFrontend:
+            parse_new_frontend_cmd();
+            break;
         case token_kind::Eof:
             if (has_open_scopes(m_env)) {
                 maybe_throw_error({"invalid end of module, expecting 'end'", pos()});
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 5dce5d4214..7975dcf23c 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -92,6 +92,7 @@ struct parser : public abstract_parser {
 
     std::string parse_doc_block();
     void parse_mod_doc_block();
+    void parse_new_frontend_cmd();
 
     void process_imports();
     void process_postponed(buffer<expr> const & args, bool is_left, buffer<notation::action_kind> const & kinds,
diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 06baaad68c..09ad7c5a9f 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -377,6 +377,17 @@ auto scanner::read_mod_doc_block() -> token_kind {
     return token_kind::ModDocBlock;
 }
 
+auto scanner::read_new_frontend() -> token_kind {
+    m_buffer.clear();
+    while (true) {
+        uchar c = curr();
+        if (c == Eof) break;
+        next();
+        m_buffer += c;
+    }
+    return token_kind::NewFrontend;
+}
+
 void scanner::read_comment_block() {
     unsigned nesting = 1;
     while (true) {
@@ -620,6 +631,7 @@ static name * g_begin_comment_block_tk  = nullptr;
 static name * g_begin_doc_block_tk      = nullptr;
 static name * g_begin_mod_doc_block_tk  = nullptr;
 static name * g_tick_tk                 = nullptr;
+static name * g_new_frontend_tk         = nullptr;
 
 void initialize_scanner() {
     g_begin_comment_tk       = new name("--");
@@ -627,6 +639,7 @@ void initialize_scanner() {
     g_begin_doc_block_tk     = new name("/--");
     g_begin_mod_doc_block_tk = new name("/-!");
     g_tick_tk                = new name("'");
+    g_new_frontend_tk        = new name("new_frontend");
 }
 
 void finalize_scanner() {
@@ -635,6 +648,7 @@ void finalize_scanner() {
     delete g_begin_doc_block_tk;
     delete g_begin_mod_doc_block_tk;
     delete g_tick_tk;
+    delete g_new_frontend_tk;
 }
 
 auto scanner::scan(environment const & env) -> token_kind {
@@ -676,6 +690,8 @@ auto scanner::scan(environment const & env) -> token_kind {
                         return read_mod_doc_block();
                     else if (n == *g_tick_tk)
                         return read_char();
+                    else if (n == *g_new_frontend_tk)
+                        return read_new_frontend();
                     else
                         return k;
                 } else {
@@ -756,7 +772,7 @@ void token::dealloc() {
     case token_kind::Numeral: case token_kind::Decimal: case token_kind::FieldNum:
         if (m_num_val != nullptr) delete m_num_val;
         return;
-    case token_kind::String: case token_kind::Char:
+    case token_kind::String: case token_kind::Char: case token_kind::NewFrontend:
     case token_kind::DocBlock: case token_kind::ModDocBlock:
         if (m_str_val != nullptr) delete m_str_val;
         return;
@@ -778,7 +794,7 @@ void token::copy(token const & tk) {
     case token_kind::Numeral: case token_kind::Decimal: case token_kind::FieldNum:
         m_num_val = new mpq(*tk.m_num_val);
         return;
-    case token_kind::String: case token_kind::Char:
+    case token_kind::String: case token_kind::Char: case token_kind::NewFrontend:
     case token_kind::DocBlock: case token_kind::ModDocBlock:
         m_str_val = new std::string(*tk.m_str_val);
         return;
@@ -803,7 +819,7 @@ void token::steal(token && tk) {
         m_num_val    = tk.m_num_val;
         tk.m_num_val = nullptr;
         return;
-    case token_kind::String: case token_kind::Char:
+    case token_kind::String: case token_kind::Char: case token_kind::NewFrontend:
     case token_kind::DocBlock: case token_kind::ModDocBlock:
         m_str_val    = tk.m_str_val;
         tk.m_str_val = nullptr;
@@ -833,7 +849,7 @@ token read_tokens(environment & env, io_state const & ios, scanner & s, buffer<t
             case token_kind::Numeral: case token_kind::Decimal: case token_kind::FieldNum:
                 tk.push_back(token(k, s.get_pos_info(), s.get_num_val()));
                 break;
-            case token_kind::String: case token_kind::Char:
+            case token_kind::String: case token_kind::Char: case token_kind::NewFrontend:
             case token_kind::DocBlock: case token_kind::ModDocBlock:
                 tk.push_back(token(k, s.get_pos_info(), s.get_str_val()));
                 break;
diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h
index 56c90b6f96..565dfedb51 100644
--- a/src/frontends/lean/scanner.h
+++ b/src/frontends/lean/scanner.h
@@ -19,7 +19,7 @@ Author: Leonardo de Moura
 namespace lean {
 enum class token_kind {Keyword, CommandKeyword, Identifier, Numeral, Decimal,
         String, Char, QuotedSymbol,
-        DocBlock, ModDocBlock, FieldNum, FieldName, Eof};
+        DocBlock, ModDocBlock, FieldNum, FieldName, NewFrontend, Eof};
 
 /**
     \brief Scanner. The behavior of the scanner is controlled using a token set.
@@ -85,6 +85,7 @@ public:
     void read_doc_block_core();
     token_kind read_doc_block();
     token_kind read_mod_doc_block();
+    token_kind read_new_frontend();
 
 public:
     scanner(std::istream & strm, char const * strm_name = nullptr);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 1c5466bd0d..e51174cd28 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -92,7 +92,7 @@ void init_token_table(token_table & t) {
          {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0},
          {"//", 0}, {"|", 0}, {"with", 0}, {"without", 0}, {"..", 0}, {"...", 0}, {",", 0}, {";", 0}, {"=>", 0},
          {".", 0}, {":", 0}, {"!", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
-         {"/-", 0}, {"/--", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0},
+         {"/-", 0}, {"/--", 0}, {"new_frontend", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0},
          {"@@", g_max_prec}, {"@", g_max_prec}, {"@&", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
          {"match", 0}, {"nomatch", 0}, {"^.", g_max_prec+1}, {"::", 67},