From c2701a8fb0dc378abefd0a204288883bdd390819 Mon Sep 17 00:00:00 2001 From: Grant Nestor Date: Sat, 27 Jan 2018 18:14:06 -0800 Subject: [PATCH 1/3] Make buffer time between last modified on disk and last modified on last save configurable --- notebook/static/notebook/js/notebook.js | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/notebook/static/notebook/js/notebook.js b/notebook/static/notebook/js/notebook.js index 39b17d2b23..edea0d5099 100644 --- a/notebook/static/notebook/js/notebook.js +++ b/notebook/static/notebook/js/notebook.js @@ -2738,10 +2738,11 @@ define([ return this.contents.get(this.notebook_path, {content: false}).then( function (data) { var last_modified = new Date(data.last_modified); + var difference_buffer = that.config.data['last_modified_buffer'] || 500; // 500 ms // We want to check last_modified (disk) > that.last_modified (our last save) // In some cases the filesystem reports an inconsistent time, - // so we allow 0.5 seconds difference before complaining. - if ((last_modified.getTime() - that.last_modified.getTime()) > 500) { // 500 ms + // so we allow 0.5 seconds (configurable in nbconfig/notebook.json as `last_modified_buffer`) difference before complaining. + if ((last_modified.getTime() - that.last_modified.getTime()) > difference_buffer) { console.warn("Last saving was done on `"+that.last_modified+"`("+that._last_modified+"), "+ "while the current file seem to have been saved on `"+data.last_modified+"`"); if (that._changed_on_disk_dialog !== null) { From 798d29bda8f63dd24fe1a5b4dba1236602937681 Mon Sep 17 00:00:00 2001 From: Grant Nestor Date: Mon, 29 Jan 2018 08:37:34 -0800 Subject: [PATCH 2/3] Change config value name and use seconds vs. milliseconds --- notebook/static/notebook/js/notebook.js | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/notebook/static/notebook/js/notebook.js b/notebook/static/notebook/js/notebook.js index edea0d5099..47ee28da13 100644 --- a/notebook/static/notebook/js/notebook.js +++ b/notebook/static/notebook/js/notebook.js @@ -2738,11 +2738,11 @@ define([ return this.contents.get(this.notebook_path, {content: false}).then( function (data) { var last_modified = new Date(data.last_modified); - var difference_buffer = that.config.data['last_modified_buffer'] || 500; // 500 ms + var last_modified_check_margin = (that.config.data['last_modified_check_margin'] || 0.5) * 1000; // 500 ms // We want to check last_modified (disk) > that.last_modified (our last save) // In some cases the filesystem reports an inconsistent time, // so we allow 0.5 seconds (configurable in nbconfig/notebook.json as `last_modified_buffer`) difference before complaining. - if ((last_modified.getTime() - that.last_modified.getTime()) > difference_buffer) { + if ((last_modified.getTime() - that.last_modified.getTime()) > last_modified_check_margin) { console.warn("Last saving was done on `"+that.last_modified+"`("+that._last_modified+"), "+ "while the current file seem to have been saved on `"+data.last_modified+"`"); if (that._changed_on_disk_dialog !== null) { From 3fce87d60ada9dce5fd3d0d75715de1ad32ba467 Mon Sep 17 00:00:00 2001 From: Thomas Kluyver Date: Mon, 5 Feb 2018 17:14:24 +0000 Subject: [PATCH 3/3] Fix name of config option in comment --- notebook/static/notebook/js/notebook.js | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/notebook/static/notebook/js/notebook.js b/notebook/static/notebook/js/notebook.js index 47ee28da13..df7dc8559f 100644 --- a/notebook/static/notebook/js/notebook.js +++ b/notebook/static/notebook/js/notebook.js @@ -2741,7 +2741,8 @@ define([ var last_modified_check_margin = (that.config.data['last_modified_check_margin'] || 0.5) * 1000; // 500 ms // We want to check last_modified (disk) > that.last_modified (our last save) // In some cases the filesystem reports an inconsistent time, - // so we allow 0.5 seconds (configurable in nbconfig/notebook.json as `last_modified_buffer`) difference before complaining. + // so we allow 0.5 seconds difference before complaining. + // This is configurable in nbconfig/notebook.json as `last_modified_check_margin`. if ((last_modified.getTime() - that.last_modified.getTime()) > last_modified_check_margin) { console.warn("Last saving was done on `"+that.last_modified+"`("+that._last_modified+"), "+ "while the current file seem to have been saved on `"+data.last_modified+"`");