cope with different number of :ok return values

src/Idris/IDEMode/REPL.idr

@@ -179,16 +179,20 @@ idePutStrLn outf i msg
     = send outf (SExpList [SymbolAtom "write-string",
                 toSExp msg, toSExp i])
 
-printIDEWithStatus : File -> Integer -> String -> SExp -> Core ()
+returnFromIDE : File -> Integer -> SExp -> Core ()
-printIDEWithStatus outf i status msg
+returnFromIDE outf i msg
-    = do let m = SExpList [SymbolAtom status, toSExp msg]
+    = do send outf (SExpList [SymbolAtom "return", msg, toSExp i])
-         send outf (SExpList [SymbolAtom "return", m, toSExp i])
 
 printIDEResult : File -> Integer -> SExp -> Core ()
-printIDEResult outf i msg = printIDEWithStatus outf i "ok" msg
+printIDEResult outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "ok", toSExp msg])
+
+printIDEResultWithHighlight : File -> Integer -> SExp -> Core ()
+printIDEResultWithHighlight outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "ok", toSExp msg
+                                                                        -- TODO return syntax highlighted result
+                                                                        , SExpList []])
 
 printIDEError : File -> Integer -> String -> Core ()
-printIDEError outf i msg = printIDEWithStatus outf i "error" (toSExp msg)
+printIDEError outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "error", toSExp msg ])
 
 SExpable REPLEval where
   toSExp EvalTC = SymbolAtom "typecheck"
@@ -214,10 +218,10 @@ displayIDEResult : {auto c : Ref Ctxt Defs} ->
        {auto o : Ref ROpts REPLOpts} ->
        File -> Integer -> REPLResult -> Core ()
 displayIDEResult outf i  (REPLError err) = printIDEError outf i err
-displayIDEResult outf i  (Evaluated x Nothing) = printIDEResult outf i $ StringAtom $ show x
+displayIDEResult outf i  (Evaluated x Nothing) = printIDEResultWithHighlight outf i $ StringAtom $ show x
-displayIDEResult outf i  (Evaluated x (Just y)) = printIDEResult outf i $ StringAtom $ show x ++ " : " ++ show y
+displayIDEResult outf i  (Evaluated x (Just y)) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y
-displayIDEResult outf i  (Printed xs) = printIDEResult outf i $ StringAtom $ showSep "\n" xs
+displayIDEResult outf i  (Printed xs) = printIDEResultWithHighlight outf i $ StringAtom $ showSep "\n" xs
-displayIDEResult outf i  (TermChecked x y) = printIDEResult outf i $ StringAtom $ show x ++ " : " ++ show y
+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)

src/Idris/REPLCommon.idr

@@ -32,7 +32,7 @@ printWithStatus status msg
     = do opts <- get ROpts
          case idemode opts of
               REPL _ => coreLift $ putStrLn msg
-              _ => pure ()
+              _      => pure () -- this function should never be called in IDE Mode
 
 export
 printResult : {auto o : Ref ROpts REPLOpts} ->

tests/Main.idr

@@ -92,7 +92,7 @@ chezTests
 
 ideModeTests : List String
 ideModeTests
-  =  [ "ideMode001", "ideMode002" ]
+  =  [ "ideMode001", "ideMode002", "ideMode003" ]
 
 chdir : String -> IO Bool
 chdir dir

tests/ideMode/ideMode003/LocType.idr

@@ -0,0 +1,7 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append [] ys = ys
+append (x :: xs) ys = x :: append xs ys

tests/ideMode/ideMode003/expected

@@ -0,0 +1,27 @@
+000018(:protocol-version 2 0)
+000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
+0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:176} a)")))))) 1)
+0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:176}_[] ?{_:177}_[])")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:177}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:178}_[] ?{_:177}_[])")))))) 1)
+0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:169}_[] ?{_:168}_[])")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:159} : (Main.Vect n[0] a[1])) -> (({arg:160} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)
+0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 31)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 29)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 19)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 17)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 5 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 27)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 25)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 15)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 3 6)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
+000015(:return (:ok ()) 1)
+000037(:return (:ok "Main.Vect : Nat -> Type -> Type" ()) 2)
+Alas the file is done, aborting

tests/ideMode/ideMode003/input

@@ -0,0 +1,2 @@
+00001e((:load-file "LocType.idr") 1)
+((:type-of "Vect") 2)

tests/ideMode/ideMode003/run

@@ -0,0 +1,3 @@
+$1 --ide-mode < input
+
+rm -rf build