From 2840a7757fe953e38d17befb43a108ae7e3fd094 Mon Sep 17 00:00:00 2001 From: Brian Gough Date: Tue, 14 Jun 2016 12:32:54 +0100 Subject: [PATCH 1/2] fix bug in synctex position calculation for syncToCode --- .../ide/pdf/controllers/PdfController.coffee | 25 ++++++++++++++++--- .../coffee/ide/pdfng/directives/pdfJs.coffee | 6 ++++- .../ide/pdfng/directives/pdfViewer.coffee | 6 ++++- 3 files changed, 31 insertions(+), 6 deletions(-) diff --git a/services/web/public/coffee/ide/pdf/controllers/PdfController.coffee b/services/web/public/coffee/ide/pdf/controllers/PdfController.coffee index 58d7c34564..f6f1006e4a 100644 --- a/services/web/public/coffee/ide/pdf/controllers/PdfController.coffee +++ b/services/web/public/coffee/ide/pdf/controllers/PdfController.coffee @@ -353,18 +353,35 @@ define [ deferred.reject() return deferred.promise + # FIXME: this actually works better if it's halfway across the + # page (or the visible part of the page). Synctex doesn't + # always find the right place in the file when the point is at + # the edge of the page, it sometimes returns the start of the + # next paragraph instead. + h = position.offset.left + + # Compute the vertical position to pass to synctex, which + # works with coordinates increasing from the top of the page + # down. This matches the browser's DOM coordinate of the + # click point, but the pdf position is measured from the + # bottom of the page so we need to invert it. + if options.fromPdfPosition and position.pageSize?.height? + v = (position.pageSize.height - position.offset.top) or 0 # measure from pdf point (inverted) + else + v = position.offset.top or 0 # measure from html click position + # It's not clear exactly where we should sync to if it wasn't directly # clicked on, but a little bit down from the very top seems best. if options.includeVisualOffset - position.offset.top = position.offset.top + 80 + v += 72 # use the same value as in pdfViewer highlighting visual offset $http({ url: "/project/#{ide.project_id}/sync/pdf", method: "GET", params: { page: position.page + 1 - h: position.offset.left.toFixed(2) - v: position.offset.top.toFixed(2) + h: h.toFixed(2) + v: v.toFixed(2) clsiserverid:ide.clsiServerId isolated: perUserCompile } @@ -395,7 +412,7 @@ define [ $scope.syncToCode = () -> synctex - .syncToCode($scope.pdf.position, includeVisualOffset: true) + .syncToCode($scope.pdf.position, includeVisualOffset: true, fromPdfPosition: true) .then (data) -> {doc, line} = data ide.editorManager.openDoc(doc, gotoLine: line) diff --git a/services/web/public/coffee/ide/pdfng/directives/pdfJs.coffee b/services/web/public/coffee/ide/pdfng/directives/pdfJs.coffee index 2df89bc35f..310a9ba7f8 100644 --- a/services/web/public/coffee/ide/pdfng/directives/pdfJs.coffee +++ b/services/web/public/coffee/ide/pdfng/directives/pdfJs.coffee @@ -50,7 +50,11 @@ define [ scope.scale = { scaleMode: 'scale_mode_fit_width' } if (position = localStorage("pdf.position.#{attrs.key}")) - scope.position = { page: +position.page, offset: { "top": +position.offset.top, "left": +position.offset.left } } + scope.position = + page: +position.page, + offset: + "top": +position.offset.top + "left": +position.offset.left #scope.position = pdfListView.getPdfPosition(true) diff --git a/services/web/public/coffee/ide/pdfng/directives/pdfViewer.coffee b/services/web/public/coffee/ide/pdfng/directives/pdfViewer.coffee index f0ec8d61b1..b719dfb0f2 100644 --- a/services/web/public/coffee/ide/pdfng/directives/pdfViewer.coffee +++ b/services/web/public/coffee/ide/pdfng/directives/pdfViewer.coffee @@ -187,7 +187,8 @@ define [ # console.log 'converted to offset = ', pdfOffset newPosition = { "page": topPageIdx, - "offset" : { "top" : pdfOffset[1], "left": 0 } + "offset" : { "top" : pdfOffset[1], "left": 0} + "pageSize": { "height": viewport.viewBox[3], "width": viewport.viewBox[2] } } return newPosition @@ -208,6 +209,8 @@ define [ return $scope.document.getPdfViewport(page.pageNum).then (viewport) -> page.viewport = viewport pageOffset = viewport.convertToViewportPoint(offset.left, offset.top) + # if the passed-in position doesn't have the page height/width add them now + position.pageSize ?= {"height": viewport.viewBox[3], "width": viewport.viewBox[2]} # console.log 'addition offset =', pageOffset # console.log 'total', pageTop + pageOffset[1] Math.round(pageTop + pageOffset[1] + currentScroll) ## 10 is margin @@ -515,6 +518,7 @@ define [ pageNum = scope.pages[first.page].pageNum + # use a visual offset of 72pt to match the offset in PdfController syncToCode scope.document.getPdfViewport(pageNum).then (viewport) -> position = { page: first.page From 991d3c7aa1308fb1ee9e641a9f42b02332894878 Mon Sep 17 00:00:00 2001 From: Brian Gough Date: Tue, 14 Jun 2016 12:49:06 +0100 Subject: [PATCH 2/2] avoid exception when switching between full and split pdf view --- .../coffee/ide/pdfng/directives/pdfViewer.coffee | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/services/web/public/coffee/ide/pdfng/directives/pdfViewer.coffee b/services/web/public/coffee/ide/pdfng/directives/pdfViewer.coffee index b719dfb0f2..5f87ff25e9 100644 --- a/services/web/public/coffee/ide/pdfng/directives/pdfViewer.coffee +++ b/services/web/public/coffee/ide/pdfng/directives/pdfViewer.coffee @@ -516,7 +516,15 @@ define [ first = highlights[0] - pageNum = scope.pages[first.page].pageNum + # switching between split and full pdf views can cause + # highlights to appear before rendering + if !scope.pages + return # ignore highlight scroll if still rendering + + pageNum = scope.pages[first.page]?.pageNum + + if !pageNum? + return # ignore highlight scroll if page not found # use a visual offset of 72pt to match the offset in PdfController syncToCode scope.document.getPdfViewport(pageNum).then (viewport) ->