Transmit hole information in the IDEMode protocol

Move printing routines into the `Idris.IDEMode.Holes` module

src/Idris/IDEMode/Holes.idr

@@ -5,6 +5,8 @@ import Core.Env
 import Idris.Resugar
 import Idris.Syntax
 
+import Idris.IDEMode.Commands
+
 public export
 record HolePremise where
   constructor MkHolePremise
@@ -118,11 +120,27 @@ showHole defs env fn args ty
          case hdata.context of
            [] => pure $ show (hdata.name) ++ " : " ++ show hdata.type
            _  => pure $ concat 
-              (map (\hole => showCount hole.multiplicity
-                             ++ (impBracket hole.isImplicit $
-                                 tidy hole.name ++ " : " ++ (show hole.type) ++ "\n" )
+              (map (\premise => showCount premise.multiplicity
+                             ++ (impBracket premise.isImplicit $
+                                 tidy premise.name ++ " : " ++ (show premise.type) ++ "\n" )
                    ) hdata.context)
               ++ "-------------------------------------\n"
               ++ nameRoot (hdata.name) ++ " : " ++ show hdata.type
 
+sexpPremise : HolePremise -> SExp
+sexpPremise premise = 
+  SExpList [StringAtom $ showCount premise.multiplicity 
+                       ++ (impBracket premise.isImplicit $
+                           tidy premise.name)
+           ,StringAtom $ show premise.type
+           ,SExpList [] -- TODO: metadata
+           ]
 
+export
+sexpHole : HoleData -> SExp
+sexpHole hole = SExpList 
+  [ StringAtom (show  hole.name)
+  , SExpList $ map sexpPremise hole.context  -- Premises
+  , SExpList [ StringAtom $ show hole.type   -- Conclusion
+             , SExpList[]]    -- TODO: Highlighting information
+  ]

src/Idris/IDEMode/REPL.idr

@@ -314,25 +314,8 @@ 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
-    sexpName : 
-      HoleData -> Core SExp
-    sexpName n = do
-      pure $ SExpList 
-        [ StringAtom (show  n.name)
-        , SExpList []  -- Premises
-        , SExpList [ StringAtom "?"   -- Conclusion
-                   , SExpList[]]    -- TODO: Highlighting information
-        ]
-  
-    holesSexp : Core SExp
-    holesSexp = pure $ SExpList !( traverse sexpName xs )
-
-
+displayIDEResult outf i  (REPL $ FoundHoles holes) 
+  = printIDEResult outf i $ SExpList $ map sexpHole holes
 displayIDEResult outf i  (REPL $ LogLevelSet k) 
   = printIDEResult outf i 
   $ StringAtom $ "Set loglevel to " ++ show k

src/Idris/REPL.idr

@@ -77,9 +77,6 @@ showInfo (n, idx, d)
                 coreLift $ putStrLn $
                         "Size change: " ++ showSep ", " scinfo
 
-
--- Put the printing of holes back here
-
 displayType : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Defs -> (Name, Int, GlobalDef) ->