From 2db3a61160d387de96b82ef10ca6816505c67103 Mon Sep 17 00:00:00 2001
From: Nikita Vilunov <nikita@vilunov.me>
Date: Mon, 8 Jun 2020 01:31:16 +0300
Subject: [PATCH] implement "--repl"

---
 src/Idris/Main.idr    |  2 +-
 src/Idris/Package.idr | 16 ++++++++++------
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr
index 934348488..e14f3dd85 100644
--- a/src/Idris/Main.idr
+++ b/src/Idris/Main.idr
@@ -131,7 +131,6 @@ stMain opts
          defs <- initDefs
          c <- newRef Ctxt defs
          s <- newRef Syn initSyntax
-         m <- newRef MD initMetadata
          addPrimitives
 
          setWorkingDir "."
@@ -157,6 +156,7 @@ stMain opts
                  when (checkVerbose opts) $ -- override Quiet if implicitly set
                      setOutput (REPL False)
                  u <- newRef UST initUState
+                 m <- newRef MD initMetadata
                  updateREPLOpts
                  session <- getSession
                  when (not $ nobanner session) $
diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr
index 16fcddfd7..4e641258a 100644
--- a/src/Idris/Package.idr
+++ b/src/Idris/Package.idr
@@ -444,15 +444,16 @@ getParseErrorLoc fname _ = replFC
 -- Just load the 'Main' module, if it exists, which will involve building
 -- it if necessary
 runRepl : {auto c : Ref Ctxt Defs} ->
+          {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           PkgDesc ->
           List CLOpt ->
           Core ()
-runRepl pkg opts
-    = do addDeps pkg
-         processOptions (options pkg)
-         preOptions opts
-         throw (InternalError "Not implemented")
+runRepl pkg opts = do
+  u <- newRef UST initUState
+  m <- newRef MD initMetadata
+  repl {u} {s}
+
 
 processPackage : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
@@ -480,7 +481,10 @@ processPackage cmd file opts
                                        | errs => coreLift (exitWith (ExitFailure 1))
                                     install pkg opts
                       Clean => clean pkg opts
-                      REPL => runRepl pkg opts
+                      REPL => do
+                        [] <- build pkg opts
+                           | errs => coreLift (exitWith (ExitFailure 1))
+                        runRepl pkg opts
 
 record POptsFilterResult where
   constructor MkPFR