Merge pull request #1259 from mrb/repl_warn_on_unknown_op_for_missing
Warn on unknown operator for missing calls in REPL
commit09dec50c17a8cec6f896168dbc82ec44125dd78a
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 27 May 2014, 07:41 (12 years ago)
parentd10c1e9b65bca2
src/Idris/REPL.hs+1−1
@@ -848,7 +848,7 @@ process h fn (Missing n)
848848 = do i <- getIState
849849 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
850850 case lookupCtxt n (idris_patdefs i) of
851− [] -> return ()
851+ [] -> ihPrintError h $ "Unknown operator " ++ show n
852852 [(_, tms)] ->
853853 iPrintResult (showSep "\n" (map (showTm i') tms))
854854 _ -> iPrintError $ "Ambiguous name"