6412ae4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Implement type-of ideslave command, which uses Check in the background

Furthermore, instead of printing with iputStrLn, use iPrintResult to indicate that the command finished successfully

commit6412ae453d4d12312e89511dd6cfcb5d5f394a22 authorHannes Mehnert <hannes@mehnert.org> dateMon 18 Nov 2013, 19:05 (13 years ago) parent98e8963

2 files changed+20−15

compare with master

unifiedsplit

src/Idris/IdeSlave.hs+2 src/Idris/REPL.hs+18−15

src/Idris/IdeSlave.hs+2

@@ -93,6 +93,7 @@ parseSExp = parse pSExp "(unknown)"

9393

9494data IdeSlaveCommand = REPLCompletions String

9595 | Interpret String

96+ | TypeOf String

9697 | LoadFile String

9798 deriving Show

9899

@@ -101,6 +102,7 @@ sexpToCommand (SexpList (x:[])) = se

101102sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

102103sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

103104sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

105+sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

104106sexpToCommand _ = Nothing

105107

106108parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/REPL.hs+18−15

@@ -233,6 +233,8 @@ ideslave orig mods

233233 Nothing -> iPrintResult $ "loaded " ++ filename

234234 Just x -> iPrintError $ "didn't load " ++ filename

235235 ideslave orig [filename]

236+ Just (TypeOf name) ->

237+ process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))

236238 Nothing -> do iPrintError "did not understand")

237239 (\e -> do iPrintError $ show e)

238240 ideslave orig mods

@@ -435,10 +437,10 @@ process h fn (Check (PRef _ n))

435437 case lookupNames n ctxt of

436438 ts@(t:_) ->

437439 case lookup t (idris_metavars ist) of

438− Just (_, i) -> showMetavarInfo c imp ist n i

439− Nothing -> do mapM_ (\n -> ihputStrLn h $ showName (Just ist) [] False c n ++ " : " ++

440− showImp (Just ist) imp c (delabTy ist n)) ts

441− ihPrintResult h ""

440+ Just (_, i) -> ihPrintResult h (showMetavarInfo c imp ist n i)

441+ Nothing -> ihPrintResult h $

442+ concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++

443+ showImp (Just ist) imp c (delabTy ist n)) $ ts

442444 [] -> ihPrintError h $ "No such variable " ++ show n

443445 where

444446 showMetavarInfo c imp ist n i

@@ -446,18 +448,19 @@ process h fn (Check (PRef _ n))

446448 (ty:_) -> putTy c imp ist i (delab ist ty)

447449 putTy c imp ist 0 sc = putGoal c imp ist sc

448450 putTy c imp ist i (PPi _ n t sc)

449− = do ihputStrLn h $ " " ++

450− (case n of

451− MN _ _ -> "_"

452− UN ('_':'_':_) -> "_"

453− _ -> showName (Just ist) [] False c n) ++

454− " : " ++ showImp (Just ist) imp c t

455− putTy c imp ist (i-1) sc

451+ = let current = " " ++

452+ (case n of

453+ MN _ _ -> "_"

454+ UN ('_':'_':_) -> "_"

455+ _ -> showName (Just ist) [] False c n) ++

456+ " : " ++ showImp (Just ist) imp c t

457+ in

458+ current ++ putTy c imp ist (i-1) sc

456459 putTy c imp ist _ sc = putGoal c imp ist sc

457460 putGoal c imp ist g

458− = do ihputStrLn h $ "--------------------------------------"

459− ihputStrLn h $ showName (Just ist) [] False c n ++ " : "

460− ++ showImp (Just ist) imp c g

461+ = "--------------------------------------\n" ++

462+ showName (Just ist) [] False c n ++ " : " ++

463+ showImp (Just ist) imp c g

461464

462465

463466process h fn (Check t)

@@ -470,7 +473,7 @@ process h fn (Check t)

470473 case tm of

471474 TType _ -> ihPrintResult h ("Type : Type 1")

472475 _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

473− showImp (Just ist) imp c (delab ist ty))

476+ showImp (Just ist) imp c (delab ist ty))

474477

475478process h fn (DocStr n)

476479 = do i <- getIState