git.iko.soy/Idris-dev
on master help sign in
Rename function to better reflect purpose
fbbe433David Raymond Christiansen
src/Idris/Elab/Term.hs+6−6
compare with master
unifiedsplit
@@ -1145,7 +1145,7 @@ elab ist info emode opts fn tm
1145 focus n
1145 focus n
1146 elab' ina (Just fc') tm
1146 elab' ina (Just fc') tm
1147 env <- get_env
1147 env <- get_env
1148− runTactical ist (maybe fc' id fc) env (P Bound n' Erased) ns
1148+ runElabAction ist (maybe fc' id fc) env (P Bound n' Erased) ns
1149 solve
1149 solve
1150 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
1150 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
1151
1151
@@ -1698,9 +1698,9 @@ metavarName _ n@(NS _ _) = n
1698metavarName (Just (ns@(_:_))) n = sNS n ns
1698metavarName (Just (ns@(_:_))) n = sNS n ns
1699metavarName _ n = n
1699metavarName _ n = n
1700
1700
1701−runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
1701+runElabAction :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
1702−runTactical ist fc env tm ns = do tm' <- eval tm
1702+runElabAction ist fc env tm ns = do tm' <- eval tm
1703− runTacTm tm'
1703+ runTacTm tm'
1704
1704
1705 where
1705 where
1706 eval tm = do ctxt <- get_context
1706 eval tm = do ctxt <- get_context
@@ -1965,8 +1965,8 @@ runTactical ist fc env tm ns = do tm' <- eval tm
1965 datatypes <- get_datatypes
1965 datatypes <- get_datatypes
1966 env <- get_env
1966 env <- get_env
1967 (_, ES (p, aux') _ _) <-
1967 (_, ES (p, aux') _ _) <-
1968− lift $ runElab aux (runTactical ist fc [] script ns)
1968+ lift $ runElab aux (runElabAction ist fc [] script ns)
1969− (newProof recH ctxt datatypes goalTT)
1969+ (newProof recH ctxt datatypes goalTT)
1970 let tm_out = getProofTerm (pterm p)
1970 let tm_out = getProofTerm (pterm p)
1971 updateAux $ const aux'
1971 updateAux $ const aux'
1972 env' <- get_env
1972 env' <- get_env
src/Idris/Prover.hs+2−2
@@ -335,7 +335,7 @@ elabloop fn d prompt prf e prev h env
335 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
335 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
336 (_, e') <- elabStep e saveState -- enable :undo
336 (_, e') <- elabStep e saveState -- enable :undo
337 (res, e'') <- elabStep e' $
337 (res, e'') <- elabStep e' $
338− runTactical ist NoFC [] tm ["Shell"]
338+ runElabAction ist NoFC [] tm ["Shell"]
339 ctxt <- getContext
339 ctxt <- getContext
340 (v, vty) <- tclift $ check ctxt [] (forget res)
340 (v, vty) <- tclift $ check ctxt [] (forget res)
341 let v' = normaliseAll ctxt [] v
341 let v' = normaliseAll ctxt [] v
@@ -346,7 +346,7 @@ elabloop fn d prompt prf e prev h env
346 -- TODO: call elaborator with Elab () as goal here
346 -- TODO: call elaborator with Elab () as goal here
347 (_, e') <- elabStep e saveState -- enable :undo
347 (_, e') <- elabStep e saveState -- enable :undo
348 (_, e'') <- elabStep e' $
348 (_, e'') <- elabStep e' $
349− runTactical ist NoFC [] tm ["Shell"]
349+ runElabAction ist NoFC [] tm ["Shell"]
350 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
350 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
351 (\err -> return (False, prev, e, False, prf, env, Left err))
351 (\err -> return (False, prev, e, False, prf, env, Left err))
352 idemodePutSExp "write-proof-state" (prf', length prf')
352 idemodePutSExp "write-proof-state" (prf', length prf')