
  0 | ||| Re-exports Idris.Package with some private declarations.
  1 | |||
  2 | ||| `Idris.Package` private items are visible here because of the common module
  3 | ||| prefix.
  4 | |||
  5 | ||| Last updated with Idris2 commit 80fd5e4d754888e02a734b05011a98ee4334fd20.
  6 | module Idris.Package.Extra
  7 | 
  8 | import public Idris.Package
  9 | 
 10 | import Idris.Package as P
 11 | import Idris.REPL
 12 | import Idris.Syntax
 13 | import IdrisPaths
 14 | 
 15 | ||| Emit captured warnings from inner scope and clear them
 16 | ||| afterwards (to avoid emitting them in some unrelated
 17 | ||| codepath later).
 18 | export
 19 | withWarnings : Ref Ctxt Defs =>
 20 |                Ref Syn SyntaxInfo =>
 21 |                Ref ROpts REPLOpts =>
 22 |                Core a -> Core a
 23 | withWarnings = P.withWarnings
 24 | 
 25 | export
 26 | runScript : Maybe (FC, String) -> Core ()
 27 | runScript = P.runScript
 28 | 
 29 | ||| Add all dependencies (transitively) from the given package file into the
 30 | ||| context so modules from each is accessible during compilation.
 31 | export
 32 | addDeps :
 33 |     {auto c : Ref Ctxt Defs} ->
 34 |     {auto s : Ref Syn SyntaxInfo} ->
 35 |     {auto o : Ref ROpts REPLOpts} ->
 36 |     PkgDesc ->
 37 |     Core ()
 38 | addDeps = P.addDeps
 39 |