edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-28 14:06:26 +03:00
Code Issues Projects Releases Wiki Activity

handle more commands in IDE mode

Browse Source
This commit is contained in:
Arnaud Bailly 2019-10-13 19:49:44 +02:00
parent ed27d32392
commit 85e6e9ca7a
4 changed files with 22 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/Idris/IDEMode/Commands.idr
View File

@ -25,7 +25,9 @@ data IDECommand
| MakeLemma Integer String | MakeLemma Integer String
| MakeCase Integer String | MakeCase Integer String
| MakeWith Integer String | MakeWith Integer String
| Metavariables Integer
| Version | Version
| GetOptions
readHints : List SExp -> Maybe (List String) readHints : List SExp -> Maybe (List String)
readHints [] = Just [] readHints [] = Just []
@ -75,7 +77,10 @@ getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n])
= Just $ MakeCase l n = Just $ MakeCase l n
getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n]) getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])
= Just $ MakeWith l n = Just $ MakeWith l n
getIDECommand (SExpList [SymbolAtom "metavariables", IntegerAtom n])
= Just $ Metavariables n
getIDECommand (SymbolAtom "version") = Just Version getIDECommand (SymbolAtom "version") = Just Version
getIDECommand (SExpList [SymbolAtom "get-options"]) = Just GetOptions
getIDECommand _ = Nothing getIDECommand _ = Nothing
export export
@ -96,6 +101,8 @@ putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate-
putIDECommand (MakeLemma line n) = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n]) 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 (MakeCase line n) = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n]) putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
putIDECommand (Metavariables n) = (SExpList [SymbolAtom "metavariables", IntegerAtom n])
putIDECommand GetOptions = (SExpList [SymbolAtom "get-options"])
putIDECommand Version = SymbolAtom "version" putIDECommand Version = SymbolAtom "version"
export export

6
src/Idris/IDEMode/REPL.idr
View File

@ -189,6 +189,12 @@ process (MakeWith l n)
process Version process Version
= do Idris.REPL.process ShowVersion = do Idris.REPL.process ShowVersion
pure () pure ()
process (Metavariables _)
= do Idris.REPL.process Metavars
pure ()
process GetOptions
= do printResult ""
pure ()
processCatch : {auto c : Ref Ctxt Defs} -> processCatch : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->

20
src/Idris/REPLCommon.idr
View File

@ -22,9 +22,9 @@ iputStrLn msg
REPL False => coreLift $ putStrLn msg REPL False => coreLift $ putStrLn msg
REPL _ => pure () REPL _ => pure ()
IDEMode i _ f => IDEMode i _ f =>
send f (SExpList [SymbolAtom "write-string", send f (SExpList [SymbolAtom "write-string",
toSExp msg, toSExp i]) toSExp msg, toSExp i])
printWithStatus : {auto o : Ref ROpts REPLOpts} -> printWithStatus : {auto o : Ref ROpts REPLOpts} ->
String -> String -> Core () String -> String -> Core ()
@ -33,9 +33,7 @@ printWithStatus status msg
case idemode opts of case idemode opts of
REPL _ => coreLift $ putStrLn msg REPL _ => coreLift $ putStrLn msg
IDEMode i _ f => IDEMode i _ f =>
do let m = SExpList [SymbolAtom status, toSExp msg, do let m = SExpList [SymbolAtom status, toSExp msg ]
-- highlighting; currently blank
SExpList []]
send f (SExpList [SymbolAtom "return", m, toSExp i]) send f (SExpList [SymbolAtom "return", m, toSExp i])
export export
@ -58,7 +56,7 @@ emitError : {auto c : Ref Ctxt Defs} ->
emitError err emitError err
= do opts <- get ROpts = do opts <- get ROpts
case idemode opts of case idemode opts of
REPL _ => REPL _ =>
do msg <- display err do msg <- display err
coreLift $ putStrLn msg coreLift $ putStrLn msg
IDEMode i _ f => IDEMode i _ f =>
@ -66,10 +64,10 @@ emitError err
case getErrorLoc err of case getErrorLoc err of
Nothing => iputStrLn msg Nothing => iputStrLn msg
Just fc => Just fc =>
send f (SExpList [SymbolAtom "warning", send f (SExpList [SymbolAtom "warning",
SExpList [toSExp (file fc), SExpList [toSExp (file fc),
toSExp (addOne (startPos fc)), toSExp (addOne (startPos fc)),
toSExp (addOne (endPos fc)), toSExp (addOne (endPos fc)),
toSExp msg, toSExp msg,
-- highlighting; currently blank -- highlighting; currently blank
SExpList []], SExpList []],
@ -104,5 +102,3 @@ resetContext
put UST initUState put UST initUState
put Syn initSyntax put Syn initSyntax
put MD initMetadata put MD initMetadata

2
tests/ideMode/ideMode001/expected
View File

@ -1,4 +1,4 @@
000018(:protocol-version 2 0) 000018(:protocol-version 2 0)
000038(:write-string "1/1: Building LocType (LocType.idr)" 1) 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
00002a(:return (:ok "Loaded LocType.idr" ()) 1) 000027(:return (:ok "Loaded LocType.idr") 1)
Alas the file is done, aborting Alas the file is done, aborting