)]}'
{
  "commit": "b399b0912f6cc195f2859c1bea425c247772a45c",
  "tree": "c4ab99f3439a9d0a99a59238dbfa31d27fd2519f",
  "parents": [
    "803553a556fd82fa1060efb0c43eda542130cb16"
  ],
  "author": {
    "name": "Kyle Miller",
    "email": "kmill31415@gmail.com",
    "time": "Sat May 16 23:35:20 2026 -0700"
  },
  "committer": {
    "name": "Kyle Miller",
    "email": "kmill31415@gmail.com",
    "time": "Sat May 16 23:35:20 2026 -0700"
  },
  "message": "feat: add `MessageData.withExprHover`\n\nThis PR adds `MessageData.withExprHover`, for creating messages that show information about an expression when hovered over. A `withExprHoverM` variant captures the current local context.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "ad5b6c4347793f251b05bd89643b749401cfc6e4",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Doc.lean",
      "new_id": "7cf39d3158c8a98809c1e5b81b937d062252ad5c",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Doc.lean"
    },
    {
      "type": "modify",
      "old_id": "d5552f455cb8c844d045ec22c2e943d0429b9bad",
      "old_mode": 33188,
      "old_path": "src/Lean/Message.lean",
      "new_id": "db099029ce1f19107b43b82cbf76370f249be178",
      "new_mode": 33188,
      "new_path": "src/Lean/Message.lean"
    }
  ]
}