From dba8e3379c9a50e245344f3e98b01a7070c9a7a8 Mon Sep 17 00:00:00 2001 From: igorocky <123@gmail.com> Date: Fri, 9 Jun 2023 21:44:26 +0200 Subject: [PATCH] #67 Implement "Hide tabs", "Scroll toolbar" and "Small buttons" view options. --- src/metamath/ui/MM_cmp_editor.res | 161 ++++++++++++------ .../ui/MM_cmp_editor_view_options.res | 51 +++++- src/metamath/ui/MM_cmp_root.res | 11 +- src/metamath/ui/MM_cmp_settings.res | 2 +- src/metamath/ui/MM_cmp_user_stmt.res | 26 ++- src/metamath/ui/MM_cmp_user_stmt.resi | 3 + .../react-components/Expln_React_UseTabs.res | 4 +- 7 files changed, 192 insertions(+), 66 deletions(-) diff --git a/src/metamath/ui/MM_cmp_editor.res b/src/metamath/ui/MM_cmp_editor.res index 71d96406..1b7e7001 100644 --- a/src/metamath/ui/MM_cmp_editor.res +++ b/src/metamath/ui/MM_cmp_editor.res @@ -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 => { @@ -29,10 +31,20 @@ let rndIconButton = ( ~active:bool, ~ref:option=?, ~title:option=?, + ~smallBtns:bool=false, () ) => { - onClick()} color="primary"> icon + onClick()} + color="primary" + style=?{ + if (smallBtns) {Some(ReactDOM.Style.make(~padding="2px", ()))} else {None} + } + > + icon + } @@ -72,6 +84,8 @@ let make = ( ~initialStateJsonStr:option, ~tempMode:bool, ~openCtxSelector:React.refunit>>, + ~showTabs:bool, + ~setShowTabs:bool=>unit, ) => { let (mainMenuIsOpened, setMainMenuIsOpened) = React.useState(_ => false) let mainMenuButtonRef = React.useRef(Js.Nullable.null) @@ -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, @@ -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 @@ -1065,60 +1088,86 @@ let make = ( } } + let rndButtonsFragment = () => { + <> + Belt_Option.isNone } + checked={mainCheckboxState->Belt_Option.getWithDefault(false)} + onChange={_ => actToggleMainCheckbox()} + style=?{ + if (smallBtns) {Some(ReactDOM.Style.make(~padding="2px", ()))} else {None} + } + /> + {rndIconButton(~icon=, ~onClick=actMoveCheckedStmtsDown, ~active= !editIsActive && canMoveCheckedStmts(state,false), + ~title="Move selected statements down", ~smallBtns, ())} + {rndIconButton(~icon=, ~onClick=actMoveCheckedStmtsUp, ~active= !editIsActive && canMoveCheckedStmts(state,true), + ~title="Move selected statements up", ~smallBtns, ())} + {rndIconButton(~icon=, ~onClick=actAddNewStmt, ~active= !editIsActive, + ~title="Add new statement (and place before selected statements if any)", ~smallBtns, ())} + {rndIconButton(~icon=, ~onClick=actDeleteCheckedStmts, + ~active= !editIsActive && atLeastOneStmtIsChecked, ~title="Delete selected statements", ~smallBtns, () + )} + {rndIconButton(~icon=, ~onClick=actDuplicateStmt, + ~active= !editIsActive && isSingleStmtChecked(state), ~title="Duplicate selected statement", + ~smallBtns, ())} + {rndIconButton(~icon=, + ~onClick=actMergeTwoStmts, + ~active=oneStatementIsChecked, ~title="Merge two similar statements", ~smallBtns, ())} + { + rndIconButton(~icon=, ~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=, ~onClick=actSubstitute, + ~active=generalModificationActionIsEnabled && state.checkedStmtIds->Js.Array2.length <= 2, + ~title="Apply a substitution to all statements", ~smallBtns,() ) } + { + rndIconButton(~icon=, ~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=, ~onClick=actOpenMainMenu, ~active={!editIsActive}, + ~ref=ReactDOM.Ref.domRef(mainMenuButtonRef), + ~title="Additional actions", ~smallBtns, () ) + } + + } + let rndButtons = () => { - - { - switch idx { - | 10 => Some(Js.Json.string("auto")) - | _ => None - } - }} + if (scrollToolbar) { + let windowWidth = window["innerWidth"] + Belt_Int.toString ++ "px"}, + () + ) > - Belt_Option.isNone } - checked={mainCheckboxState->Belt_Option.getWithDefault(false)} - onChange={_ => actToggleMainCheckbox()} - /> - {rndIconButton(~icon=, ~onClick=actMoveCheckedStmtsDown, ~active= !editIsActive && canMoveCheckedStmts(state,false), - ~title="Move selected statements down", ())} - {rndIconButton(~icon=, ~onClick=actMoveCheckedStmtsUp, ~active= !editIsActive && canMoveCheckedStmts(state,true), - ~title="Move selected statements up", ())} - {rndIconButton(~icon=, ~onClick=actAddNewStmt, ~active= !editIsActive, - ~title="Add new statement (and place before selected statements if any)", ())} - {rndIconButton(~icon=, ~onClick=actDeleteCheckedStmts, - ~active= !editIsActive && atLeastOneStmtIsChecked, ~title="Delete selected statements", () - )} - {rndIconButton(~icon=, ~onClick=actDuplicateStmt, - ~active= !editIsActive && isSingleStmtChecked(state), ~title="Duplicate selected statement", ())} - {rndIconButton(~icon=, - ~onClick=actMergeTwoStmts, - ~active=oneStatementIsChecked, ~title="Merge two similar statements", ())} - { - rndIconButton(~icon=, ~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=, ~onClick=actSubstitute, - ~active=generalModificationActionIsEnabled && state.checkedStmtIds->Js.Array2.length <= 2, - ~title="Apply a substitution to all statements", () ) } - { - rndIconButton(~icon=, ~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=, ~onClick=actOpenMainMenu, ~active={!editIsActive}, - ~ref=ReactDOM.Ref.domRef(mainMenuButtonRef), - ~title="Additional actions", () ) - } - - + {rndButtonsFragment()} + + } else { + + { + // switch idx { + // | 10 => Some(Js.Json.string("auto")) + // | _ => None + // } + // }} + > + {rndButtonsFragment()} + + + } } let rndErrors = (stmt:userStmt):reElem => { @@ -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 => { 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) @@ -18,6 +21,9 @@ let make = ( 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) @@ -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]) + { React.string("View Options") } + + setHideTabs(_ => b)) + /> + } + label="Hide tabs" + /> setInlineMode(_ => b)) /> } - label="Compact Mode" + label="Compact mode" + /> + setScrollToolbar(_ => b)) + /> + } + label="Scroll toolbar" + /> + setSmallBtns(_ => b)) + /> + } + label="Small buttons" /> diff --git a/src/metamath/ui/MM_cmp_root.res b/src/metamath/ui/MM_cmp_root.res index 26419d8d..a612ffd7 100644 --- a/src/metamath/ui/MM_cmp_root.res +++ b/src/metamath/ui/MM_cmp_root.res @@ -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) @@ -200,6 +201,8 @@ let make = () => { initialStateJsonStr=editorInitialStateJsonStr tempMode=tempMode.contents openCtxSelector + showTabs + setShowTabs={b=>setShowTabs(_ => b)} /> | ExplorerIndex => { onExpandedChange=actCtxSelectorExpandedChange doExpand=openCtxSelector /> - {renderTabs()} + { + if (showTabs) { + renderTabs() + } else { +
+ } + } } content={contentTop => { diff --git a/src/metamath/ui/MM_cmp_settings.res b/src/metamath/ui/MM_cmp_settings.res index cbe81e43..79aeb014 100644 --- a/src/metamath/ui/MM_cmp_settings.res +++ b/src/metamath/ui/MM_cmp_settings.res @@ -971,7 +971,7 @@ let make = ( onChange=evt2bool(actHideContextSelectorChange) /> } - label="Hide Metamath context header" + label="Hide context header" /> { @@ -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 @@ -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 + } - - - + + - - - - + + + { if (copiedToClipboard->Belt.Option.isSome) { diff --git a/src/metamath/ui/MM_cmp_user_stmt.resi b/src/metamath/ui/MM_cmp_user_stmt.resi index f5d746a0..91ce90fc 100644 --- a/src/metamath/ui/MM_cmp_user_stmt.resi +++ b/src/metamath/ui/MM_cmp_user_stmt.resi @@ -23,6 +23,9 @@ type viewOptions = { showType:bool, showJstf:bool, inlineMode:bool, + scrollToolbar:bool, + smallBtns:bool, + hideTabs:bool, } type props = { diff --git a/src/rescript-utils/main/react-components/Expln_React_UseTabs.res b/src/rescript-utils/main/react-components/Expln_React_UseTabs.res index 15d7bce4..90ac8bbe 100644 --- a/src/rescript-utils/main/react-components/Expln_React_UseTabs.res +++ b/src/rescript-utils/main/react-components/Expln_React_UseTabs.res @@ -136,7 +136,7 @@ let useTabs = ():tabMethods<'a> => { variant=#scrollable onChange={(_,id)=>openTab(id)} style=ReactDOM.Style.make( - ~minHeight="20px", + ~minHeight="25px", () ) > @@ -170,7 +170,7 @@ let useTabs = ():tabMethods<'a> => { } } style=ReactDOM.Style.make( - ~minHeight="20px", + ~minHeight="25px", ~padding="3px", () )