@@ -238,7 +238,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)
238 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))
238 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))
239 (ProofSearch rec False depth t psnames hints)]
239 (ProofSearch rec False depth t psnames hints)]
240 let def = PClause fc mn (PRef fc [] mn) [] (body top) []
240 let def = PClause fc mn (PRef fc [] mn) [] (body top) []
241− newmv <- idrisCatch
241+ newmv_pre <- idrisCatch
242 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])
242 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])
243 (tm, ty) <- elabVal recinfo ERHS (PRef fc [] mn)
243 (tm, ty) <- elabVal recinfo ERHS (PRef fc [] mn)
244 ctxt <- getContext
244 ctxt <- getContext
@@ -249,10 +249,11 @@ doProofSearch fn updatefile rec l n hints (Just depth)
249 (dropCtxt envlen
249 (dropCtxt envlen
250 (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))
250 (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))
251 (\e -> return ("?" ++ show n))
251 (\e -> return ("?" ++ show n))
252+ let newmv = guessBrackets False tyline (show n) newmv_pre
252 if updatefile then
253 if updatefile then
253 do let fb = fn ++ "~"
254 do let fb = fn ++ "~"
254 runIO $ writeSource fb (unlines before ++
255 runIO $ writeSource fb (unlines before ++
255− updateMeta False tyline (show n) newmv ++ "\n"
256+ updateMeta tyline (show n) newmv ++ "\n"
256 ++ unlines later)
257 ++ unlines later)
257 runIO $ copyFile fb fn
258 runIO $ copyFile fb fn
258 else iPrintResult newmv
259 else iPrintResult newmv
@@ -270,18 +271,34 @@ doProofSearch fn updatefile rec l n hints (Just depth)
270 nsroot (SN (WhereN _ _ n)) = nsroot n
271 nsroot (SN (WhereN _ _ n)) = nsroot n
271 nsroot n = n
272 nsroot n = n
273−updateMeta brack ('?':cs) n new
274+updateMeta ('?':cs) n new
274 | length cs >= length n
275 | length cs >= length n
275 = case splitAt (length n) cs of
276 = case splitAt (length n) cs of
276 (mv, c:cs) ->
277 (mv, c:cs) ->
277 if ((isSpace c || c == ')' || c == '}') && mv == n)
278 if ((isSpace c || c == ')' || c == '}') && mv == n)
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 = ""
288+guessBrackets brack ('?':cs) n new
289+ | length cs >= length n
290+ = case splitAt (length n) cs of
292+ if ((isSpace c || c == ')' || c == '}') && mv == n)
278− then addBracket brack new ++ (c : cs)
293+ then addBracket brack new
279− else '?' : mv ++ c : updateMeta True cs n new
294+ else guessBrackets True cs n new
280 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
295 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
281−updateMeta brack ('=':cs) n new = '=':updateMeta False cs 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
282−updateMeta brack (c:cs) n new
299+guessBrackets brack (c:cs) n new
283− = c : updateMeta (brack || not (isSpace c)) cs n new
300+ = guessBrackets (brack || not (isSpace c)) cs n new
284−updateMeta brack [] n new = ""
301+guessBrackets brack [] n new = ""
286checkProv line n = isProv' False line n
303checkProv line n = isProv' False line n
@@ -326,7 +343,7 @@ makeLemma fn updatefile l n
326 constraints i classes mty ++
343 constraints i classes mty ++
327 showTmOpts (defaultPPOption { ppopt_pinames = True })
344 showTmOpts (defaultPPOption { ppopt_pinames = True })
328 (stripMNBind skip margs (delab i mty))
345 (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)
331 if updatefile then
348 if updatefile then
332 do let fb = fn ++ "~"
349 do let fb = fn ++ "~"
@@ -454,7 +471,7 @@ makeLemma fn updatefile l n
454 = case span (not . blank) (reverse before) of
471 = case span (not . blank) (reverse before) of
455 (bef, []) -> (bef, "" : [])
472 (bef, []) -> (bef, "" : [])
457− mvline = updateMeta False tyline (show n) lem_app in
474+ mvline = updateMeta tyline (show n) lem_app in
458 unlines $ reverse bef_start ++
475 unlines $ reverse bef_start ++
459 [blankline, lem, blankline] ++
476 [blankline, lem, blankline] ++
460 reverse bef_end ++ mvline : later
477 reverse bef_end ++ mvline : later