From 17fec60d7a057304af3bcef58c929bbd9cd60d09 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 27 Jun 2020 21:09:03 +0100 Subject: [PATCH] Add new clause at next blank line This fixes a thing that's been annoying me in the vim mode. It's usually something that's left to the editor, but we do all the work for the vim mode! (This is hard to test conveniently, sorry...) --- src/Idris/REPL.idr | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index f1d368323..684e1a8b0 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -234,7 +234,11 @@ rtrim : String -> String rtrim str = reverse (ltrim (reverse str)) addClause : String -> Nat -> List String -> List String -addClause c Z xs = rtrim c :: xs +addClause c Z [] = rtrim c :: [] +addClause c Z (x :: xs) + = if all isSpace (unpack x) + then rtrim c :: x :: xs + else x :: addClause c Z xs addClause c (S k) (x :: xs) = x :: addClause c k xs addClause c (S k) [] = [c]