@@ -709,7 +709,7 @@ process h fn (DoProofSearch updatefile l n hints)
709709 if updatefile then
710710 do let fb = fn ++ "~"
711711 runIO $ writeFile fb (unlines before ++
712− updateMeta tyline (show n) newmv ++ "\n"
712+ updateMeta False tyline (show n) newmv ++ "\n"
713713 ++ unlines later)
714714 runIO $ copyFile fb fn
715715 else ihPrintResult h newmv
@@ -727,16 +727,22 @@ process h fn (DoProofSearch updatefile l n hints)
727727 nsroot (SN (WhereN _ _ n)) = nsroot n
728728 nsroot n = n
729729
730− updateMeta ('?':cs) n new
730+ updateMeta brack ('?':cs) n new
731731 | length cs >= length n
732732 = case splitAt (length n) cs of
733733 (mv, c:cs) ->
734734 if (isSpace c && mv == n)
735− then new ++ (c : cs)
736− else '?' : mv ++ c : updateMeta cs n new
735+ then addBracket brack new ++ (c : cs)
736+ else '?' : mv ++ c : updateMeta True cs n new
737737 (mv, []) -> if (mv == n) then new else '?' : mv
738− updateMeta (c:cs) n new = c : updateMeta cs n new
739− updateMeta [] n new = ""
738+ updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
739+ updateMeta brack (c:cs) n new
740+ = c : updateMeta (not (not brack && isSpace c)) cs n new
741+ updateMeta brack [] n new = ""
742+
743+ addBracket False new = new
744+ addBracket True new | any isSpace new = '(' : new ++ ")"
745+ | otherwise = new
740746
741747process h fn (Spec t)
742748 = do (tm, ty) <- elabVal toplevel False t