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 calculate x
30 = x by-lhs my_axiom x
31`;
33function App() {
34 // Load content from URL on mount using lazy initialization
35 const [content, setContent] = useState<string>(() => {
36 const urlContent = getContentFromUrl();
37 return urlContent || DEFAULT_EXAMPLE;
38 });
39 const [verificationResult, setVerificationResult] = useState<VerificationResult | null>(null);
40 const [isVerifying, setIsVerifying] = useState(false);
41 const verificationTimeoutRef = useRef<number | null>(null);
42 const urlUpdateTimeoutRef = useRef<number | null>(null);
44 // Debounced verification
45 useEffect(() => {
46 if (verificationTimeoutRef.current) {
47 clearTimeout(verificationTimeoutRef.current);
48 }
50 const contentToVerify = content.trim();
52 verificationTimeoutRef.current = window.setTimeout(() => {
53 if (!contentToVerify) {
54 setVerificationResult(null);
55 setIsVerifying(false);
56 } else {
57 setIsVerifying(true);
58 const result = verifyProofContent(contentToVerify);
59 setVerificationResult(result);
60 setIsVerifying(false);
61 }
62 }, 500); // 500ms debounce
64 return () => {
65 if (verificationTimeoutRef.current) {
66 clearTimeout(verificationTimeoutRef.current);
67 }
68 };
69 }, [content]);
71 // Debounced URL update
72 useEffect(() => {
73 if (urlUpdateTimeoutRef.current) {
74 clearTimeout(urlUpdateTimeoutRef.current);
75 }
77 urlUpdateTimeoutRef.current = window.setTimeout(() => {
78 updateUrlWithContent(content);
79 }, 1000); // 1 second debounce for URL updates
81 return () => {
82 if (urlUpdateTimeoutRef.current) {
83 clearTimeout(urlUpdateTimeoutRef.current);
84 }
85 };
86 }, [content]);
88 const handleDownload = () => {
89 const blob = new Blob([content], { type: 'text/plain' });
90 const url = URL.createObjectURL(blob);
91 const link = document.createElement('a');
92 link.href = url;
93 link.download = 'proof.prf';
94 document.body.appendChild(link);
95 link.click();
96 document.body.removeChild(link);
97 URL.revokeObjectURL(url);
98 };
100 return (
101 <ThemeProvider theme={theme}>
102 <CssBaseline />
103 <Box sx={{ height: '100vh', display: 'flex', flexDirection: 'column' }}>
104 <AppBar onDownload={handleDownload} />
105 <Box sx={{ flex: 1, display: 'flex', overflow: 'hidden', p: 2, gap: 2 }}>
106 <Paper
107 elevation={2}
108 sx={{
109 flex: 1,
110 display: 'flex',
111 flexDirection: 'column',
112 overflow: 'hidden',
113 p: 2,
114 }}
115 >
116 <ProofEditor content={content} onChange={setContent} />
117 </Paper>
118 <Paper
119 elevation={2}
120 sx={{
121 flex: 1,
122 display: 'flex',
123 flexDirection: 'column',
124 overflow: 'hidden',
125 }}
126 >
127 <ResultsPanel result={verificationResult} isVerifying={isVerifying} />
128 </Paper>
129 </Box>
130 </Box>
131 </ThemeProvider>
132 );
133}
135export default App;