Add editor options for plain text mode and to disable block folding to

workaround rendering speed issues in CodeMirror with very large scripts.
Fixes #4631.

Re-arrange editor options in the Preferences dialogue to tidy things up.
This commit is contained in:
Aditya Toshniwal
2019-09-04 15:46:08 +01:00
committed by Dave Page
parent 5e54f20578
commit 1c2ba72f02
16 changed files with 403 additions and 375 deletions

View File

@@ -1792,14 +1792,7 @@ define([
foldOptions: {
widget: '\u2026',
},
foldGutter: {
rangeFinder: CodeMirror.fold.combine(
CodeMirror.pgadminBeginRangeFinder,
CodeMirror.pgadminIfRangeFinder,
CodeMirror.pgadminLoopRangeFinder,
CodeMirror.pgadminCaseRangeFinder
),
},
foldGutter: true,
gutters: [
'CodeMirror-linenumbers', 'CodeMirror-foldgutter', 'breakpoints',
],