@@ -653,7 +653,7 @@ elab ist info emode opts fn tm
654 -- if f is local, just do a simple_app
654 -- if f is local, just do a simple_app
655 -- FIXME: Anyone feel like refactoring this mess? - EB
655 -- FIXME: Anyone feel like refactoring this mess? - EB
656− elab' ina topfc tm@(PApp fc (PRef _ f) args_in)
656+ elab' ina topfc tm@(PApp fc (PRef ffc f) args_in)
657 | pattern && not reflection && not (e_qq ina) && e_nomatching ina
657 | pattern && not reflection && not (e_qq ina) && e_nomatching ina
658 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
658 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
659 | otherwise = implicitApp $
659 | otherwise = implicitApp $
@@ -661,6 +661,7 @@ elab ist info emode opts fn tm
661 ty <- goal
661 ty <- goal
662 fty <- get_type (Var f)
662 fty <- get_type (Var f)
663 ctxt <- get_context
663 ctxt <- get_context
664+ annot <- findHighlight f
664 let args = insertScopedImps fc (normalise ctxt env fty) args_in
665 let args = insertScopedImps fc (normalise ctxt env fty) args_in
665 let unmatchableArgs = if pattern
666 let unmatchableArgs = if pattern
666 then getUnmatchable (tt_ctxt ist) f
667 then getUnmatchable (tt_ctxt ist) f
@@ -671,11 +672,12 @@ elab ist info emode opts fn tm
671 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
672 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
672 if (f `elem` map fst env && length args == 1 && length args_in == 1)
673 if (f `elem` map fst env && length args == 1 && length args_in == 1)
673 then -- simple app, as below
674 then -- simple app, as below
674− do simple_app False
675+ do simple_app False
675 (elabE (ina { e_isfn = True }) (Just fc) (PRef fc f))
676 (elabE (ina { e_isfn = True }) (Just fc) (PRef fc f))
676 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
677 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
677 (show tm)
678 (show tm)
680+ highlightSource ffc annot
679 return []
681 return []
681 do ivs <- get_instances
683 do ivs <- get_instances
@@ -703,7 +705,7 @@ elab ist info emode opts fn tm
703 sortBy cmpArg (zip ns args)
705 sortBy cmpArg (zip ns args)
704 ulog <- getUnifyLog
706 ulog <- getUnifyLog
705 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
707 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
706− [] fc False f
708+ [] fc False f
707 (zip ns' (unmatchableArgs ++ repeat False))
709 (zip ns' (unmatchableArgs ++ repeat False))
708 (f == sUN "Force")
710 (f == sUN "Force")
709 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
711 (map (\x -> getTm x) eargs) -- TODO: remove this False arg