mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 16:21:46 +03:00
First steps towards emacs idris-mode compatibility
To make sure the protocol doesn't jam, supply stub implementation to all protocol commands. Report to REPL when an unimplemented command is used. Notes ----- 1. We don't support add-proof-clause. I guess all proof-related stuff should be removed from the protocol 2. Some types are stub types too. That's because we need to `SExpable` more structured types like `PTerm`. I'll leave that to the future. 3. I've lifted `REPLResult` into `IDEResult` inside `IDEMode/REPL.idr`. That's because some results, like `who-calls` only make sense in the context of an IDE, not in the context of a user-facing REPL. The Editing commands should be moved from the REPL into the IDE and called from the REPL. I leave that to the future, once more of the protocol is implemented. 4. Export a few functions from the REPL so that the IDE can call them. 5. There's one outstanding issue with the emacs idris-mode: it currently calls the unsupported `:consolewidth` REPL command. This is harmless, and can wait until @edwinb decides whether we should support it in the future or not. 6. There was a bug as to how holes are returned to the user. The format isn't documented in the protocol, so we'll need to reproduce it, perhaps from the idris-mode elisp sources.
This commit is contained in:
Ohad Kammar
parent
1945619db7
commit
83793113ba
@ -15,6 +15,9 @@ data SExp = SExpList (List SExp)
|
||||
| IntegerAtom Integer
|
||||
| SymbolAtom String
|
||||
|
||||
public export
|
||||
data DocMode = Overview | Full
|
||||
|
||||
public export
|
||||
data IDECommand
|
||||
= Interpret String
|
||||
@ -22,12 +25,25 @@ data IDECommand
|
||||
| TypeOf String (Maybe (Integer, Integer))
|
||||
| CaseSplit Integer Integer String
|
||||
| AddClause Integer String
|
||||
-- deprecated: | AddProofClause
|
||||
| AddMissing Integer String
|
||||
| ExprSearch Integer String (List String) Bool
|
||||
| GenerateDef Integer String
|
||||
| MakeLemma Integer String
|
||||
| MakeCase Integer String
|
||||
| MakeWith Integer String
|
||||
| DocsFor String (Maybe DocMode)
|
||||
| Apropos String
|
||||
| Metavariables Integer
|
||||
| WhoCalls String
|
||||
| CallsWho String
|
||||
| BrowseNamespace String
|
||||
| NormaliseTerm String -- TODO: implement a Binary lib
|
||||
| ShowTermImplicits String -- and implement Binary (Term)
|
||||
| HideTermImplicits String -- for these four defintions,
|
||||
| ElaborateTerm String -- then change String to Term, as in idris1
|
||||
| PrintDefinition String
|
||||
| ReplCompletions String
|
||||
| Version
|
||||
| GetOptions
|
||||
|
||||
@ -58,6 +74,8 @@ getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n])
|
||||
= Just $ CaseSplit l 0 n
|
||||
getIDECommand (SExpList [SymbolAtom "add-clause", IntegerAtom l, StringAtom n])
|
||||
= Just $ AddClause l n
|
||||
getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
|
||||
= Just $ AddMissing line n
|
||||
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n])
|
||||
= Just $ ExprSearch l n [] False
|
||||
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, SExpList hs])
|
||||
@ -79,8 +97,36 @@ getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n])
|
||||
= Just $ MakeCase l n
|
||||
getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])
|
||||
= Just $ MakeWith l n
|
||||
getIDECommand (SExpList (SymbolAtom "docs-for" :: StringAtom n :: modeTail))
|
||||
= do -- Maybe monad
|
||||
modeOpt <- case modeTail of
|
||||
[] => Just Nothing
|
||||
[SymbolAtom "overview"] => Just $ Just Overview
|
||||
[SymbolAtom "full" ] => Just $ Just Full
|
||||
_ => Nothing
|
||||
Just $ DocsFor n modeOpt
|
||||
getIDECommand (SExpList [SymbolAtom "apropos", StringAtom n])
|
||||
= Just $ Apropos n
|
||||
getIDECommand (SExpList [SymbolAtom "metavariables", IntegerAtom n])
|
||||
= Just $ Metavariables n
|
||||
getIDECommand (SExpList [SymbolAtom "who-calls", StringAtom n])
|
||||
= Just $ WhoCalls n
|
||||
getIDECommand (SExpList [SymbolAtom "calls-who", StringAtom n])
|
||||
= Just $ CallsWho n
|
||||
getIDECommand (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
|
||||
= Just $ BrowseNamespace ns
|
||||
getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm])
|
||||
= Just $ NormaliseTerm tm
|
||||
getIDECommand (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
|
||||
= Just $ ShowTermImplicits tm
|
||||
getIDECommand (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
|
||||
= Just $ HideTermImplicits tm
|
||||
getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
|
||||
= Just $ ElaborateTerm tm
|
||||
getIDECommand (SExpList [SymbolAtom "print-definition", StringAtom n])
|
||||
= Just $ PrintDefinition n
|
||||
getIDECommand (SExpList [SymbolAtom "repl-completions", StringAtom n])
|
||||
= Just $ ReplCompletions n
|
||||
getIDECommand (SymbolAtom "version") = Just Version
|
||||
getIDECommand (SExpList [SymbolAtom "get-options"]) = Just GetOptions
|
||||
getIDECommand _ = Nothing
|
||||
@ -94,6 +140,7 @@ putIDECommand (TypeOf cmd Nothing) = (SExpList [SymbolAtom "type-of",
|
||||
putIDECommand (TypeOf cmd (Just (line, col))) = (SExpList [SymbolAtom "type-of", StringAtom cmd, IntegerAtom line, IntegerAtom col])
|
||||
putIDECommand (CaseSplit line col n) = (SExpList [SymbolAtom "case-split", IntegerAtom line, IntegerAtom col, StringAtom n])
|
||||
putIDECommand (AddClause line n) = (SExpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n])
|
||||
putIDECommand (AddMissing line n) = (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
|
||||
putIDECommand (ExprSearch line n exprs mode) = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, SExpList $ map StringAtom exprs, getMode mode])
|
||||
where
|
||||
getMode : Bool -> SExp
|
||||
@ -103,7 +150,22 @@ putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate-
|
||||
putIDECommand (MakeLemma line n) = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
|
||||
putIDECommand (MakeCase line n) = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
|
||||
putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
|
||||
putIDECommand (DocsFor n modeOpt) = let modeTail = case modeOpt of
|
||||
Nothing => []
|
||||
Just Overview => [SymbolAtom "overview"]
|
||||
Just Full => [SymbolAtom "full"] in
|
||||
(SExpList (SymbolAtom "docs-for" :: StringAtom n :: modeTail))
|
||||
putIDECommand (Apropos n) = (SExpList [SymbolAtom "apropos", StringAtom n])
|
||||
putIDECommand (Metavariables n) = (SExpList [SymbolAtom "metavariables", IntegerAtom n])
|
||||
putIDECommand (WhoCalls n) = (SExpList [SymbolAtom "who-calls", StringAtom n])
|
||||
putIDECommand (CallsWho n) = (SExpList [SymbolAtom "calls-who", StringAtom n])
|
||||
putIDECommand (BrowseNamespace ns) = (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
|
||||
putIDECommand (NormaliseTerm tm) = (SExpList [SymbolAtom "normalise-term", StringAtom tm])
|
||||
putIDECommand (ShowTermImplicits tm) = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
|
||||
putIDECommand (HideTermImplicits tm) = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
|
||||
putIDECommand (ElaborateTerm tm) = (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
|
||||
putIDECommand (PrintDefinition n) = (SExpList [SymbolAtom "print-definition", StringAtom n])
|
||||
putIDECommand (ReplCompletions n) = (SExpList [SymbolAtom "repl-completions", StringAtom n])
|
||||
putIDECommand GetOptions = (SExpList [SymbolAtom "get-options"])
|
||||
putIDECommand Version = SymbolAtom "version"
|
||||
|
||||
|
||||
@ -119,49 +119,99 @@ getInput f
|
||||
do inp <- getNChars f (integerToNat (cast num))
|
||||
pure (pack inp)
|
||||
|
||||
||| Do nothing and tell the user to wait for us to implmement this (or join the effort!)
|
||||
todoCmd : {auto o : Ref ROpts REPLOpts} ->
|
||||
String -> Core ()
|
||||
todoCmd cmdName = iputStrLn $ cmdName ++ ": command not yet implemented. Hopefully soon!"
|
||||
|
||||
|
||||
data IDEResult
|
||||
= REPL REPLResult
|
||||
| NameList (List Name)
|
||||
| Term String -- should be a PTerm + metadata, or SExp.
|
||||
| TTTerm String -- should be a TT Term + metadata, or perhaps SExp
|
||||
|
||||
replWrap : Core REPLResult -> Core IDEResult
|
||||
replWrap m = pure $ REPL !m
|
||||
|
||||
process : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
IDECommand -> Core REPLResult
|
||||
IDECommand -> Core IDEResult
|
||||
process (Interpret cmd)
|
||||
= interpret cmd
|
||||
= replWrap $ interpret cmd
|
||||
process (LoadFile fname _)
|
||||
= Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
|
||||
= replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
|
||||
process (TypeOf n Nothing)
|
||||
= Idris.REPL.process (Check (PRef replFC (UN n)))
|
||||
= replWrap $ Idris.REPL.process (Check (PRef replFC (UN n)))
|
||||
process (TypeOf n (Just (l, c)))
|
||||
= Idris.REPL.process (Editing (TypeAt (fromInteger l) (fromInteger c) (UN n)))
|
||||
= replWrap $ Idris.REPL.process (Editing (TypeAt (fromInteger l) (fromInteger c) (UN n)))
|
||||
process (CaseSplit l c n)
|
||||
= Idris.REPL.process (Editing (CaseSplit False (fromInteger l) (fromInteger c) (UN n)))
|
||||
= replWrap $ Idris.REPL.process (Editing (CaseSplit False (fromInteger l) (fromInteger c) (UN n)))
|
||||
process (AddClause l n)
|
||||
= Idris.REPL.process (Editing (AddClause False (fromInteger l) (UN n)))
|
||||
= replWrap $ Idris.REPL.process (Editing (AddClause False (fromInteger l) (UN n)))
|
||||
process (AddMissing l n)
|
||||
= do todoCmd "add-missing"
|
||||
pure $ REPL $ Edited $ DisplayEdit []
|
||||
process (ExprSearch l n hs all)
|
||||
= Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n)
|
||||
= replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n)
|
||||
(map UN hs) all))
|
||||
process (GenerateDef l n)
|
||||
= Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n)))
|
||||
= replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n)))
|
||||
process (MakeLemma l n)
|
||||
= Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n)))
|
||||
= replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n)))
|
||||
process (MakeCase l n)
|
||||
= Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN n)))
|
||||
= replWrap $ Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN n)))
|
||||
process (MakeWith l n)
|
||||
= Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN n)))
|
||||
= replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN n)))
|
||||
process (DocsFor n modeOpt)
|
||||
= do todoCmd "docs-for"
|
||||
pure $ REPL $ Printed []
|
||||
process (Apropos n)
|
||||
= do todoCmd "apropros"
|
||||
pure $ REPL $ Printed []
|
||||
process (WhoCalls n)
|
||||
= do todoCmd "who-calls"
|
||||
pure $ NameList []
|
||||
process (CallsWho n)
|
||||
= do todoCmd "calls-who"
|
||||
pure $ NameList []
|
||||
process (BrowseNamespace ns)
|
||||
= do todoCmd "browse-namespace"
|
||||
pure $ NameList []
|
||||
process (NormaliseTerm tm)
|
||||
= do todoCmd "normalise-term"
|
||||
pure $ Term tm
|
||||
process (ShowTermImplicits tm)
|
||||
= do todoCmd "show-term-implicits"
|
||||
pure $ Term tm
|
||||
process (HideTermImplicits tm)
|
||||
= do todoCmd "hide-term-implicits"
|
||||
pure $ Term tm
|
||||
process (ElaborateTerm tm)
|
||||
= do todoCmd "elaborate-term"
|
||||
pure $ TTTerm tm
|
||||
process (PrintDefinition n)
|
||||
= do todoCmd "print-definition"
|
||||
pure $ REPL $ Printed [n]
|
||||
process (ReplCompletions n)
|
||||
= do todoCmd "repl-completions"
|
||||
pure $ NameList []
|
||||
process Version
|
||||
= Idris.REPL.process ShowVersion
|
||||
= replWrap $ Idris.REPL.process ShowVersion
|
||||
process (Metavariables _)
|
||||
= Idris.REPL.process Metavars
|
||||
= replWrap $ Idris.REPL.process Metavars
|
||||
process GetOptions
|
||||
= Idris.REPL.process GetOpts
|
||||
= replWrap $ Idris.REPL.process GetOpts
|
||||
|
||||
processCatch : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
IDECommand -> Core REPLResult
|
||||
IDECommand -> Core IDEResult
|
||||
processCatch cmd
|
||||
= do c' <- branch
|
||||
u' <- get UST
|
||||
@ -175,7 +225,7 @@ processCatch cmd
|
||||
put Syn s'
|
||||
put ROpts o'
|
||||
msg <- perror err
|
||||
pure $ REPLError msg)
|
||||
pure $ REPL $ REPLError msg)
|
||||
|
||||
idePutStrLn : File -> Integer -> String -> Core ()
|
||||
idePutStrLn outf i msg
|
||||
@ -212,41 +262,79 @@ SExpable REPLOpt where
|
||||
|
||||
|
||||
sexpName : Name -> SExp
|
||||
sexpName n = SExpList [ StringAtom (show n), SExpList [], SExpList [] ]
|
||||
sexpName n = SExpList [ StringAtom (show n), SExpList [], SExpList [StringAtom "?", SExpList[]]]
|
||||
|
||||
displayIDEResult : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
File -> Integer -> REPLResult -> Core ()
|
||||
displayIDEResult outf i (REPLError err) = printIDEError outf i err
|
||||
displayIDEResult outf i (Evaluated x Nothing) = printIDEResultWithHighlight outf i $ StringAtom $ show x
|
||||
displayIDEResult outf i (Evaluated x (Just y)) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y
|
||||
displayIDEResult outf i (Printed xs) = printIDEResultWithHighlight outf i $ StringAtom $ showSep "\n" xs
|
||||
displayIDEResult outf i (TermChecked x y) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y
|
||||
displayIDEResult outf i (FileLoaded x) = printIDEResult outf i $ SExpList []
|
||||
displayIDEResult outf i (ErrorLoadingFile x err) = printIDEError outf i $ "Error loading file " ++ x ++ ": " ++ show err
|
||||
displayIDEResult outf i (ErrorsBuildingFile x errs) = printIDEError outf i $ "Error(s) building file " ++ x ++ ": " ++ (showSep "\n" $ map show errs)
|
||||
displayIDEResult outf i NoFileLoaded = printIDEError outf i "No file can be reloaded"
|
||||
displayIDEResult outf i (CurrentDirectory dir) = printIDEResult outf i $ StringAtom $ "Current working directory is '" ++ dir ++ "'"
|
||||
displayIDEResult outf i CompilationFailed = printIDEError outf i "Compilation failed"
|
||||
displayIDEResult outf i (Compiled f) = printIDEResult outf i $ StringAtom $ "File " ++ f ++ " written"
|
||||
displayIDEResult outf i (ProofFound x) = printIDEResult outf i $ StringAtom $ show x
|
||||
--displayIDEResult outf i (Missed cases) = printIDEResult outf i $ showSep "\n" $ map handleMissing cases
|
||||
displayIDEResult outf i (CheckedTotal xs) = printIDEResult outf i $ StringAtom $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
|
||||
displayIDEResult outf i (FoundHoles []) = printIDEResult outf i $ SExpList []
|
||||
displayIDEResult outf i (FoundHoles xs) = printIDEResult outf i $ holesSexp
|
||||
File -> Integer -> IDEResult -> Core ()
|
||||
displayIDEResult outf i (REPL $ REPLError err)
|
||||
= printIDEError outf i err
|
||||
displayIDEResult outf i (REPL RequestedHelp )
|
||||
= printIDEResult outf i
|
||||
$ StringAtom $ displayHelp
|
||||
displayIDEResult outf i (REPL $ Evaluated x Nothing)
|
||||
= printIDEResultWithHighlight outf i
|
||||
$ StringAtom $ show x
|
||||
displayIDEResult outf i (REPL $ Evaluated x (Just y))
|
||||
= printIDEResultWithHighlight outf i
|
||||
$ StringAtom $ show x ++ " : " ++ show y
|
||||
displayIDEResult outf i (REPL $ Printed xs)
|
||||
= printIDEResultWithHighlight outf i
|
||||
$ StringAtom $ showSep "\n" xs
|
||||
displayIDEResult outf i (REPL $ TermChecked x y)
|
||||
= printIDEResultWithHighlight outf i
|
||||
$ StringAtom $ show x ++ " : " ++ show y
|
||||
displayIDEResult outf i (REPL $ FileLoaded x)
|
||||
= printIDEResult outf i $ SExpList []
|
||||
displayIDEResult outf i (REPL $ ErrorLoadingFile x err)
|
||||
= printIDEError outf i
|
||||
$ "Error loading file " ++ x ++ ": " ++ show err
|
||||
displayIDEResult outf i (REPL $ ErrorsBuildingFile x errs)
|
||||
= printIDEError outf i
|
||||
$ "Error(s) building file " ++ x ++ ": " ++
|
||||
(showSep "\n" $ map show errs)
|
||||
displayIDEResult outf i (REPL $ NoFileLoaded)
|
||||
= printIDEError outf i "No file can be reloaded"
|
||||
displayIDEResult outf i (REPL $ CurrentDirectory dir)
|
||||
= printIDEResult outf i
|
||||
$ StringAtom $ "Current working directory is '" ++ dir ++ "'"
|
||||
displayIDEResult outf i (REPL CompilationFailed)
|
||||
= printIDEError outf i "Compilation failed"
|
||||
displayIDEResult outf i (REPL $ Compiled f)
|
||||
= printIDEResult outf i $ StringAtom
|
||||
$ "File " ++ f ++ " written"
|
||||
displayIDEResult outf i (REPL $ ProofFound x)
|
||||
= printIDEResult outf i
|
||||
$ StringAtom $ show x
|
||||
displayIDEResult outf i (REPL $ Missed cases)
|
||||
= printIDEResult outf i
|
||||
$ StringAtom $ showSep "\n"
|
||||
$ map handleMissing cases
|
||||
displayIDEResult outf i (REPL $ CheckedTotal xs)
|
||||
= printIDEResult outf i
|
||||
$ StringAtom $ showSep "\n"
|
||||
$ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
|
||||
displayIDEResult outf i (REPL $ FoundHoles [])
|
||||
= printIDEResult outf i $ SExpList []
|
||||
displayIDEResult outf i (REPL $ FoundHoles xs)
|
||||
= printIDEResult outf i $ holesSexp
|
||||
where
|
||||
holesSexp : SExp
|
||||
holesSexp = SExpList $ map sexpName xs
|
||||
|
||||
displayIDEResult outf i (LogLevelSet k) = printIDEResult outf i $ StringAtom $ "Set loglevel to " ++ show k
|
||||
displayIDEResult outf i (OptionsSet opts) = printIDEResult outf i optionsSexp
|
||||
displayIDEResult outf i (REPL $ LogLevelSet k)
|
||||
= printIDEResult outf i
|
||||
$ StringAtom $ "Set loglevel to " ++ show k
|
||||
displayIDEResult outf i (REPL $ OptionsSet opts)
|
||||
= printIDEResult outf i optionsSexp
|
||||
where
|
||||
optionsSexp : SExp
|
||||
optionsSexp = SExpList $ map toSExp opts
|
||||
displayIDEResult outf i (VersionIs x) = printIDEResult outf i versionSExp
|
||||
displayIDEResult outf i (REPL $ VersionIs x)
|
||||
= printIDEResult outf i versionSExp
|
||||
where
|
||||
semverSexp : SExp
|
||||
semverSexp = case (semVer x) of
|
||||
@ -258,11 +346,19 @@ displayIDEResult outf i (VersionIs x) = printIDEResult outf i versionSExp
|
||||
versionSExp : SExp
|
||||
versionSExp = SExpList [ semverSexp, tagSexp ]
|
||||
|
||||
|
||||
displayIDEResult outf i (Edited (DisplayEdit xs)) = printIDEResult outf i $ StringAtom $ showSep "\n" xs
|
||||
displayIDEResult outf i (Edited (EditError x)) = printIDEError outf i x
|
||||
displayIDEResult outf i (Edited (MadeLemma lit name pty pappstr)) =
|
||||
printIDEResult outf i $ StringAtom $ (relit lit $ show name ++ " : " ++ show pty ++ "\n") ++ pappstr
|
||||
displayIDEResult outf i (REPL $ Edited (DisplayEdit xs))
|
||||
= printIDEResult outf i $ StringAtom $ showSep "\n" xs
|
||||
displayIDEResult outf i (REPL $ Edited (EditError x))
|
||||
= printIDEError outf i x
|
||||
displayIDEResult outf i (REPL $ Edited (MadeLemma lit name pty pappstr))
|
||||
= printIDEResult outf i
|
||||
$ StringAtom $ (relit lit $ show name ++ " : " ++ show pty ++ "\n") ++ pappstr
|
||||
displayIDEResult outf i (NameList ns)
|
||||
= printIDEResult outf i $ SExpList $ map toSExp ns
|
||||
displayIDEResult outf i (Term t)
|
||||
= printIDEResult outf i $ StringAtom t
|
||||
displayIDEResult outf i (TTTerm t)
|
||||
= printIDEResult outf i $ StringAtom t
|
||||
displayIDEResult outf i _ = pure ()
|
||||
|
||||
|
||||
@ -271,8 +367,8 @@ handleIDEResult : {auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
File -> Integer -> REPLResult -> Core ()
|
||||
handleIDEResult outf i Exited = idePutStrLn outf i "Bye for now!"
|
||||
File -> Integer -> IDEResult -> Core ()
|
||||
handleIDEResult outf i (REPL Exited) = idePutStrLn outf i "Bye for now!"
|
||||
handleIDEResult outf i other = displayIDEResult outf i other
|
||||
|
||||
loop : {auto c : Ref Ctxt Defs} ->
|
||||
|
||||
@ -177,16 +177,15 @@ stMain opts
|
||||
setOutput (IDEMode 0 stdin stdout)
|
||||
replIDE {c} {u} {m}
|
||||
else do
|
||||
throw (InternalError "Not implemeted yet")
|
||||
-- let (host, port) = ideSocketModeHostPort opts
|
||||
-- f <- coreLift $ initIDESocketFile host port
|
||||
-- case f of
|
||||
-- Left err => do
|
||||
-- coreLift $ putStrLn err
|
||||
-- coreLift $ exit 1
|
||||
-- Right file => do
|
||||
-- setOutput (IDEMode 0 file file)
|
||||
-- replIDE {c} {u} {m}
|
||||
let (host, port) = ideSocketModeHostPort opts
|
||||
f <- coreLift $ initIDESocketFile host port
|
||||
case f of
|
||||
Left err => do
|
||||
coreLift $ putStrLn err
|
||||
coreLift $ exitWith (ExitFailure 1)
|
||||
Right file => do
|
||||
setOutput (IDEMode 0 file file)
|
||||
replIDE {c} {u} {m}
|
||||
else do
|
||||
repl {c} {u} {m}
|
||||
showTimeRecord
|
||||
|
||||
@ -819,6 +819,7 @@ mutual
|
||||
prompt NormaliseAll = ""
|
||||
prompt Execute = "[exec] "
|
||||
|
||||
export
|
||||
handleMissing : MissedResult -> String
|
||||
handleMissing (CasesMissing x xs) = show x ++ ":\n" ++ showSep "\n" xs
|
||||
handleMissing (CallsNonCovering fn ns) = (show fn ++ ": Calls non covering function"
|
||||
@ -871,6 +872,7 @@ mutual
|
||||
displayResult (OptionsSet opts) = printResult $ showSep "\n" $ map show opts
|
||||
displayResult _ = pure ()
|
||||
|
||||
export
|
||||
displayHelp : String
|
||||
displayHelp =
|
||||
showSep "\n" $ map cmdInfo help
|
||||
|
||||
Loading…
Reference in New Issue
Block a user