IntenseWebs/pgadmin4
3
0
Fork 0
mirror of https://github.com/pgadmin-org/pgadmin4.git synced 2025-02-25 18:55:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

Ensure breakpoints are cleared properly when clearing all of them. Fixes #1745

Browse Source
This commit is contained in:
Neel Patel 2017-01-08 19:05:13 +05:30 committed by Dave Page
parent 1325b30e0b
commit d87345ef52
1 changed files with 15 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
web/pgadmin/tools/debugger/templates/debugger/js/direct.js
View File

@ -804,10 +804,10 @@ define(
// If gutterMarker is undefined that means there is no marker defined previously
// So we need to set the breakpoint command here...
if (info.gutterMarkers == undefined) {
baseUrl = "{{ url_for('debugger.index') }}" + "set_breakpoint/" + trans_id + "/" + self.active_line_no + "/" + "1";
baseUrl = "{{ url_for('debugger.index') }}" + "set_breakpoint/" + trans_id + "/" + (self.active_line_no + 1) + "/" + "1";
}
else {
baseUrl = "{{ url_for('debugger.index') }}" + "set_breakpoint/" + trans_id + "/" + self.active_line_no + "/" + "0";
baseUrl = "{{ url_for('debugger.index') }}" + "set_breakpoint/" + trans_id + "/" + (self.active_line_no + 1) + "/" + "0";
}
$.ajax({
@ -1443,11 +1443,22 @@ define(
controller.set_breakpoint(self.trans_id,m+1,1); //set the breakpoint
}
else {
controller.set_breakpoint(self.trans_id,m+1,0); //clear the breakpoint
if (info.gutterMarkers.breakpoints == undefined) {
controller.set_breakpoint(self.trans_id,m+1,1); //set the breakpoint
}
else {
controller.set_breakpoint(self.trans_id,m+1,0); //clear the breakpoint
}
}
// If line folding is defined then gutterMarker will be defined so
// we need to find out 'breakpoints' information
var markers = info.gutterMarkers;
if (markers != undefined && info.gutterMarkers.breakpoints == undefined)
markers = info.gutterMarkers.breakpoints
cm.setGutterMarker(
m, "breakpoints", info.gutterMarkers ? null : function() {
m, "breakpoints", markers ? null : function() {
var marker = document.createElement("div");
marker.style.color = "#822";