new: setting of editor highlight

2023-10-12 13:28:01 +08:00
parent a43a000c68
commit 7388ad4524
13 changed files with 70 additions and 4 deletions
--- a/lib/view/page/editor.dart
+++ b/lib/view/page/editor.dart
@@ -57,10 +57,12 @@ class _EditorPageState extends State<EditorPage> {
    super.initState();

    /// Higher priority than [path]
-    _langCode = widget.langCode ?? Highlights.getCode(widget.path);
-    _controller = CodeController(
-      language: Highlights.all[_langCode],
-    );
+    if (Stores.setting.editorHighlight.fetch()) {
+      _langCode = widget.langCode ?? Highlights.getCode(widget.path);
+    }
+      _controller = CodeController(
+        language: Highlights.all[_langCode],
+      );

    /// TODO: This is a temporary solution to avoid the loading stuck
    Future.delayed(const Duration(milliseconds: 377)).then((value) async {