da25e42 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak proof search metavariable update

commitda25e42e71a4a273cec700bfc1e1eb5f533c0a33 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 22 Jan 2014, 14:52 (13 years ago) parent1fe537f

2 files changed+1−4

unifiedsplit

libs/neweffects/Effects.idr−3

@@ -253,9 +253,6 @@ runEnv env prog = eff env prog (\r, env => pure (r ** env))

253253runPure : Env id xs -> Eff id a xs xs' -> a

254254runPure env prog = eff env prog (\r, env => r)

255255

256−-- runPureEnv : Env id xs -> Eff id a xs xs' -> (x : a ** Env id (xs' x))

257−-- runPureEnv env prog = eff env prog (%unifyLog (\r, env => id (r ** env)))

258−

259256runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a

260257runWith inj env prog = eff env prog (\r, env => inj r)

261258

src/Idris/REPL.hs+1−1

@@ -744,7 +744,7 @@ process h fn (DoProofSearch updatefile l n hints)

744744 | length cs >= length n

745745 = case splitAt (length n) cs of

746746 (mv, c:cs) ->

747− if (isSpace c && mv == n)

747+ if ((isSpace c || c == ')' || c == '}') && mv == n)

748748 then addBracket brack new ++ (c : cs)

749749 else '?' : mv ++ c : updateMeta True cs n new

750750 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv