Fix frontend to verify Dafny code

psoft-tools/package.json

@@ -11,6 +11,7 @@
   },
   "dependencies": {
     "@monaco-editor/react": "^4.6.0",
+    "@types/react-router-dom": "^5.3.3",
     "autoprefixer": "^10.4.17",
     "postcss": "^8.4.35",
     "react": "^18.2.0",

psoft-tools/src/components/DafnyEditor.tsx

@@ -1,5 +1,5 @@
 import { EditorProps, useMonaco } from "@monaco-editor/react";
-import { useEffect } from "react";
+import { useEffect, useRef } from "react";
 import { Editor } from "@monaco-editor/react";
 import useDafny from "../hooks/useDafny";
 
@@ -41,5 +41,27 @@ export default function DafnyEditor({
     };
   }, [monaco]);
 
-  return <Editor {...EditorProps} />;
+  const editorRef = useRef(null);
+
+  function handleEditorDidMount(editor, monaco) {
+    editorRef.current = editor;
+  }
+
+  function showValue() {
+    globalThis.dafnyCode = editorRef.current?.getValue();
+  }
+
+  function clearValue() {
+    editorRef.current?.setValue("");
+  }
+
+   return (<div><button onClick={clearValue}>Clear</button>
+        <Editor {
+          ...EditorProps} 
+          value={"// Please enter Dafny code below and delete this comment!"}
+          onMount={handleEditorDidMount}
+          onChange={showValue}
+        />
+      </div>
+    );
 }

psoft-tools/src/custom.d.ts

@@ -1,4 +1,8 @@
 declare module "*.svg" {
     const content: React.FunctionComponent<React.SVGAttributes<SVGElement>>;
     export default content;
-  }
+  }
+
+declare global {
+  var dafnyCode: string;
+}

psoft-tools/src/pages/index.tsx

@@ -1,5 +1,5 @@
 import Navbar from "../components/Navbar";
-import { useState } from "react";
+import { useState, useRef } from "react";
 import { post } from "../lib/api";
 import { ThreeDots } from "react-loader-spinner";
 import DafnyEditor from "../components/DafnyEditor";
@@ -19,7 +19,16 @@ export default function Index() {
 
   const handleVerify = () => {
     setLoading(true);
-    post("http://localhost:3000/verify", code)
+    var obj = {
+      requester: "postman",
+      files: [
+        {
+        name: "problem.dfy",
+        content: globalThis.dafnyCode
+        }
+      ]
+    }
+    post("http://localhost/compile", JSON.stringify(obj))
       .then((response) => {
         setLoading(false);
         setData(response);
@@ -95,7 +104,6 @@ export default function Index() {
         style={{ paddingTop: "50px", width: "100%", overflow: "hidden" }}
       >
         <div style={{ width: "50%", justifyContent: "left" }}>
-
           <DafnyEditor
             EditorProps={{
               height: "92vh",
@@ -114,7 +122,6 @@ export default function Index() {
             )}
           </div>
           <div className="flex flex-row justify-evenly max-h-11 mb-4">
-            <button onClick={handleClickClear}>Clear</button>
             <button onClick={handleVerify}>Verify Dafny</button>
             <button onClick={handleRun}>Run Dafny</button>
           </div>