-
Notifications
You must be signed in to change notification settings - Fork 49
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Proposal for an API based "Suggestions" detail in infoview (#312)
* first version * fix formatting mishap * fix import * Update infoview/suggestions.tsx Co-authored-by: Gabriel Ebner <[email protected]> * Update infoview/suggestions.tsx Co-authored-by: Gabriel Ebner <[email protected]> * insert tactic into editor * rm props.widget * add dosuggest icon * handle unset suggestionURL * suggestions detail open when suggestions activated * debounce prefix * Update infoview/info.tsx Co-authored-by: Gabriel Ebner <[email protected]> * Update src/infoview.ts Co-authored-by: Gabriel Ebner <[email protected]> * Update infoview/info.tsx Co-authored-by: Gabriel Ebner <[email protected]> * Update infoview/suggestions.tsx Co-authored-by: Gabriel Ebner <[email protected]> * typo * Update infoview/suggestions.tsx Co-authored-by: Gabriel Ebner <[email protected]> * Update infoview/suggestions.tsx Co-authored-by: Gabriel Ebner <[email protected]> * Update infoview/suggestions.tsx Co-authored-by: Gabriel Ebner <[email protected]> * Update infoview/suggestions.tsx Co-authored-by: Gabriel Ebner <[email protected]> * x-api-key instead of api_key in message Co-authored-by: Gabriel Ebner <[email protected]>
- Loading branch information
1 parent
8ca7fa6
commit d62eece
Showing
8 changed files
with
302 additions
and
29 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,149 @@ | ||
| import * as React from 'react'; | ||
| import { WidgetIdentifier } from 'lean-client-js-core'; | ||
| import { SuggestionsInfoStatus, SuggestionsInt, SuggestionsModelResult, SuggestionsTacticInfo } from '../src/shared'; | ||
| import { useEvent, delayedThrottled } from './util'; | ||
| import { SuggestionsEvent, SuggestionsErrorEvent, post } from './server'; | ||
|
|
||
| const statusColTable: { [T in SuggestionsInfoStatus]: string } = { | ||
| 'loading': 'gold', | ||
| 'error': 'dark-red', | ||
| 'valid': 'green', | ||
| 'solving': 'blue', | ||
| 'done': '' | ||
| } | ||
| interface SuggestionsProps { | ||
| widget: WidgetIdentifier; | ||
| goalState: string; | ||
| } | ||
|
|
||
| function SingleTacticInfo(props: { tacticInfo: SuggestionsTacticInfo, widget: WidgetIdentifier}): JSX.Element { | ||
| return ( | ||
| <a className={'font-code link pointer mh2 glow easeTransition ' + statusColTable.done} style={{whiteSpace: 'pre-wrap'}} key={`${props.tacticInfo.tactic}`} | ||
| onClick={ | ||
| e => { | ||
| e.preventDefault(); | ||
| post({ | ||
| command: 'insert_text', | ||
| text: `${props.tacticInfo.tactic},`, | ||
| insert_type: 'relative' | ||
| }) | ||
| }} | ||
| > | ||
| {props.tacticInfo.tactic} | ||
| </a> | ||
| ) | ||
| } | ||
|
|
||
|
|
||
| function Waiter(): JSX.Element { | ||
| const [count, setCount] = React.useState(0); | ||
| React.useEffect(() => { | ||
| const interval = setInterval(() => setCount((count + 1) % 4), 500); | ||
| return () => clearInterval(interval); | ||
| }, [count]); | ||
| return <span>{'.'.repeat(count)}</span>; | ||
| } | ||
|
|
||
| function Suggestions(props: { | ||
| goalState: string, reqId: number, widget: WidgetIdentifier | ||
| }) { | ||
| const [status, setStatus] = React.useState<SuggestionsInfoStatus>('loading'); | ||
| const [errorMsg, setErrorMsg] = React.useState<string>(); | ||
| const [suggestionsResults, setSuggestionsResults] = React.useState<SuggestionsModelResult>(); | ||
|
|
||
| // get Suggestions results - set Suggestions results | ||
| useEvent( | ||
| SuggestionsEvent, | ||
| (suggestions: SuggestionsInt) => { | ||
| if (suggestions.results && props.reqId === suggestions.reqId) { | ||
| if (suggestions.results.error) { | ||
| setErrorMsg(suggestions.results.error); | ||
| setStatus('error'); | ||
| } else { | ||
| setSuggestionsResults(suggestions.results); | ||
| setStatus('done'); | ||
| } | ||
| } | ||
| }, | ||
| [props.reqId] | ||
| ); | ||
|
|
||
| React.useEffect(() => { | ||
| setStatus('loading'); | ||
| setErrorMsg(undefined); // reset error msg | ||
| }, [props.reqId]); | ||
|
|
||
| return props.goalState && ( | ||
| <div> | ||
| <div> | ||
| {['loading', 'error'].includes(status) ? | ||
| <p className={'easeTransition ml3 ' + statusColTable[status]}> | ||
| {status === 'loading' ? 'Querying Suggestions' : 'Something went wrong :('} | ||
| {status === 'loading'? <Waiter />: null} | ||
| </p> | ||
| : null} | ||
| {errorMsg ? <i className={'easeTransition ml3 ' + statusColTable[status]}>{errorMsg}</i> : null} | ||
| {(['done', 'checking'].includes(status) && suggestionsResults && !suggestionsResults.error && suggestionsResults.tactic_infos) ? | ||
| <div>{Object.values(suggestionsResults.tactic_infos).map( | ||
| tactic_info => <div><SingleTacticInfo key={tactic_info.tactic} tacticInfo={tactic_info} widget={props.widget}/><br/></div> | ||
| )}</div> | ||
| : null | ||
| } | ||
| </div> | ||
| </div> | ||
| ); | ||
| } | ||
|
|
||
| export function Suggestor(props: SuggestionsProps): JSX.Element { | ||
| const [suggReqId, setSuggReqId] = React.useState(0); | ||
| const [doSuggest, setDoSuggest] = React.useState(false); | ||
| const [errorMsg, setErrorMsg] = React.useState<string>(); | ||
| const [prefix, setPrefix] = React.useState(''); | ||
|
|
||
| useEvent( | ||
| SuggestionsErrorEvent, | ||
| (s) => { | ||
| setErrorMsg(s.error); | ||
| }, [] | ||
| ); | ||
|
|
||
| React.useEffect(() => { | ||
| setDoSuggest(true); | ||
| }, [prefix, props.goalState]) | ||
| React.useEffect(delayedThrottled( | ||
| 300, | ||
| () => { | ||
| if (doSuggest) setDoSuggest(false); | ||
| else return; | ||
| if (props.goalState !== undefined && props.goalState !== 'no goals') { | ||
| setSuggReqId(rid => { | ||
| post({ | ||
| command: 'get_suggestions', | ||
| reqId: rid + 1, | ||
| goalState: props.goalState, | ||
| prefix | ||
| }); | ||
| setErrorMsg(undefined); // reset error msg | ||
| return rid + 1 | ||
| }); | ||
| } | ||
| } | ||
| ), [prefix, props.goalState, doSuggest]) | ||
|
|
||
| const inputProps = { style: { display: 'inline' }, type: 'text', size: 12, value: prefix }; | ||
|
|
||
| return ( | ||
| <div> | ||
| {errorMsg | ||
| ? <i className={'easeTransition mv2 ' + statusColTable.error}>{errorMsg}</i> | ||
| : <div> | ||
| <form className='ml2' onSubmit={(e) => e.preventDefault()}> | ||
| <span>Tactic suggestions with prefix: </span> | ||
| <input {...inputProps} onChange={(e) => setPrefix(e.target.value)} /> | ||
| </form> | ||
| <Suggestions widget={props.widget} goalState={props.goalState} reqId={suggReqId}/> | ||
| </div> | ||
| } | ||
| </div> | ||
| ); | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.