@@ -238,7 +238,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)
238238 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))
239239 (ProofSearch rec False depth t psnames hints)]
240240 let def = PClause fc mn (PRef fc [] mn) [] (body top) []
241− newmv <- idrisCatch
241+ newmv_pre <- idrisCatch
242242 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])
243243 (tm, ty) <- elabVal recinfo ERHS (PRef fc [] mn)
244244 ctxt <- getContext
@@ -249,10 +249,11 @@ doProofSearch fn updatefile rec l n hints (Just depth)
249249 (dropCtxt envlen
250250 (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))
251251 (\e -> return ("?" ++ show n))
252+ let newmv = guessBrackets False tyline (show n) newmv_pre
252253 if updatefile then
253254 do let fb = fn ++ "~"
254255 runIO $ writeSource fb (unlines before ++
255− updateMeta False tyline (show n) newmv ++ "\n"
256+ updateMeta tyline (show n) newmv ++ "\n"
256257 ++ unlines later)
257258 runIO $ copyFile fb fn
258259 else iPrintResult newmv
@@ -270,18 +271,34 @@ doProofSearch fn updatefile rec l n hints (Just depth)
270271 nsroot (SN (WhereN _ _ n)) = nsroot n
271272 nsroot n = n
272273
273−updateMeta brack ('?':cs) n new
274+updateMeta ('?':cs) n new
274275 | length cs >= length n
275276 = case splitAt (length n) cs of
276277 (mv, c:cs) ->
277278 if ((isSpace c || c == ')' || c == '}') && mv == n)
278− then addBracket brack new ++ (c : cs)
279− else '?' : mv ++ c : updateMeta True cs n new
279+ then new ++ (c : cs)
280+ else '?' : mv ++ c : updateMeta cs n new
281+ (mv, []) -> if (mv == n) then new else '?' : mv
282+updateMeta ('=':'>':cs) n new = '=':'>':updateMeta cs n new
283+updateMeta ('=':cs) n new = '=':updateMeta cs n new
284+updateMeta (c:cs) n new
285+ = c : updateMeta cs n new
286+updateMeta [] n new = ""
287+
288+guessBrackets brack ('?':cs) n new
289+ | length cs >= length n
290+ = case splitAt (length n) cs of
291+ (mv, c:cs) ->
292+ if ((isSpace c || c == ')' || c == '}') && mv == n)
293+ then addBracket brack new
294+ else guessBrackets True cs n new
280295 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
281−updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
282−updateMeta brack (c:cs) n new
283− = c : updateMeta (brack || not (isSpace c)) cs n new
284−updateMeta brack [] n new = ""
296+guessBrackets brack ('=':'>':cs) n new = guessBrackets False cs n new
297+guessBrackets brack ('-':'>':cs) n new = guessBrackets False cs n new
298+guessBrackets brack ('=':cs) n new = guessBrackets False cs n new
299+guessBrackets brack (c:cs) n new
300+ = guessBrackets (brack || not (isSpace c)) cs n new
301+guessBrackets brack [] n new = ""
285302
286303checkProv line n = isProv' False line n
287304 where
@@ -326,7 +343,7 @@ makeLemma fn updatefile l n
326343 constraints i classes mty ++
327344 showTmOpts (defaultPPOption { ppopt_pinames = True })
328345 (stripMNBind skip margs (delab i mty))
329− let lem_app = show n ++ appArgs skip margs mty
346+ let lem_app = guessBrackets False tyline (show n) (show n ++ appArgs skip margs mty)
330347
331348 if updatefile then
332349 do let fb = fn ++ "~"
@@ -454,7 +471,7 @@ makeLemma fn updatefile l n
454471 = case span (not . blank) (reverse before) of
455472 (bef, []) -> (bef, "" : [])
456473 x -> x
457− mvline = updateMeta False tyline (show n) lem_app in
474+ mvline = updateMeta tyline (show n) lem_app in
458475 unlines $ reverse bef_start ++
459476 [blankline, lem, blankline] ++
460477 reverse bef_end ++ mvline : later