From ddcb4eb664b1c9a43ef759aa865cf7a544cf19ab Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@galois.com>
Date: Fri, 27 Sep 2024 11:44:55 -0700
Subject: [PATCH 1/2] Allow doctests to span multiple lines with a trailing \
 like the REPL already supports

Additionally this allows empty doctest lines to be skipped without error
---
 src/Cryptol/REPL/Command.hs      | 10 +++++++++-
 tests/docstrings/T02.cry         |  3 ++-
 tests/docstrings/T02.icry.stdout |  2 +-
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index 15d180e7c..ab9fed561 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -2062,7 +2062,7 @@ data SubcommandResult = SubcommandResult
 checkBlock ::
   [T.Text] {- ^ lines of the code block -} ->
   REPL [SubcommandResult]
-checkBlock = isolated . go
+checkBlock = isolated . go . continuedLines
   where
     go [] = pure []
     go (line:block) =
@@ -2104,6 +2104,14 @@ checkBlock = isolated . go
               subresults <- checkBlock block
               pure (subresult : subresults)
 
+-- | Combine lines ending in a backslash with the next line.
+continuedLines :: [T.Text] -> [T.Text]
+continuedLines xs =
+  case span ("\\" `T.isSuffixOf`) xs of
+    ([], []) -> []
+    (a, []) -> [foldMap T.init a] -- permissive
+    (a, b:bs) -> T.concat (map T.init a ++ [b]) : continuedLines bs
+
 captureLog :: REPL a -> REPL (String, a)
 captureLog m = do
   previousLogger <- getLogger
diff --git a/tests/docstrings/T02.cry b/tests/docstrings/T02.cry
index d5d3b3566..a387be698 100644
--- a/tests/docstrings/T02.cry
+++ b/tests/docstrings/T02.cry
@@ -31,7 +31,8 @@ submodule F7 = submodule F where
 /**
  ** ```repl
  ** let y = 20
- ** :check f 10 == 20
+ ** :check f 10 \
+ **          == 20
  ** ``` */
 f : Integer -> Integer
 f x = x + x
diff --git a/tests/docstrings/T02.icry.stdout b/tests/docstrings/T02.icry.stdout
index 91cd6c906..67a232eab 100644
--- a/tests/docstrings/T02.icry.stdout
+++ b/tests/docstrings/T02.icry.stdout
@@ -23,7 +23,7 @@ Checking T02::f
 
 let y = 20
 
-:check f 10 == 20
+:check f 10          == 20
 Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.

From 1a341b5b2a81a099296595f494f4a0cf647bb5a7 Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@galois.com>
Date: Fri, 27 Sep 2024 11:50:22 -0700
Subject: [PATCH 2/2] strip leading whitespace from line after trailing \

---
 src/Cryptol/REPL/Command.hs      | 13 ++++++++++---
 tests/docstrings/T02.cry         |  1 +
 tests/docstrings/T02.icry.stdout |  2 +-
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index ab9fed561..fc64c1f3f 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -2065,7 +2065,9 @@ checkBlock ::
 checkBlock = isolated . go . continuedLines
   where
     go [] = pure []
-    go (line:block) =
+    go (line:block)
+      | T.all isSpace line = go block
+      | otherwise =
       case parseCommand (findNbCommand True) (T.unpack line) of
         Nothing -> do
           pure [SubcommandResult
@@ -2109,8 +2111,13 @@ continuedLines :: [T.Text] -> [T.Text]
 continuedLines xs =
   case span ("\\" `T.isSuffixOf`) xs of
     ([], []) -> []
-    (a, []) -> [foldMap T.init a] -- permissive
-    (a, b:bs) -> T.concat (map T.init a ++ [b]) : continuedLines bs
+    (a, []) -> [concat' (map T.init a)] -- permissive
+    (a, b:bs) -> concat' (map T.init a ++ [b]) : continuedLines bs
+  where
+    -- concat that eats leading whitespace between elements
+    concat' [] = T.empty
+    concat' (y:ys) = T.concat (y : map (T.dropWhile isSpace) ys)
+
 
 captureLog :: REPL a -> REPL (String, a)
 captureLog m = do
diff --git a/tests/docstrings/T02.cry b/tests/docstrings/T02.cry
index a387be698..540f79a3f 100644
--- a/tests/docstrings/T02.cry
+++ b/tests/docstrings/T02.cry
@@ -31,6 +31,7 @@ submodule F7 = submodule F where
 /**
  ** ```repl
  ** let y = 20
+ **
  ** :check f 10 \
  **          == 20
  ** ``` */
diff --git a/tests/docstrings/T02.icry.stdout b/tests/docstrings/T02.icry.stdout
index 67a232eab..91cd6c906 100644
--- a/tests/docstrings/T02.icry.stdout
+++ b/tests/docstrings/T02.icry.stdout
@@ -23,7 +23,7 @@ Checking T02::f
 
 let y = 20
 
-:check f 10          == 20
+:check f 10 == 20
 Using exhaustive testing.
 Testing... Passed 1 tests.
 Q.E.D.