Skip to content

Commit

Permalink
#67 Implement "Hide tabs", "Scroll toolbar" and "Small buttons" view …
Browse files Browse the repository at this point in the history 
…options.
  • Loading branch information
igorocky committed Jun 9, 2023
1 parent 4264240 commit dba8e33
Show file tree
Hide file tree
Showing 7 changed files with 192 additions and 66 deletions.
161 changes: 107 additions & 54 deletions src/metamath/ui/MM_cmp_editor.res
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ open Local_storage_utils
open Common
open MM_wrk_pre_ctx_data

@val external window: {..} = "window"

let unifyAllIsRequiredCnt = ref(0)

let editorSaveStateToLocStor = (state:editorState, key:string, tempMode:bool):unit => {
Expand All @@ -29,10 +31,20 @@ let rndIconButton = (
~active:bool,
~ref:option<ReactDOM.domRef>=?,
~title:option<string>=?,
~smallBtns:bool=false,
()
) => {
<span ?ref ?title>
<IconButton disabled={!active} onClick={_ => onClick()} color="primary"> icon </IconButton>
<IconButton
disabled={!active}
onClick={_ => onClick()}
color="primary"
style=?{
if (smallBtns) {Some(ReactDOM.Style.make(~padding="2px", ()))} else {None}
}
>
icon
</IconButton>
</span>
}

Expand Down Expand Up @@ -72,6 +84,8 @@ let make = (
~initialStateJsonStr:option<string>,
~tempMode:bool,
~openCtxSelector:React.ref<Js.Nullable.t<unit=>unit>>,
~showTabs:bool,
~setShowTabs:bool=>unit,
) => {
let (mainMenuIsOpened, setMainMenuIsOpened) = React.useState(_ => false)
let mainMenuButtonRef = React.useRef(Js.Nullable.null)
Expand All @@ -94,6 +108,12 @@ let make = (
let (inlineMode, setInlineMode) = useStateFromLocalStorageBool(
~key="editor-inlineMode", ~default=false, ~tempMode
)
let (scrollToolbar, setScrollToolbar) = useStateFromLocalStorageBool(
~key="editor-scrollToolbar", ~default=false, ~tempMode
)
let (smallBtns, setSmallBtns) = useStateFromLocalStorageBool(
~key="editor-smallBtns", ~default=false, ~tempMode
)

let (state, setStatePriv) = React.useState(_ => createInitialEditorState(
~settingsV=preCtxData.settingsV.ver,
Expand Down Expand Up @@ -987,6 +1007,9 @@ let make = (
showType onShowTypeChange = {b => setShowType(_ => b) }
showJstf onShowJstfChange = {b => setShowJstf(_ => b) }
inlineMode onInlineModeChange = {b => setInlineMode(_ => b) }
scrollToolbar onScrollToolbarChange = {b => setScrollToolbar(_ => b) }
smallBtns onSmallBtnsChange = {b => setSmallBtns(_ => b) }
hideTabs={!showTabs} onHideTabsChange = {b => setShowTabs(!b) }
/>
})
})->ignore
Expand Down Expand Up @@ -1065,60 +1088,86 @@ let make = (
}
}

let rndButtonsFragment = () => {
<>
<Checkbox
disabled=editIsActive
indeterminate={ mainCheckboxState->Belt_Option.isNone }
checked={mainCheckboxState->Belt_Option.getWithDefault(false)}
onChange={_ => actToggleMainCheckbox()}
style=?{
if (smallBtns) {Some(ReactDOM.Style.make(~padding="2px", ()))} else {None}
}
/>
{rndIconButton(~icon=<MM_Icons.ArrowDownward/>, ~onClick=actMoveCheckedStmtsDown, ~active= !editIsActive && canMoveCheckedStmts(state,false),
~title="Move selected statements down", ~smallBtns, ())}
{rndIconButton(~icon=<MM_Icons.ArrowUpward/>, ~onClick=actMoveCheckedStmtsUp, ~active= !editIsActive && canMoveCheckedStmts(state,true),
~title="Move selected statements up", ~smallBtns, ())}
{rndIconButton(~icon=<MM_Icons.Add/>, ~onClick=actAddNewStmt, ~active= !editIsActive,
~title="Add new statement (and place before selected statements if any)", ~smallBtns, ())}
{rndIconButton(~icon=<MM_Icons.DeleteForever/>, ~onClick=actDeleteCheckedStmts,
~active= !editIsActive && atLeastOneStmtIsChecked, ~title="Delete selected statements", ~smallBtns, ()
)}
{rndIconButton(~icon=<MM_Icons.ControlPointDuplicate/>, ~onClick=actDuplicateStmt,
~active= !editIsActive && isSingleStmtChecked(state), ~title="Duplicate selected statement",
~smallBtns, ())}
{rndIconButton(~icon=<MM_Icons.MergeType style=ReactDOM.Style.make(~transform="rotate(180deg)", ())/>,
~onClick=actMergeTwoStmts,
~active=oneStatementIsChecked, ~title="Merge two similar statements", ~smallBtns, ())}
{
rndIconButton(~icon=<MM_Icons.Search/>, ~onClick=actSearchAsrt,
~active=generalModificationActionIsEnabled && state.frms->Belt_MapString.size > 0,
~title="Add new statements from existing assertions (and place before selected statements if any)",
~smallBtns, ()
)
}
{ rndIconButton(~icon=<MM_Icons.TextRotationNone/>, ~onClick=actSubstitute,
~active=generalModificationActionIsEnabled && state.checkedStmtIds->Js.Array2.length <= 2,
~title="Apply a substitution to all statements", ~smallBtns,() ) }
{
rndIconButton(~icon=<MM_Icons.Hub/>, ~onClick={() => actUnify(())},
~active=generalModificationActionIsEnabled
&& (!atLeastOneStmtIsChecked || singleProvableChecked->Belt.Option.isSome)
&& state.stmts->Js_array2.length > 0,
~title="Unify all statements or unify selected provable bottom-up", ~smallBtns, () )
}
{
rndIconButton(~icon=<MM_Icons.Menu/>, ~onClick=actOpenMainMenu, ~active={!editIsActive},
~ref=ReactDOM.Ref.domRef(mainMenuButtonRef),
~title="Additional actions", ~smallBtns, () )
}
</>
}

let rndButtons = () => {
<Paper>
<Row
spacing = 0.
childXsOffset = {idx => {
switch idx {
| 10 => Some(Js.Json.string("auto"))
| _ => None
}
}}
if (scrollToolbar) {
let windowWidth = window["innerWidth"]
<Paper
style=ReactDOM.Style.make(
~whiteSpace="nowrap",
~overflowX="scroll",
~overflowY="hidden",
~width={(windowWidth-5)->Belt_Int.toString ++ "px"},
()
)
>
<Checkbox
disabled=editIsActive
indeterminate={ mainCheckboxState->Belt_Option.isNone }
checked={mainCheckboxState->Belt_Option.getWithDefault(false)}
onChange={_ => actToggleMainCheckbox()}
/>
{rndIconButton(~icon=<MM_Icons.ArrowDownward/>, ~onClick=actMoveCheckedStmtsDown, ~active= !editIsActive && canMoveCheckedStmts(state,false),
~title="Move selected statements down", ())}
{rndIconButton(~icon=<MM_Icons.ArrowUpward/>, ~onClick=actMoveCheckedStmtsUp, ~active= !editIsActive && canMoveCheckedStmts(state,true),
~title="Move selected statements up", ())}
{rndIconButton(~icon=<MM_Icons.Add/>, ~onClick=actAddNewStmt, ~active= !editIsActive,
~title="Add new statement (and place before selected statements if any)", ())}
{rndIconButton(~icon=<MM_Icons.DeleteForever/>, ~onClick=actDeleteCheckedStmts,
~active= !editIsActive && atLeastOneStmtIsChecked, ~title="Delete selected statements", ()
)}
{rndIconButton(~icon=<MM_Icons.ControlPointDuplicate/>, ~onClick=actDuplicateStmt,
~active= !editIsActive && isSingleStmtChecked(state), ~title="Duplicate selected statement", ())}
{rndIconButton(~icon=<MM_Icons.MergeType style=ReactDOM.Style.make(~transform="rotate(180deg)", ())/>,
~onClick=actMergeTwoStmts,
~active=oneStatementIsChecked, ~title="Merge two similar statements", ())}
{
rndIconButton(~icon=<MM_Icons.Search/>, ~onClick=actSearchAsrt,
~active=generalModificationActionIsEnabled && state.frms->Belt_MapString.size > 0,
~title="Add new statements from existing assertions (and place before selected statements if any)", ()
)
}
{ rndIconButton(~icon=<MM_Icons.TextRotationNone/>, ~onClick=actSubstitute,
~active=generalModificationActionIsEnabled && state.checkedStmtIds->Js.Array2.length <= 2,
~title="Apply a substitution to all statements", () ) }
{
rndIconButton(~icon=<MM_Icons.Hub/>, ~onClick={() => actUnify(())},
~active=generalModificationActionIsEnabled
&& (!atLeastOneStmtIsChecked || singleProvableChecked->Belt.Option.isSome)
&& state.stmts->Js_array2.length > 0,
~title="Unify all statements or unify selected provable bottom-up", () )
}
{
rndIconButton(~icon=<MM_Icons.Menu/>, ~onClick=actOpenMainMenu, ~active={!editIsActive},
~ref=ReactDOM.Ref.domRef(mainMenuButtonRef),
~title="Additional actions", () )
}
</Row>
</Paper>
{rndButtonsFragment()}
</Paper>
} else {
<Paper>
<Row
spacing = 0.
// childXsOffset = {idx => {
// switch idx {
// | 10 => Some(Js.Json.string("auto"))
// | _ => None
// }
// }}
>
{rndButtonsFragment()}
</Row>
</Paper>
}
}

let rndErrors = (stmt:userStmt):reElem => {
Expand Down Expand Up @@ -1146,7 +1195,11 @@ let make = (
}
}

let viewOptions = { MM_cmp_user_stmt.showCheckbox:showCheckbox, showLabel, showType, showJstf, inlineMode, }
let viewOptions = {
MM_cmp_user_stmt.showCheckbox:showCheckbox,
showLabel, showType, showJstf, inlineMode,
scrollToolbar, smallBtns, hideTabs:!showTabs
}

let rndStmt = (stmt:userStmt):reElem => {
<MM_cmp_user_stmt
Expand Down
51 changes: 50 additions & 1 deletion src/metamath/ui/MM_cmp_editor_view_options.res
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,19 @@ let make = (
~showType:bool, ~onShowTypeChange:bool=>unit,
~showJstf:bool, ~onShowJstfChange:bool=>unit,
~inlineMode:bool, ~onInlineModeChange:bool=>unit,
~scrollToolbar:bool, ~onScrollToolbarChange:bool=>unit,
~smallBtns:bool, ~onSmallBtnsChange:bool=>unit,
~hideTabs:bool, ~onHideTabsChange:bool=>unit,
~onClose:unit=>unit,
) => {
let (showCheckbox, setShowCheckbox) = React.useState(() => showCheckbox)
let (showLabel, setShowLabel) = React.useState(() => showLabel)
let (showType, setShowType) = React.useState(() => showType)
let (showJstf, setShowJstf) = React.useState(() => showJstf)
let (inlineMode, setInlineMode) = React.useState(() => inlineMode)
let (scrollToolbar, setScrollToolbar) = React.useState(() => scrollToolbar)
let (smallBtns, setSmallBtns) = React.useState(() => smallBtns)
let (hideTabs, setHideTabs) = React.useState(() => hideTabs)

React.useEffect1(() => {
onShowCheckboxChange(showCheckbox)
Expand All @@ -44,11 +50,36 @@ let make = (
None
}, [inlineMode])

React.useEffect1(() => {
onScrollToolbarChange(scrollToolbar)
None
}, [scrollToolbar])

React.useEffect1(() => {
onSmallBtnsChange(smallBtns)
None
}, [smallBtns])

React.useEffect1(() => {
onHideTabsChange(hideTabs)
None
}, [hideTabs])

<Paper style=ReactDOM.Style.make(~padding="10px", ())>
<Col>
<span style=ReactDOM.Style.make(~fontWeight="bold", ~fontSize="1.1em", ())>
{ React.string("View Options") }
</span>
<Button onClick={_=>onClose()}> {React.string("Close")} </Button>
<FormControlLabel
control={
<Checkbox
checked=hideTabs
onChange=evt2bool(b => setHideTabs(_ => b))
/>
}
label="Hide tabs"
/>
<FormControlLabel
control={
<Checkbox
Expand Down Expand Up @@ -92,7 +123,25 @@ let make = (
onChange=evt2bool(b => setInlineMode(_ => b))
/>
}
label="Compact Mode"
label="Compact mode"
/>
<FormControlLabel
control={
<Checkbox
checked=scrollToolbar
onChange=evt2bool(b => setScrollToolbar(_ => b))
/>
}
label="Scroll toolbar"
/>
<FormControlLabel
control={
<Checkbox
checked=smallBtns
onChange=evt2bool(b => setSmallBtns(_ => b))
/>
}
label="Small buttons"
/>
<Button onClick={_=>onClose()}> {React.string("Close")} </Button>
</Col>
Expand Down
11 changes: 10 additions & 1 deletion src/metamath/ui/MM_cmp_root.res
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,7 @@ let make = () => {
@warning("-27")
let {tabs, addTab, openTab, removeTab, renderTabs, updateTabs, activeTabId} = Expln_React_UseTabs.useTabs()
let (state, setState) = React.useState(_ => createInitialState(~settings=settingsReadFromLocStor()))
let (showTabs, setShowTabs) = React.useState(() => true)

let reloadCtx = React.useRef(Js.Nullable.null)
let openCtxSelector = React.useRef(Js.Nullable.null)
Expand Down Expand Up @@ -200,6 +201,8 @@ let make = () => {
initialStateJsonStr=editorInitialStateJsonStr
tempMode=tempMode.contents
openCtxSelector
showTabs
setShowTabs={b=>setShowTabs(_ => b)}
/>
| ExplorerIndex =>
<MM_cmp_pe_index
Expand Down Expand Up @@ -250,7 +253,13 @@ let make = () => {
onExpandedChange=actCtxSelectorExpandedChange
doExpand=openCtxSelector
/>
{renderTabs()}
{
if (showTabs) {
renderTabs()
} else {
<div style=ReactDOM.Style.make(~display="none", ()) />
}
}
</Col>
}
content={contentTop => {
Expand Down
2 changes: 1 addition & 1 deletion src/metamath/ui/MM_cmp_settings.res
View file
Original file line number Diff line number Diff line change
Expand Up @@ -971,7 +971,7 @@ let make = (
onChange=evt2bool(actHideContextSelectorChange)
/>
}
label="Hide Metamath context header"
label="Hide context header"
/>
<Divider/>
<MM_cmp_type_settings
Expand Down
26 changes: 19 additions & 7 deletions src/metamath/ui/MM_cmp_user_stmt.res
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,9 @@ type viewOptions = {
showType:bool,
showJstf:bool,
inlineMode:bool,
scrollToolbar:bool,
smallBtns:bool,
hideTabs:bool,
}

let makeInitialState = () => {
Expand Down Expand Up @@ -584,12 +587,16 @@ let propsAreSame = (a:props,b:props):bool => {
a.settingsVer == b.settingsVer
&& a.preCtxVer == b.preCtxVer
&& a.varsText == b.varsText

&& a.visualizationIsOn == b.visualizationIsOn
&& a.viewOptions.showCheckbox == b.viewOptions.showCheckbox
&& a.viewOptions.showLabel == b.viewOptions.showLabel
&& a.viewOptions.showType == b.viewOptions.showType
&& a.viewOptions.showJstf == b.viewOptions.showJstf
&& a.viewOptions.inlineMode == b.viewOptions.inlineMode
&& a.viewOptions.scrollToolbar == b.viewOptions.scrollToolbar
&& a.viewOptions.smallBtns == b.viewOptions.smallBtns
&& a.viewOptions.hideTabs == b.viewOptions.hideTabs

&& a.stmt.label == b.stmt.label
&& a.stmt.labelEditMode == b.stmt.labelEditMode
Expand Down Expand Up @@ -1022,19 +1029,24 @@ let make = React.memoCustomCompareProps( ({
}

let rndSelectionButtons = () => {
let style = if (viewOptions.smallBtns) {
Some(ReactDOM.Style.make(~padding="0px", ~minWidth="30px", ~minHeight="26px", ()))
} else {
None
}
<Row alignItems=#center>
<ButtonGroup variant=#outlined size=#small >
<Button title="Expand selection" onClick={_=>actExpandSelection()}> <MM_Icons.ZoomOutMap/> </Button>
<Button title="Shrink selection" onClick={_=>actShrinkSelection()}> <MM_Icons.ZoomInMap/> </Button>
<Button title="Add new statement above" onClick={_=>actAddStmtAbove()}>
<Button title="Expand selection" onClick={_=>actExpandSelection()} ?style> <MM_Icons.ZoomOutMap/> </Button>
<Button title="Shrink selection" onClick={_=>actShrinkSelection()} ?style> <MM_Icons.ZoomInMap/> </Button>
<Button title="Add new statement above" onClick={_=>actAddStmtAbove()} ?style>
<MM_Icons.Logout style=ReactDOM.Style.make(~transform="rotate(-90deg)", ()) />
</Button>
<Button title="Add new statement below" onClick={_=>actAddStmtBelow()}>
<Button title="Add new statement below" onClick={_=>actAddStmtBelow()} ?style>
<MM_Icons.Logout style=ReactDOM.Style.make(~transform="rotate(90deg)", ()) />
</Button>
<Button title="Copy to the clipboard" onClick={_=>actCopyToClipboard()}> <MM_Icons.ContentCopy/> </Button>
<Button title="Edit" onClick={_=>actEditSelection()}> <MM_Icons.Edit/> </Button>
<Button title="Unselect" onClick={_=>actUnselect()}> <MM_Icons.CancelOutlined/> </Button>
<Button title="Copy to the clipboard" onClick={_=>actCopyToClipboard()} ?style> <MM_Icons.ContentCopy/> </Button>
<Button title="Edit" onClick={_=>actEditSelection()} ?style> <MM_Icons.Edit/> </Button>
<Button title="Unselect" onClick={_=>actUnselect()} ?style> <MM_Icons.CancelOutlined/> </Button>
</ButtonGroup>
{
if (copiedToClipboard->Belt.Option.isSome) {
Expand Down
Loading

0 comments on commit dba8e33

Please sign in to comment.