@@ -299,8 +299,17 @@ process fn (RmProof n')
299 let ms = idris_metavars i
299 let ms = idris_metavars i
300 putIState $ i { idris_metavars = n : ms }
300 putIState $ i { idris_metavars = n : ms }
302−process fn (AddProof prf)
302+process fn' (AddProof prf)
304+ ex <- liftIO $ doesFileExist fn'
305+ let fnExt = fn' <.> "idr"
306+ exExt <- liftIO $ doesFileExist fnExt
311+ else fail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
303− = do let fb = fn ++ "~"
312+ let fb = fn ++ "~"
304 liftIO $ copyFile fn fb -- make a backup in case something goes wrong!
313 liftIO $ copyFile fn fb -- make a backup in case something goes wrong!
305 prog <- liftIO $ readFile fb
314 prog <- liftIO $ readFile fb
306 i <- getIState
315 i <- getIState