diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index f4a1991eef..8261478d13 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -128,6 +128,22 @@ data IDEResult | TTTerm String -- should be a TT Term + metadata, or perhaps SExp | NameLocList (List (Name, FC)) | VersionSExp Version + | OptionsSExp (List REPLOpt) + +getOptions : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + Core (List REPLOpt) +getOptions = do + pp <- getPPrint + opts <- get ROpts + pure $ [ ShowImplicits (showImplicits pp) + , ShowMachineNames (showMachineNames pp) + , ShowNamespace (fullNamespace pp) + , ShowTypes (showTypes opts) + , EvalMode (evalMode opts) + , Editor (editor opts) + ] + replWrap : Core REPLResult -> Core IDEResult replWrap m = pure $ REPL !m @@ -238,7 +254,8 @@ process Version process (Metavariables _) = FoundHoles <$> getUserHolesData process GetOptions - = replWrap $ Idris.REPL.process GetOpts + = do opts <- getOptions + pure $ OptionsSExp opts processCatch : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> @@ -364,6 +381,9 @@ displayIDEResult outf i (REPL $ LogLevelSet k) = printIDEResult outf i $ AString $ "Set loglevel to " ++ show k displayIDEResult outf i (REPL $ OptionsSet opts) + = printIDEResult outf i + $ AString $ showSep "\n" $ map show opts +displayIDEResult outf i (OptionsSExp opts) = printIDEResult outf i $ AnOptionList $ map cast opts displayIDEResult outf i (REPL $ VersionIs x) = printIDEResult outf i $ AString (showVersion True x) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 84c00483b0..e1b31bd692 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -194,9 +194,11 @@ getOptions : {auto c : Ref Ctxt Defs} -> getOptions = do pp <- getPPrint opts <- get ROpts - pure $ [ ShowImplicits (showImplicits pp), ShowMachineNames (showMachineNames pp) + pure $ [ ShowImplicits (showImplicits pp) + , ShowMachineNames (showMachineNames pp) , ShowNamespace (fullNamespace pp) - , ShowTypes (showTypes opts), EvalMode (evalMode opts) + , ShowTypes (showTypes opts) + , EvalMode (evalMode opts) , Editor (editor opts) ]