From 4febbc43f6d235910ffac96eb62777db77673a36 Mon Sep 17 00:00:00 2001 From: Max Brunsfeld Date: Fri, 26 Apr 2019 19:13:32 -0700 Subject: [PATCH] In docs playground, scroll tree whenever cursor moves --- docs/assets/js/playground.js | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/docs/assets/js/playground.js b/docs/assets/js/playground.js index 6bb12c26..0b7e8127 100644 --- a/docs/assets/js/playground.js +++ b/docs/assets/js/playground.js @@ -125,8 +125,6 @@ var handleCursorMovement = debounce(() => { highlightedNodeLink = null; } - if (!codeEditor.somethingSelected()) return; - const selection = codeEditor.getDoc().listSelections()[0]; let start = {row: selection.anchor.line, column: selection.anchor.ch}; let end = {row: selection.head.line, column: selection.head.ch}; @@ -163,10 +161,10 @@ var renderTree = debounce(() => { result += "(${type}` result += `[${start.row + 1}, ${start.column}] - [${end.row + 1}, ${end.column}]`; - if (node.namedChildCount > 0) { - for (let i = 0, n = node.namedChildCount; i < n; i++) { + if (node.namedChildren.length > 0) { + for (let i = 0, n = node.namedChildren.length; i < n; i++) { result += '\n'; - renderNode(node.namedChild(i), indentLevel + 1); + renderNode(node.namedChildren[i], indentLevel + 1); } } result += ')';