add dev version of new typewriter input

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<InputAbbreviationRewriter>()
+  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}) {
         <div className="typewriter-input-wrapper">
           <div ref={inputRef} className="typewriter-input" />
         </div>
+
+        <ContentEditable
+          innerRef={typewriterRef}
+          id="unicode-input"
+          html={typewriterContent.current}
+          onBlur={handleTypeWriterBlur}
+          onChange={handleTypewriterChange} />
+        {/* <div ref={inputRef2} id="unicode-input" contentEditable="true"></div> */}
         <button type="submit" disabled={processing} className="btn btn-inverted">
           <FontAwesomeIcon icon={faWandMagicSparkles} />&nbsp;{t("Execute")}
         </button>

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;
+}

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",

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",