Merge branch 'master' into dev_0.6

2020-05-17 00:23:45 +02:00
parent 69b101ce55 0f054bc606
commit 3a199b79c9
14 changed files with 377 additions and 129 deletions
@@ -91,7 +91,8 @@ class GuiDocHighlighter(QSyntaxHighlighter):
        self.colTagErr = QColor(*self.theTheme.colTagErr)
        self.colRepTag = QColor(*self.theTheme.colRepTag)
        self.colMod    = QColor(*self.theTheme.colMod)
-        self.colTrail  = QColor(*self.theTheme.colEmph,64)
+        self.colTrail  = QColor(*self.theTheme.colEmph)
+        self.colTrail.setAlpha(64)

        self.hStyles = {
            "header1"   : self._makeFormat(self.colHead, "bold",1.8),