selectInsertPanel.js

window;import{jsx as e,jsxs as r}from"react/jsx-runtime";import*as t from"react";import{RpcContext as a,EditorContext as o,useAsync as n,mapRpcError as l}from"@leanprover/infoview";function i({pos:i,goals:s,selectedLocations:c,replaceRange:d,title:p,help:u,callback:m}){const f=t.useContext(a),v=t.useContext(o),h=n((async()=>{const e=function(e,r){for(const t of e)if(t.mvarId===r.mvarId)return t;throw new Error(`could not find goal for location ${JSON.stringify(r)}`)}(s,c[0]);return await f.call(m,{cursorPos:i,ctx:e.ctx,selectedLocations:c,replaceRange:d})}),[s,c,i,d]),g="resolved"===h.state?e("pre",{className:"font-code pre-wrap",children:e("a",{onClick:async()=>{"resolved"===h.state&&h.value&&(await v.api.applyEdit(h.value.edit),await v.revealPosition({...h.value.newCursorPos,uri:i.uri}))},className:"link pointer dim",title:"Apply suggestion",children:h.value&&h.value.content})}):"rejected"===h.state?e("p",{style:{color:"red"},children:l(h.error).message}):e("p",{children:"Loading...'"}),w=0===c.length?e("span",{children:u}):g;return r("details",{open:!0,children:[e("summary",{className:"mv2 pointer",children:p}),e("div",{className:"ml1",children:w})]})}export{i as default};