Require repl and convert \r\n to \n in lexer

cryptol-remote-api/src/CryptolServer/FocusedModule.hs

@@ -11,7 +11,6 @@ import Data.Aeson as JSON
 
 import Cryptol.ModuleSystem (meFocusedModule, meLoadedModules)
 import Cryptol.ModuleSystem.Env (isLoadedParamMod)
-import qualified Cryptol.TypeCheck.AST as T
 import Cryptol.Utils.PP
 
 import CryptolServer

src/Cryptol/Parser/LexerUtils.hs

@@ -342,7 +342,10 @@ alexGetByte i =
   do (c,rest) <- T.uncons (input i)
      let i' = i { alexPos = move (alexPos i) c, input = rest }
          b  = byteForChar c
-     return (b,i')
+     -- treat \r\n as \n
+     case (b, alexGetByte i') of
+       (13, skip@(Just (10, _))) -> skip
+       _ -> pure (b, i')
 
 data Layout = Layout | NoLayout
 

src/Cryptol/REPL/Command.hs

@@ -2012,7 +2012,7 @@ extractCodeBlocks raw = go [] cleanLines
     go finished (x:xs)
       | (ticks, lang) <- T.span ('`' ==) x
       , 3 <= T.length ticks
-      = if lang `elem` ["", "repl"]
+      = if lang == "repl"
         then keep finished ticks [] xs
         else skip finished ticks xs
       | otherwise = go finished xs

tests/docstrings/T01.cry

@@ -3,14 +3,14 @@ module T01 where
 submodule Sub where
   /**
    * This verifies that pp shadows the outer definition
-   * ```
+   * ```repl
    * :check pp
    * ```
    */
   pp = True
 
 /**
- * ```
+ * ```repl
  * :check ~ pp
  * ```
  */

tests/docstrings/T02.cry

@@ -11,17 +11,18 @@ submodule F where
     c = 1
 
   /**
-   * ```
+   * Longer code block delimiters are supported
+   * ````repl
    * :exhaust p
-   * ```
+   * ````
    */
   p x = c + x == x + c
 
 submodule F7 = submodule F where
   type n = 7
 
 /**
- * ```
+ * ```repl
  * let y = 20
  * :check f 10 == 20
  * ```

tests/docstrings/T04.cry

@@ -6,6 +6,11 @@ module T03 where
  * ```repl
  * :load AFile.cry
  * ```
+ *
+ * Stuff not marked repl is ignored
+ * ```
+ * garbage
+ * ```
  */
 a : Bit
 a = True