diff --git a/src/Init/Lean/Elab/Frontend.lean b/src/Init/Lean/Elab/Frontend.lean
index e02723832a..431bf6544f 100644
--- a/src/Init/Lean/Elab/Frontend.lean
+++ b/src/Init/Lean/Elab/Frontend.lean
@@ -62,6 +62,14 @@ end Frontend
 
 open Frontend
 
+def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : Environment × MessageLog :=
+let fileName := fileName.getD "<input>";
+let ctx      := Parser.mkParserContextCore env input fileName;
+let cmdState := Command.mkState env {} opts;
+match (processCommands ctx).run { commandState := cmdState, parserState := {} } with
+| EStateM.Result.ok _ s    => (s.commandState.env, s.commandState.messages)
+| EStateM.Result.error _ s => (s.commandState.env, s.commandState.messages)
+
 def testFrontend (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) :=
 do env ← mkEmptyEnvironment;
    let fileName := fileName.getD "<input>";
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 1102ce5cec..3e96b5f1b9 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -3,16 +3,16 @@ open Lean
 open Lean.Elab
 
 def run (input : String) : MetaIO Unit :=
-do opts ← MetaIO.getOptions;
-   (env, messages) ← liftM $ testFrontend input opts;
+do env  ← MetaIO.getEnv;
+   opts ← MetaIO.getOptions;
+   let (env, messages) := process input env opts;
    messages.toList.forM $ fun msg => IO.println msg;
    pure ()
 
 set_option trace.Elab true
 
 #eval run
-"import Init.Core
- universe u universe v
+"universe u universe v
  section namespace foo.bla end bla end foo
  variable (p q : Prop)
  variable (_ b : _)
@@ -24,4 +24,5 @@ set_option trace.Elab true
  #check α
  #check Nat.succ
  #check Nat.add
+ #check run
  end"