- reloadBuffer(buf);
-}
-
-
-void GuiView::reloadBuffer(Buffer * buf)
-{
- FileName filename = buf->fileName();
- Buffer const * parent = buf->parent();
- bool const is_child = parent != buf;
- // The user has already confirmed that the changes, if any, should
- // be discarded. So we just release the Buffer and don't call closeBuffer();
- theBufferList().release(buf);
- buf = loadDocument(filename);
- docstring const disp_fn = makeDisplayPath(filename.absFilename());
- docstring str;
- if (buf) {
- // re-allocate master if necessary
- if (is_child && theBufferList().isLoaded(parent)
- && buf->parent() != parent)
- buf->setParent(parent);
- buf->updateLabels();
- setBuffer(buf);
- buf->errors("Parse");
- str = bformat(_("Document %1$s reloaded."), disp_fn);
- } else {
- str = bformat(_("Could not reload document %1$s"), disp_fn);
- }
- message(str);