[edition] Add a FreeText editor (mozilla#14970)

- add a basic UI to edit some text in a pdf; - an editor can be moved, suppressed, cut, copied, pasted, selected; - add an undo/redo manager.
calixteman · Jun 1, 2022 · 47a78db · 47a78db
1 parent 1ac33c9
commit 47a78db
Show file tree

Hide file tree

Showing 21 changed files with 1,820 additions and 4 deletions.
diff --git a/extensions/chromium/preferences_schema.json b/extensions/chromium/preferences_schema.json
@@ -160,6 +160,10 @@
       ],
       "default": 2
     },
+    "annotationEditionMode": {
+      "type": "boolean",
+      "default": false
+    },
     "enablePermissions": {
       "type": "boolean",
       "default": false