[ repl ] better printing of holes

* Fixed printing in the IDEMode (& include highlighting)
* Now also print the type of the holes

Author: gallais

src/Idris/IDEMode/REPL.idr

@@ -30,7 +30,6 @@ import Idris.Resugar
 import Idris.REPL
 import Idris.Syntax
 import Idris.Version
-import Idris.Pretty
 import Idris.Doc.String
 
 import Idris.IDEMode.Commands
@@ -385,7 +384,17 @@ displayIDEResult outf i  (REPL $ CheckedTotal xs)
   $ StringAtom $ showSep "\n"
   $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
 displayIDEResult outf i  (REPL $ FoundHoles holes)
-  = printIDEResult outf i $ SExpList $ map sexpHole holes
+  = printIDEResultWithHighlight outf i =<< case holes of
+      []  => pure (StringAtom "No holes", [])
+      [x] => do let hole = pretty x.name <++> colon <++> prettyTerm x.type
+                hlght <- renderWithDecorations syntaxToProperties
+                           $ "1 hole" <+> colon <++> hole
+                pure $ mapFst StringAtom hlght
+      xs => do let holes = xs <&> \ x => pretty x.name <++> colon <++> prettyTerm x.type
+               let header = pretty (length xs) <++> pretty "holes" <+> colon
+               hlght <- renderWithDecorations syntaxToProperties
+                           $ vcat (header :: map (indent 2) holes)
+               pure $ mapFst StringAtom hlght
 displayIDEResult outf i  (REPL $ LogLevelSet k)
   = printIDEResult outf i
   $ StringAtom $ "Set loglevel to " ++ show k

src/Idris/REPL.idr

@@ -1093,10 +1093,13 @@ mutual
   displayResult (Missed cases) = printResult $ vsep (handleMissing <$> cases)
   displayResult (CheckedTotal xs) = printResult (vsep (map (\(fn, tot) => pretty fn <++> pretty "is" <++> pretty tot) xs))
   displayResult (FoundHoles []) = printResult (reflow "No holes")
-  displayResult (FoundHoles [x]) = printResult (reflow "1 hole" <+> colon <++> pretty x.name)
+  displayResult (FoundHoles [x]) = do
+     let hole = pretty x.name <++> colon <++> prettyTerm x.type
+     printResult (reflow "1 hole" <+> colon <++> hole)
   displayResult (FoundHoles xs) = do
-    let holes = concatWith (surround (pretty ", ")) (pretty . name <$> xs)
-    printResult (pretty (length xs) <++> pretty "holes" <+> colon <++> holes)
+    let header = pretty (length xs) <++> pretty "holes" <+> colon
+    let holes  = xs <&> \ x => pretty x.name <++> colon <++> prettyTerm x.type
+    printResult $ vcat (header :: map (indent 2) holes)
   displayResult (LogLevelSet Nothing) = printResult (reflow "Logging turned off")
   displayResult (LogLevelSet (Just k)) = printResult (reflow "Set log level to" <++> pretty k)
   displayResult (ConsoleWidthSet (Just k)) = printResult (reflow "Set consolewidth to" <++> pretty k)

tests/Main.idr

@@ -86,7 +86,8 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
        "interactive021", "interactive022", "interactive023", "interactive024",
        "interactive025", "interactive026", "interactive027", "interactive028",
        "interactive029", "interactive030", "interactive031", "interactive032",
-       "interactive033", "interactive034", "interactive035", "interactive036"]
+       "interactive033", "interactive034", "interactive035", "interactive036",
+       "interactive037"]
 
 idrisTestsInterface : TestPool
 idrisTestsInterface = MkTestPool "Interface" [] Nothing

tests/idris2/basic049/expected

@@ -55,5 +55,5 @@ Fld:72:26--72:29
 Main> Main.myDog : OrdinaryDog
 Main> Main.mySuperDog : SuperDog
 Main> Main.other : Other String
-Main> 1 hole: Main.r2_shouldNotTypecheck1
+Main> 1 hole: Main.r2_shouldNotTypecheck1 : ?_ [no locals in scope]
 Main> Bye for now!

tests/idris2/import003/expected

@@ -1,7 +1,7 @@
 1/2: Building A (A.idr)
 2/2: Building B (B.idr)
-B> 1 hole: A.defA
+B> 1 hole: A.defA : Int -> Int
 B> Bye for now!
 2/2: Building C (C.idr)
-C> 1 hole: C.newHole
+C> 1 hole: C.newHole : Int -> Int
 C> Bye for now!

tests/idris2/interactive037/Holes.idr

@@ -0,0 +1,10 @@
+module Holes
+
+int : Int
+int = ?a
+
+nat : Nat
+nat = ?b
+
+equal : cast Holes.int === Holes.nat
+equal = ?c

tests/idris2/interactive037/expected

@@ -0,0 +1,6 @@
+1/1: Building Holes (Holes.idr)
+Holes> 3 holes:
+  Holes.a : Int
+  Holes.b : Nat
+  Holes.c : integerToNat (prim__cast_IntInteger ?a) = ?b
+Holes> Bye for now!

tests/idris2/interactive037/input

@@ -0,0 +1,2 @@
+:m
+:q

tests/idris2/interactive037/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner Holes.idr < input

tests/idris2/perror010/expected

@@ -35,6 +35,6 @@ TrailingLam:3:9--3:22
  3 | f k = f \n => k (S n)
              ^^^^^^^^^^^^^
 
-Main> 1 hole: Main.a
+Main> 1 hole: Main.a : Nat -> Nat
 Main> 
 Bye for now!