| 102 | } |
| 103 | |
| 104 | json server_tool::to_json() { |
| 105 | return { |
| 106 | {"display_name", display_name}, |
| 107 | {"tool", name}, |
| 108 | {"type", "builtin"}, |
| 109 | {"permissions", json{ |
| 110 | {"write", permission_write} |
| 111 | }}, |
| 112 | {"definition", get_definition()}, |
| 113 | }; |
| 114 | } |
| 115 | |
| 116 | // |
| 117 | // read_file: read a file with optional line range and line-number prefix |