@@ -653,7 +653,7 @@ elab ist info emode opts fn tm
653653 solve
654654 -- if f is local, just do a simple_app
655655 -- 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)
657657 | pattern && not reflection && not (e_qq ina) && e_nomatching ina
658658 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
659659 | otherwise = implicitApp $
@@ -661,6 +661,7 @@ elab ist info emode opts fn tm
661661 ty <- goal
662662 fty <- get_type (Var f)
663663 ctxt <- get_context
664+ annot <- findHighlight f
664665 let args = insertScopedImps fc (normalise ctxt env fty) args_in
665666 let unmatchableArgs = if pattern
666667 then getUnmatchable (tt_ctxt ist) f
@@ -671,11 +672,12 @@ elab ist info emode opts fn tm
671672 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
672673 if (f `elem` map fst env && length args == 1 && length args_in == 1)
673674 then -- simple app, as below
674− do simple_app False
675+ do simple_app False
675676 (elabE (ina { e_isfn = True }) (Just fc) (PRef fc f))
676677 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
677678 (show tm)
678679 solve
680+ highlightSource ffc annot
679681 return []
680682 else
681683 do ivs <- get_instances
@@ -703,7 +705,7 @@ elab ist info emode opts fn tm
703705 sortBy cmpArg (zip ns args)
704706 ulog <- getUnifyLog
705707 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
706− [] fc False f
708+ [] fc False f
707709 (zip ns' (unmatchableArgs ++ repeat False))
708710 (f == sUN "Force")
709711 (map (\x -> getTm x) eargs) -- TODO: remove this False arg