#21 Add a "reset" option.

expln · Aug 5, 2023 · 6195322 · 6195322
1 parent 0080f38
commit 6195322
Show file tree

Hide file tree

Showing 5 changed files with 31 additions and 4 deletions.
diff --git a/src/metamath/test/MM_wrk_editor_json.res b/src/metamath/test/MM_wrk_editor_json.res
@@ -83,7 +83,6 @@ let createInitialEditorState = (
         disjText: stateLocStor->Belt.Option.map(obj => obj.disjText)->Belt.Option.getWithDefault(""),
         disjEditMode: false,
         disjErr: None,
-        disj: Belt_MapInt.fromArray([]),
 
         wrkCtx: None,
 

diff --git a/src/metamath/test/MM_wrk_editor_test.res b/src/metamath/test/MM_wrk_editor_test.res
@@ -68,7 +68,6 @@ let createEditorState = (
         disjText: "",
         disjEditMode: false,
         disjErr: None,
-        disj: Belt_MapInt.fromArray([]),
 
         wrkCtx: None,
 

diff --git a/src/metamath/ui/MM_cmp_editor.res b/src/metamath/ui/MM_cmp_editor.res
@@ -1240,6 +1240,10 @@ let make = (
         })->ignore
     }
 
+    let actResetEditorContent = () => {
+        setState(resetEditorContent)
+    }
+
     let rndError = (msgOpt,color) => {
         switch msgOpt {
             | None => <></>
@@ -1306,6 +1310,14 @@ let make = (
                         >
                             {"Import from JSON ..."->React.string}
                         </MenuItem>
+                        <MenuItem
+                            onClick={() => {
+                                actCloseMainMenu()
+                                actResetEditorContent()
+                            }}
+                        >
+                            {"Reset editor content"->React.string}
+                        </MenuItem>
                         <MenuItem
                             onClick={() => {
                                 actCloseMainMenu()

diff --git a/src/metamath/worker/MM_wrk_editor.res b/src/metamath/worker/MM_wrk_editor.res
@@ -209,7 +209,6 @@ type editorState = {
     disjText: string,
     disjEditMode: bool,
     disjErr: option<string>,
-    disj: Belt_MapInt.t<Belt_SetInt.t>,
 
     wrkCtx: option<mmContext>,
 
@@ -2572,3 +2571,21 @@ let textToSyntaxTree = (
         }
     }
 }
+
+let resetEditorContent = (st:editorState):editorState => {
+    {
+        ...st,
+
+        descr: "",
+        descrEditMode: false,
+
+        varsText: "",
+        varsEditMode: false,
+
+        disjText: "",
+        disjEditMode: false,
+
+        stmts: [],
+        checkedStmtIds: [],
+    }
+}
diff --git a/src/metamath/worker/MM_wrk_editor.resi b/src/metamath/worker/MM_wrk_editor.resi
@@ -124,7 +124,6 @@ type editorState = {
     disjText: string,
     disjEditMode: bool,
     disjErr: option<string>,
-    disj: Belt_MapInt.t<Belt_SetInt.t>,
 
     wrkCtx: option<mmContext>,
 
@@ -200,6 +199,7 @@ let findStmtsToMerge: editorState => result<(userStmt,userStmt), string>
 let parseJstf: string => result<option<jstf>,string>
 let removeAllTempData: editorState => editorState
 let isEditMode: editorState => bool
+let resetEditorContent: editorState => editorState
 
 let getIdsOfSelectedNodes: stmtCont => (int,Belt_SetInt.t)
 let hasSelectedText: stmtCont => bool