Skip to content

Commit

Permalink
#21 Add a warning about editing in TEMP mode.
Browse files Browse the repository at this point in the history
  • Loading branch information
igorocky committed Jun 23, 2023
1 parent 378c99a commit d332821
Show file tree
Hide file tree
Showing 3 changed files with 83 additions and 12 deletions.
26 changes: 20 additions & 6 deletions src/metamath/ui-utils/MM_react_common.res
Original file line number Diff line number Diff line change
Expand Up @@ -38,9 +38,18 @@ let rndProgress = (~text:string, ~pct:option<float>=?, ~onTerminate:option<unit=
</Paper>
}

let rndInfoDialog = (~text:string, ~onOk:unit=>unit) => {
let rndInfoDialog = (~text:string, ~onOk:unit=>unit, ~title:option<string>=?, ()) => {
<Paper style=ReactDOM.Style.make(~padding="10px", ())>
<Col spacing=1.>
<span
style=ReactDOM.Style.make(
~fontWeight="bold",
~display=?{if (title->Belt_Option.isNone) {Some("none")} else {None}},
()
)
>
{title->Belt_Option.getWithDefault("")->React.string}
</span>
<span>
{text->React.string}
</span>
Expand All @@ -51,13 +60,18 @@ let rndInfoDialog = (~text:string, ~onOk:unit=>unit) => {
</Paper>
}

let openInfoDialog = (~modalRef:modalRef, ~text:string, ~onOk:option<unit=>unit>=?, ()) => {
let openInfoDialog = (~modalRef:modalRef, ~text:string, ~onOk:option<unit=>unit>=?, ~title:option<string>=?, ()) => {
openModal(modalRef, _ => React.null)->promiseMap(modalId => {
updateModal(modalRef, modalId, () => {
rndInfoDialog(~text, ~onOk = () => {
closeModal(modalRef, modalId)
onOk->Belt_Option.forEach(clbk => clbk())
})
rndInfoDialog(
~text,
~onOk = () => {
closeModal(modalRef, modalId)
onOk->Belt_Option.forEach(clbk => clbk())
},
~title?,
()
)
})
})->ignore
}
Expand Down
1 change: 1 addition & 0 deletions src/metamath/ui-utils/MM_react_common.resi
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ let openInfoDialog: (
~modalRef: Expln_React_Modal.modalRef,
~text: string,
~onOk: unit => unit =?,
~title:string=?,
unit,
) => unit

Expand Down
68 changes: 62 additions & 6 deletions src/metamath/ui/MM_cmp_editor.res
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,20 @@ let jsonStrOptToEditorStateLocStor = (jsonStrOpt:option<string>):option<editorSt
})
}

let previousEditingIsNotCompletedTitle = "Previous editing is not completed"
let previousEditingIsNotCompletedText =
`You've attempted to edit something in the editor while the previous edit is not complete.`
++ ` Please complete the previous edit before starting a new one.`

let editingInTempModeTitle = "Editing in TEMP mode"
let editingInTempModeText =
`You are about to edit in TEMP mode.`
++ ` All changes you do in TEMP mode will be erased upon closing current browser tab.`
++ ` If you want to continue editing in NORMAL mode, please do the following actions:`
++ ` 1) use "Export to JSON" to copy current editor state to the clipboard;`
++ ` 2) open a new tab (or switch to an already opened tab) with metamath-lamp in NORMAL mode;`
++ ` 3) use "Import from JSON" to load the copied editor state from the clipboard.`

@react.component
let make = (
~modalRef:modalRef,
Expand All @@ -87,6 +101,7 @@ let make = (
) => {
let (mainMenuIsOpened, setMainMenuIsOpened) = React.useState(_ => false)
let mainMenuButtonRef = React.useRef(Js.Nullable.null)
let (warnedAboutTempMode, setWarnedAboutTempMode) = React.useState(_ => false)

let (showCheckbox, setShowCheckbox) = useStateFromLocalStorageBool(
~key="editor-showCheckbox", ~default=true, ~tempMode
Expand Down Expand Up @@ -261,12 +276,52 @@ let make = (
}
let actBeginEdit0 = (setter:editorState=>editorState) => {
if (!editIsActive) {
setState(setter)
if (tempMode && !warnedAboutTempMode) {
openInfoDialog(
~modalRef,
~title=editingInTempModeTitle,
~text=editingInTempModeText,
~onOk = () => {
setWarnedAboutTempMode(_ => true)
setState(setter)
},
()
)
} else {
setState(setter)
}
} else {
openInfoDialog(
~modalRef,
~title=previousEditingIsNotCompletedTitle,
~text=previousEditingIsNotCompletedText,
()
)
}
}
let actBeginEdit = (setter:(editorState,string)=>editorState, stmtId:string) => {
let actBeginEdit = (setter:(editorState,stmtId)=>editorState, stmtId:string) => {
if (!editIsActive) {
setState(setter(_,stmtId))
if (tempMode && !warnedAboutTempMode) {
openInfoDialog(
~modalRef,
~title=editingInTempModeTitle,
~text=editingInTempModeText,
~onOk = () => {
setWarnedAboutTempMode(_ => true)
setState(setter(_,stmtId))
},
()
)
} else {
setState(setter(_,stmtId))
}
} else {
openInfoDialog(
~modalRef,
~title=previousEditingIsNotCompletedTitle,
~text=previousEditingIsNotCompletedText,
()
)
}
}
let actCompleteEdit = (setter:editorState=>editorState) => {
Expand Down Expand Up @@ -950,9 +1005,10 @@ let make = (
})->ignore
}

let actShowInfoAboutGettingCompletedProof = () => {
let actShowInfoAboutGettingCompletedProof = (title:string) => {
openInfoDialog(
~modalRef,
~title,
~text=`In order to show a completed proof please do the following: `
++ `1) Make sure the step you want to show a completed proof for is marked with a green chekmark. `
++ `If it is not, try to "unify all"; 2) Select the step you want to show a completed proof for; `
Expand All @@ -967,10 +1023,10 @@ let make = (
switch stmt.proofStatus {
| Some(Ready) => actExportProof(stmt.id)
| Some(Waiting) | Some(NoJstf) | Some(JstfIsIncorrect) | None =>
actShowInfoAboutGettingCompletedProof()
actShowInfoAboutGettingCompletedProof(`A proof is not available`)
}
}
| _ => actShowInfoAboutGettingCompletedProof()
| _ => actShowInfoAboutGettingCompletedProof(`A single provable step should be selected`)
}
}

Expand Down

0 comments on commit d332821

Please sign in to comment.