From d05767d74c461744ed2dd903f47959f503edd691 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 18 Jun 2024 17:37:28 +0200 Subject: [PATCH] add dev version of new typewriter input --- client/src/components/infoview/typewriter.tsx | 32 +++++++++++++++++++ client/src/css/level.css | 12 +++++++ package-lock.json | 27 ++++++++++++++++ package.json | 2 ++ 4 files changed, 73 insertions(+) diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx index 5f12159..f83bd5f 100644 --- a/client/src/components/infoview/typewriter.tsx +++ b/client/src/components/infoview/typewriter.tsx @@ -21,6 +21,8 @@ import { ChatContext, PageContext, MonacoEditorContext, ProofContext, GameIdCont import { goalsToString, lastStepHasErrors, loadGoals } from './goals' import { GameHint, ProofState } from './rpc_api' import { useTranslation } from 'react-i18next' +import { InputAbbreviationRewriter } from '@leanprover/unicode-input-component' +import ContentEditable from 'react-contenteditable' export interface GameDiagnosticsParams { uri: DocumentUri; @@ -91,6 +93,19 @@ export function Typewriter({disabled}: {disabled?: boolean}) { const inputRef = useRef() + // TODO: added for new typewriter. Clean up. + const [abbrRewriter, setAbbrRewriter] = useState() + const typewriterRef = useRef() + const typewriterContent = useRef('(new typewriter)') + const handleTypewriterChange = evt => { + typewriterContent.current = evt.target.value; + abbrRewriter?.resetAbbreviations() + }; + const handleTypeWriterBlur = () => { + console.log(`handle typewriter blur. content: ${typewriterContent.current}`); + }; + + // The context storing all information about the current proof const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext) @@ -179,6 +194,15 @@ export function Typewriter({disabled}: {disabled?: boolean}) { // }, [uri]); + // Use unicode abbreviations in typewriter input + useEffect(() => { + const abbrRewriter = new InputAbbreviationRewriter({ + abbreviationCharacter: "\\", + customTranslations: {}, + eagerReplacementEnabled: false + }, typewriterRef.current!) + setAbbrRewriter(abbrRewriter) + }, []) useEffect(() => { const myEditor = monaco.editor.create(inputRef.current!, { @@ -267,6 +291,14 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
+ + + {/*
*/} diff --git a/client/src/css/level.css b/client/src/css/level.css index e325a95..133db44 100644 --- a/client/src/css/level.css +++ b/client/src/css/level.css @@ -356,3 +356,15 @@ td code { background: #DDF6FF; text-align: center; } + +#unicode-input { + min-width: 0; + flex: 1; + /* padding: 0.4em .6em 0; */ + font-size: var(--vscode-editor-font-size); + background-color: white; + border: 2px solid orange; + display: flex; + flex-direction: column; + font-family: JuliaMono, monospace; +} diff --git a/package-lock.json b/package-lock.json index c2471fb..86ad7af 100644 --- a/package-lock.json +++ b/package-lock.json @@ -18,6 +18,7 @@ "@fortawesome/free-solid-svg-icons": "^6.5.1", "@fortawesome/react-fontawesome": "^0.2.0", "@leanprover/infoview": "^0.4.3", + "@leanprover/unicode-input-component": "^0.1.0", "@mui/icons-material": "^5.11.0", "@mui/material": "^5.11.1", "@reduxjs/toolkit": "^1.9.1", @@ -38,6 +39,7 @@ "octokit": "^3.1.2", "path-browserify": "^1.0.1", "react": "^18.2.0", + "react-contenteditable": "^3.3.7", "react-country-flag": "^3.1.0", "react-dom": "^18.2.0", "react-i18next": "^14.1.0", @@ -2827,6 +2829,19 @@ "resolved": "https://registry.npmjs.org/@leanprover/infoview-api/-/infoview-api-0.2.1.tgz", "integrity": "sha512-4sYdwOhUsa5wfvo/ZsCbcm8fBWcrATciZq0sWfmi5NRbIyZ+c2QjTm6D9CeYPCNvz9yvD1KBp/2+hKEZ8SOHkA==" }, + "node_modules/@leanprover/unicode-input": { + "version": "0.1.0", + "resolved": "https://registry.npmjs.org/@leanprover/unicode-input/-/unicode-input-0.1.0.tgz", + "integrity": "sha512-B/rB8HwSzbM+Jg1DGM5yLJVxy6+OrOXwuo/tDLuGy8UsmtcOwqPXCIvrVBK7P723tF5+NmxewSUK3rQVEjng9A==" + }, + "node_modules/@leanprover/unicode-input-component": { + "version": "0.1.0", + "resolved": "https://registry.npmjs.org/@leanprover/unicode-input-component/-/unicode-input-component-0.1.0.tgz", + "integrity": "sha512-QX2WhhShPDpCE6YTHjJ63hF8UdYU0gke/GXeln8jtuIj2F7n0gqSzzt4jS1JSOHcNEop9KuPy9oWw3iyQ8EIVg==", + "dependencies": { + "@leanprover/unicode-input": "~0.1.0" + } + }, "node_modules/@mui/base": { "version": "5.0.0-beta.34", "resolved": "https://registry.npmjs.org/@mui/base/-/base-5.0.0-beta.34.tgz", @@ -13872,6 +13887,18 @@ "node": ">=0.10.0" } }, + "node_modules/react-contenteditable": { + "version": "3.3.7", + "resolved": "https://registry.npmjs.org/react-contenteditable/-/react-contenteditable-3.3.7.tgz", + "integrity": "sha512-GA9NbC0DkDdpN3iGvib/OMHWTJzDX2cfkgy5Tt98JJAbA3kLnyrNbBIpsSpPpq7T8d3scD39DHP+j8mAM7BIfQ==", + "dependencies": { + "fast-deep-equal": "^3.1.3", + "prop-types": "^15.7.1" + }, + "peerDependencies": { + "react": ">=16.3" + } + }, "node_modules/react-country-flag": { "version": "3.1.0", "resolved": "https://registry.npmjs.org/react-country-flag/-/react-country-flag-3.1.0.tgz", diff --git a/package.json b/package.json index e626c88..9b46287 100644 --- a/package.json +++ b/package.json @@ -15,6 +15,7 @@ "@fortawesome/free-solid-svg-icons": "^6.5.1", "@fortawesome/react-fontawesome": "^0.2.0", "@leanprover/infoview": "^0.4.3", + "@leanprover/unicode-input-component": "^0.1.0", "@mui/icons-material": "^5.11.0", "@mui/material": "^5.11.1", "@reduxjs/toolkit": "^1.9.1", @@ -35,6 +36,7 @@ "octokit": "^3.1.2", "path-browserify": "^1.0.1", "react": "^18.2.0", + "react-contenteditable": "^3.3.7", "react-country-flag": "^3.1.0", "react-dom": "^18.2.0", "react-i18next": "^14.1.0",