Desugar do blocks inside of %runTactics
commit149c1044ab722e66266a313cad93ccae4da78c72
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateFri 20 Feb 2015, 15:58 (12 years ago)
parent2a1de7a
src/Idris/DSL.hs+1
@@ -76,6 +76,7 @@ expandDo dsl (PDoBlock ds)
7676 block b _ = PElabError (Msg "Invalid statement in do block")
7777
7878expandDo 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
7980expandDo dsl t = t
8081
8182-- | Replace DSL-bound variable in a term
src/Idris/ParseExpr.hs+1−1
@@ -498,7 +498,7 @@ runTactics syn = do try (lchar '%' *> reserved "runTactics")
498498 fc <- getFC
499499 tm <- simpleExpr syn
500500 i <- get
501− return $ debindApp syn (desugar syn i (PRunTactics fc tm))
501+ return $ PRunTactics fc tm
502502 <?> "new-style tactics expression"
503503
504504{- | Parses a disambiguation expression