||| Re-exports Idris.Package with some private declarations.
|||
||| `Idris.Package` private items are visible here because of the common module
||| prefix.
|||
||| Last updated with Idris2 commit 80fd5e4d754888e02a734b05011a98ee4334fd20.
module Idris.Package.Extra

import public Idris.Package

import Idris.Package as P
import Idris.REPL
import Idris.Syntax
import IdrisPaths

||| Emit captured warnings from inner scope and clear them
||| afterwards (to avoid emitting them in some unrelated
||| codepath later).
export
withWarnings : Ref Ctxt Defs =>
               Ref Syn SyntaxInfo =>
               Ref ROpts REPLOpts =>
               Core a -> Core a
withWarnings = P.withWarnings

export
runScript : Maybe (FC, String) -> Core ()
runScript = P.runScript

||| Add all dependencies (transitively) from the given package file into the
||| context so modules from each is accessible during compilation.
export
addDeps :
    {auto c : Ref Ctxt Defs} ->
    {auto s : Ref Syn SyntaxInfo} ->
    {auto o : Ref ROpts REPLOpts} ->
    PkgDesc ->
    Core ()
addDeps = P.addDeps