2cb780a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3869 from mheinzel/master

Fixing behavior of addMissing (interactively adding missing clauses)

commit2cb780ab55dd253f11199f2f0e47cfbc43062d19 authorNiklas Larsson <metaniklas@gmail.com> dateTue 20 Jun 2017, 19:35 (9 years ago) parent180fc75 b9bad2d

10 files changed+52−8

compare with master

unifiedsplit

src/Idris/Interactive.hs+5−7 test/TestData.hs+3−1 test/interactive015/expected+6 test/interactive015/input+2 test/interactive015/run+8 test/interactive015/src/interactive015.idr+4 test/interactive016/expected+7 test/interactive016/input+2 test/interactive016/run+8 test/interactive016/src/interactive016.idr+7

src/Idris/Interactive.hs+5−7

@@ -111,7 +111,7 @@ addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()

111111addMissing fn updatefile l n

112112 = do src <- runIO $ readSource fn

113113 let (before, tyline : later) = splitAt (l-1) (lines src)

114− let indent = getIndent 0 (show n) tyline

114+ let indent = getIndent tyline

115115 i <- getIState

116116 cl <- getInternalApp fn l

117117 let n' = getAppName cl

@@ -124,9 +124,9 @@ addMissing fn updatefile l n

124124 if updatefile

125125 then do let fb = fn ++ "~"

126126 runIO $ writeSource fb (unlines (before ++ nonblank)

127− ++ extras ++

128− (if null extras then ""

129− else "\n" ++ unlines rest))

127+ ++ extras

128+ ++ (if null extras then "" else "\n")

129+ ++ unlines rest)

130130 runIO $ copyFile fb fn

131131 else iPrintResult extras

132132 where showPat = show . stripNS

@@ -155,9 +155,7 @@ addMissing fn updatefile l n

155155 "\n" ++ rest))

156156 showNew nm i _ [] = return ""

157157

158− getIndent i n [] = 0

159− getIndent i n xs | take (length n) xs == n = i

160− getIndent i n (x : xs) = getIndent (i + 1) n xs

158+ getIndent s = length (takeWhile isSpace s)

161159

162160

163161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

test/TestData.hs+3−1

@@ -155,7 +155,9 @@ testFamiliesData = [

155155 ( 11, ANY ),

156156 ( 12, ANY ),

157157 ( 13, ANY ),

158− ( 14, C_CG )]),

158+ ( 14, C_CG ),

159+ ( 15, ANY ),

160+ ( 16, ANY )]),

159161 ("interfaces", "Interfaces",

160162 [ ( 1, ANY ),

161163 ( 2, ANY ),

test/interactive015/expectednew file+6

@@ -0,0 +1,6 @@

1+test (Just x) = ?Nothing_rhs_1

3+test : Maybe a -> Bool

4+test Nothing = False

5+test (Just x) = ?Nothing_rhs_1

test/interactive015/inputnew file+2

@@ -0,0 +1,2 @@

1+:addmissing 3 Nothing

2+:addmissing! 3 Nothing

test/interactive015/runnew file+8

@@ -0,0 +1,8 @@

1+#!/usr/bin/env bash

3+cp src/interactive015.idr .

4+${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input

6+cat interactive015.idr

8+rm -f *.ibc interactive015.idr

test/interactive015/src/interactive015.idrnew file+4

@@ -0,0 +1,4 @@

2+test : Maybe a -> Bool

3+test Nothing = False

test/interactive016/expectednew file+7

@@ -0,0 +1,7 @@

2+test : Maybe a -> Bool

3+test Nothing = False

4+test (Just x) = True

6+other : Int

7+other = 3

test/interactive016/inputnew file+2

@@ -0,0 +1,2 @@

1+:addmissing 3 Nothing

2+:addmissing! 3 Nothing

test/interactive016/runnew file+8

@@ -0,0 +1,8 @@

1+#!/usr/bin/env bash

3+cp src/interactive016.idr .

4+${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input

6+cat interactive016.idr

8+rm -f *.ibc interactive016.idr

test/interactive016/src/interactive016.idrnew file+7

@@ -0,0 +1,7 @@

2+test : Maybe a -> Bool

3+test Nothing = False

4+test (Just x) = True

6+other : Int

7+other = 3