Availability::- use_module(pldoc(doc_html)).
- edit_button(+File, +Options)// is det
- Create an edit button for File. If the button is clicked,
JavaScript sends a message to the server without modifying the
current page. JavaScript code is in the file pldoc.js.