1import { useState, useEffect, useRef } from 'react';
2import { Box, Paper } from '@mui/material';
3import { ThemeProvider, createTheme } from '@mui/material/styles';
4import CssBaseline from '@mui/material/CssBaseline';
5import AppBar from './components/AppBar';
6import ProofEditor from './components/ProofEditor';
7import ResultsPanel from './components/ResultsPanel';
8import { verifyProofContent } from './utils/verification';
9import type { VerificationResult } from './utils/verification';
10import { getContentFromUrl, updateUrlWithContent } from './utils/urlState';
12const theme = createTheme({
13 palette: {
14 mode: 'light',
15 primary: {
16 main: '#1976d2',
17 },
18 },
19});
21const DEFAULT_EXAMPLE = `axiom my_axiom
22 suppose a : Nat
23 conclude eq(a, a)
25theorem reflexivity
26 suppose x : Nat
27 conclude eq(x, x)
28 proof
29 exact my_axiom
30`;
32function App() {
33 // Load content from URL on mount using lazy initialization
34 const [content, setContent] = useState<string>(() => {
35 const urlContent = getContentFromUrl();
36 return urlContent || DEFAULT_EXAMPLE;
37 });
38 const [verificationResult, setVerificationResult] = useState<VerificationResult | null>(null);
39 const [isVerifying, setIsVerifying] = useState(false);
40 const verificationTimeoutRef = useRef<number | null>(null);
41 const urlUpdateTimeoutRef = useRef<number | null>(null);
43 // Debounced verification
44 useEffect(() => {
45 if (verificationTimeoutRef.current) {
46 clearTimeout(verificationTimeoutRef.current);
47 }
49 const contentToVerify = content.trim();
51 verificationTimeoutRef.current = window.setTimeout(() => {
52 if (!contentToVerify) {
53 setVerificationResult(null);
54 setIsVerifying(false);
55 } else {
56 setIsVerifying(true);
57 const result = verifyProofContent(contentToVerify);
58 setVerificationResult(result);
59 setIsVerifying(false);
60 }
61 }, 500); // 500ms debounce
63 return () => {
64 if (verificationTimeoutRef.current) {
65 clearTimeout(verificationTimeoutRef.current);
66 }
67 };
68 }, [content]);
70 // Debounced URL update
71 useEffect(() => {
72 if (urlUpdateTimeoutRef.current) {
73 clearTimeout(urlUpdateTimeoutRef.current);
74 }
76 urlUpdateTimeoutRef.current = window.setTimeout(() => {
77 updateUrlWithContent(content);
78 }, 1000); // 1 second debounce for URL updates
80 return () => {
81 if (urlUpdateTimeoutRef.current) {
82 clearTimeout(urlUpdateTimeoutRef.current);
83 }
84 };
85 }, [content]);
87 const handleDownload = () => {
88 const blob = new Blob([content], { type: 'text/plain' });
89 const url = URL.createObjectURL(blob);
90 const link = document.createElement('a');
91 link.href = url;
92 link.download = 'proof.prf';
93 document.body.appendChild(link);
94 link.click();
95 document.body.removeChild(link);
96 URL.revokeObjectURL(url);
97 };
99 return (
100 <ThemeProvider theme={theme}>
101 <CssBaseline />
102 <Box sx={{ height: '100vh', display: 'flex', flexDirection: 'column' }}>
103 <AppBar onDownload={handleDownload} />
104 <Box sx={{ flex: 1, display: 'flex', overflow: 'hidden', p: 2, gap: 2 }}>
105 <Paper
106 elevation={2}
107 sx={{
108 flex: 1,
109 display: 'flex',
110 flexDirection: 'column',
111 overflow: 'hidden',
112 p: 2,
113 }}
114 >
115 <ProofEditor content={content} onChange={setContent} />
116 </Paper>
117 <Paper
118 elevation={2}
119 sx={{
120 flex: 1,
121 display: 'flex',
122 flexDirection: 'column',
123 overflow: 'hidden',
124 }}
125 >
126 <ResultsPanel result={verificationResult} isVerifying={isVerifying} />
127 </Paper>
128 </Box>
129 </Box>
130 </ThemeProvider>
131 );
132}
134export default App;