149c104 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Desugar do blocks inside of %runTactics

149c104David Raymond Christiansen12 years ago

src/Idris/DSL.hs+1

@@ -76,6 +76,7 @@ expandDo dsl (PDoBlock ds)

76 block b _ = PElabError (Msg "Invalid statement in do block")

78expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

79+expandDo dsl (PRunTactics fc tm) = PRunTactics fc $ expandDo dsl tm

79expandDo dsl t = t

80expandDo dsl t = t

81-- | Replace DSL-bound variable in a term

82-- | Replace DSL-bound variable in a term

src/Idris/ParseExpr.hs+1−1

@@ -498,7 +498,7 @@ runTactics syn = do try (lchar '%' *> reserved "runTactics")

498 fc <- getFC

499 tm <- simpleExpr syn

500 i <- get

501− return $ debindApp syn (desugar syn i (PRunTactics fc tm))

501+ return $ PRunTactics fc tm

502 <?> "new-style tactics expression"

503

504{- | Parses a disambiguation expression