diff --git a/Projects/MathlibDemo/MathlibDemo.lean b/Projects/MathlibDemo/MathlibDemo.lean index d4e5aa5d..460985ec 100644 --- a/Projects/MathlibDemo/MathlibDemo.lean +++ b/Projects/MathlibDemo/MathlibDemo.lean @@ -6,3 +6,9 @@ import MathlibDemo.Bijection import MathlibDemo.Logic import MathlibDemo.Rational import MathlibDemo.Ring + +import Verso +import VersoBlog +import VersoManual +import VersoUtil +import VersoSearch diff --git a/Projects/MathlibDemo/build.sh b/Projects/MathlibDemo/build.sh index 4ddc624d..1456a1b8 100755 --- a/Projects/MathlibDemo/build.sh +++ b/Projects/MathlibDemo/build.sh @@ -3,19 +3,6 @@ # Operate in the directory where this file is located cd $(dirname $0) -# Updating Mathlib: We follow the instructions at -# https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4 - -# Note: we had once problems with the `lake-manifest` when a new dependency got added -# to `mathlib`, we may need to add `rm lake-manifest.json` again if that's still a problem. - -# currently the mathlib post-update-hook is not good enough to update the lean-toolchain. -# things break if the new lakefile is not valid in the old lean version -curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain - -# note: mathlib has now a post-update hook that modifies the `lean-toolchain` -# and calls `lake exe cache get`. - lake update -R lake build lake build Batteries diff --git a/Projects/MathlibDemo/lake-manifest.json b/Projects/MathlibDemo/lake-manifest.json index c9a1cbb7..7614b3a7 100644 --- a/Projects/MathlibDemo/lake-manifest.json +++ b/Projects/MathlibDemo/lake-manifest.json @@ -1,31 +1,61 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/mathlib4", + [{"url": "https://github.com/leanprover/verso", "type": "git", "subDir": null, "scope": "", - "rev": "bfd79bd53242ce07c2f41264531699b721cd209d", + "rev": "9137d010a277cd29e0989a65445805c292caf01e", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.27.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "1603151ac0db4e822908e18094f16acc250acaff", + "scope": "", + "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "1e55697c44a646f8a22e2a91878efc4496aa5743", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", + "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e25fe66cf13e902ba550533ef681cc35a9f18dc2", + "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +75,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6980f6ca164de593cb77cd03d8eac549cc444156", + "rev": "c04225ee7c0585effbd933662b3151f01b600e40", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.62", + "inputRev": "v0.0.85", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c3a19fa17982c5c1413fea335f371869b8b12e1d", + "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e1d2994e0acdee2f0c03c9d84d28a5df34aa0020", + "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +105,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5e6a77528fb6cace1f0adf2563e4e1bc1da541ae", + "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +115,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "a0abd472348dd725adbb26732e79b26e7e220913", + "rev": "55c37290ff6186e2e965d68cf853a57c0702db82", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.27.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "MathlibDemo", diff --git a/Projects/MathlibDemo/lakefile.toml b/Projects/MathlibDemo/lakefile.toml index 530a913c..04f58b43 100644 --- a/Projects/MathlibDemo/lakefile.toml +++ b/Projects/MathlibDemo/lakefile.toml @@ -7,7 +7,12 @@ pp.unicode.fun = true [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "master" +rev = "v4.27.0" + +[[require]] +name = "verso" +git = "https://github.com/leanprover/verso" +rev = "v4.27.0" [[lean_lib]] name = "MathlibDemo" diff --git a/Projects/MathlibDemo/lean-toolchain b/Projects/MathlibDemo/lean-toolchain index 1efd3655..d9ca740c 100644 --- a/Projects/MathlibDemo/lean-toolchain +++ b/Projects/MathlibDemo/lean-toolchain @@ -1 +1,2 @@ -leanprover/lean4:v4.21.0-rc3 +leanprover/lean4:v4.27.0 + diff --git a/Projects/Stable/Stable.lean b/Projects/Stable/Stable.lean new file mode 100644 index 00000000..d1299c3f --- /dev/null +++ b/Projects/Stable/Stable.lean @@ -0,0 +1,5 @@ +import Verso +import VersoBlog +import VersoManual +import VersoUtil +import VersoSearch diff --git a/Projects/Stable/Stable/SampleDoc.lean b/Projects/Stable/Stable/SampleDoc.lean new file mode 100644 index 00000000..0177ded5 --- /dev/null +++ b/Projects/Stable/Stable/SampleDoc.lean @@ -0,0 +1,24 @@ +import VersoManual +open Verso Doc +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean + +#doc (Manual) "My Document" => + +This is a Verso document. + +It can include inline math, like this: $`x + 4 = -3`. + +It can also include block math, like +$$`\int_\mathsf{this}^\mathtt{orthis} \mathit{or{\ldots}maybe{\ldots}this}` + +We also support inline lean, like this: {lean}`Nat.add_assoc`. + +We also support block lean, like this: + +```lean +/-- The name we will be greeting -/ +def theName := "Jimothy" + +#eval s!"Hello {theName}" +``` diff --git a/Projects/Stable/build.sh b/Projects/Stable/build.sh new file mode 100755 index 00000000..9320820a --- /dev/null +++ b/Projects/Stable/build.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash + +# Operate in the directory where this file is located +cd $(dirname $0) + +lake update -R +lake build \ No newline at end of file diff --git a/Projects/Stable/lake-manifest.json b/Projects/Stable/lake-manifest.json new file mode 100644 index 00000000..79ade4bd --- /dev/null +++ b/Projects/Stable/lake-manifest.json @@ -0,0 +1,45 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover/verso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "9137d010a277cd29e0989a65445805c292caf01e", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "1e55697c44a646f8a22e2a91878efc4496aa5743", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}], + "name": "Stable", + "lakeDir": ".lake"} diff --git a/Projects/Stable/lakefile.toml b/Projects/Stable/lakefile.toml new file mode 100644 index 00000000..f551028d --- /dev/null +++ b/Projects/Stable/lakefile.toml @@ -0,0 +1,13 @@ +name = "Stable" +defaultTargets = ["Stable"] + +[leanOptions] +pp.unicode.fun = true + +[[require]] +name = "verso" +git = "https://github.com/leanprover/verso" +rev = "v4.27.0" + +[[lean_lib]] +name = "Stable" diff --git a/Projects/Stable/lean-toolchain b/Projects/Stable/lean-toolchain new file mode 100644 index 00000000..5249182c --- /dev/null +++ b/Projects/Stable/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.27.0 diff --git a/Projects/lean-nightly/LeanNightly.lean b/Projects/lean-nightly/LeanNightly.lean deleted file mode 100644 index e69de29b..00000000 diff --git a/Projects/lean-nightly/lake-manifest.json b/Projects/lean-nightly/lake-manifest.json deleted file mode 100644 index c6a0a16b..00000000 --- a/Projects/lean-nightly/lake-manifest.json +++ /dev/null @@ -1,5 +0,0 @@ -{"version": 7, - "packagesDir": ".lake/packages", - "packages": [], - "name": "leanlatest", - "lakeDir": ".lake"} diff --git a/Projects/lean-nightly/lakefile.lean b/Projects/lean-nightly/lakefile.lean deleted file mode 100644 index 989d55a6..00000000 --- a/Projects/lean-nightly/lakefile.lean +++ /dev/null @@ -1,12 +0,0 @@ -import Lake -open Lake DSL - -package leanlatest { - -- add package configuration options here - leanOptions := #[⟨`experimental.module, true⟩] -} - -@[default_target] -lean_lib LeanNightly { - -- add library configuration options here -} diff --git a/Projects/lean-nightly/lean-nightly.lean b/Projects/lean-nightly/lean-nightly.lean deleted file mode 100644 index e69de29b..00000000 diff --git a/Projects/lean-nightly/lean-toolchain b/Projects/lean-nightly/lean-toolchain deleted file mode 100644 index 6a9c6db3..00000000 --- a/Projects/lean-nightly/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:nightly diff --git a/Projects/mathlib-stable/.gitignore b/Projects/mathlib-stable/.gitignore deleted file mode 100644 index 1282aa2b..00000000 --- a/Projects/mathlib-stable/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -/build -/lake-packages/* -*.olean diff --git a/Projects/mathlib-stable/MathlibStable.lean b/Projects/mathlib-stable/MathlibStable.lean deleted file mode 100644 index f3335e00..00000000 --- a/Projects/mathlib-stable/MathlibStable.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Mathlib -import ProofWidgets diff --git a/Projects/mathlib-stable/lake-manifest.json b/Projects/mathlib-stable/lake-manifest.json deleted file mode 100644 index ad0112d2..00000000 --- a/Projects/mathlib-stable/lake-manifest.json +++ /dev/null @@ -1,77 +0,0 @@ -{"version": 7, - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover/std4", - "type": "git", - "subDir": null, - "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", - "name": "std", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/import-graph.git", - "type": "git", - "subDir": null, - "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "rev": "971ecd03805fe1026721e65f53ef163132abb75c", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "stable", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/hhu-adam/lean4web-tools.git", - "type": "git", - "subDir": null, - "rev": "8be7734dfa9a686d3a1329651e2a1a690e1123b6", - "name": "webeditor", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}], - "name": "mathlibStable", - "lakeDir": ".lake"} diff --git a/Projects/mathlib-stable/lakefile.lean b/Projects/mathlib-stable/lakefile.lean deleted file mode 100644 index 9b8e45b3..00000000 --- a/Projects/mathlib-stable/lakefile.lean +++ /dev/null @@ -1,14 +0,0 @@ -import Lake -open Lake DSL - -require mathlib from git - "https://github.com/leanprover-community/mathlib4"@"stable" - -package mathlibStable { - -- add package configuration options here -} - -@[default_target] -lean_lib MathlibStable { - -- add library configuration options here -} diff --git a/Projects/mathlib-stable/lean-toolchain b/Projects/mathlib-stable/lean-toolchain deleted file mode 100644 index 9ad30404..00000000 --- a/Projects/mathlib-stable/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.7.0 diff --git a/Projects/mathlib-stable/mathlib-stable.lean b/Projects/mathlib-stable/mathlib-stable.lean deleted file mode 100644 index e69de29b..00000000 diff --git a/Projects/mathlib-v4.24.0/.gitignore b/Projects/mathlib-v4.24.0/.gitignore deleted file mode 100644 index 1282aa2b..00000000 --- a/Projects/mathlib-v4.24.0/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -/build -/lake-packages/* -*.olean diff --git a/Projects/mathlib-v4.24.0/MathlibStable.lean b/Projects/mathlib-v4.24.0/MathlibStable.lean deleted file mode 100644 index f3335e00..00000000 --- a/Projects/mathlib-v4.24.0/MathlibStable.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Mathlib -import ProofWidgets diff --git a/Projects/mathlib-v4.24.0/lake-manifest.json b/Projects/mathlib-v4.24.0/lake-manifest.json deleted file mode 100644 index 46ffedb8..00000000 --- a/Projects/mathlib-v4.24.0/lake-manifest.json +++ /dev/null @@ -1,95 +0,0 @@ -{"version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "scope": "", - "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.24.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "d768126816be17600904726ca7976b185786e6b9", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "556caed0eadb7901e068131d1be208dd907d07a2", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.74", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "mathlibStable", - "lakeDir": ".lake"} diff --git a/Projects/mathlib-v4.24.0/lakefile.lean b/Projects/mathlib-v4.24.0/lakefile.lean deleted file mode 100644 index 508854af..00000000 --- a/Projects/mathlib-v4.24.0/lakefile.lean +++ /dev/null @@ -1,14 +0,0 @@ -import Lake -open Lake DSL - -require mathlib from git - "https://github.com/leanprover-community/mathlib4"@"v4.24.0" - -package mathlibStable { - -- add package configuration options here -} - -@[default_target] -lean_lib MathlibStable { - -- add library configuration options here -} diff --git a/Projects/mathlib-v4.24.0/lean-toolchain b/Projects/mathlib-v4.24.0/lean-toolchain deleted file mode 100644 index c00a5350..00000000 --- a/Projects/mathlib-v4.24.0/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.24.0 diff --git a/Projects/mathlib-v4.24.0/mathlib-stable.lean b/Projects/mathlib-v4.24.0/mathlib-stable.lean deleted file mode 100644 index e69de29b..00000000 diff --git a/client/src/App.tsx b/client/src/App.tsx index 42d60da3..875d753a 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -17,6 +17,7 @@ import { PreferencesContext } from './Popups/Settings' import { Entries } from './utils/Entries' import { fixedEncodeURIComponent, formatArgs, lookupUrl, parseArgs } from './utils/UrlParsing' import { useWindowDimensions } from './utils/WindowWidth' +import TabView from './TabView'; // CSS import './css/App.css' @@ -429,14 +430,11 @@ function App() { }
-
-

- You are in the plain text editor

- Go back to the Monaco Editor (click ) - for the infoview to update! -

-
+ diff --git a/client/src/TabView.tsx b/client/src/TabView.tsx new file mode 100644 index 00000000..e49ffff1 --- /dev/null +++ b/client/src/TabView.tsx @@ -0,0 +1,166 @@ +import { faCode } from "@fortawesome/free-solid-svg-icons"; +import { FontAwesomeIcon } from "@fortawesome/react-fontawesome"; +import { ReactNode, RefObject, useEffect, useState } from "react"; +import "./css/TabView.css"; +import { preview } from "vite"; + +type TabId = "info" | "preview"; +interface TabViewButtonProps { + id: TabId; + currentTab: TabId; + setTabId: (id: TabId) => void; + children: ReactNode; +} + +function TabViewButton({ id, currentTab, setTabId, children }: TabViewButtonProps) { + const isActive = id === currentTab; + return ( + + ); +} + +interface VersoPreviewProps { + currentTab: TabId; + isUsingMobile: boolean; + code: string; +} + +function VersoPreview({ currentTab, isUsingMobile, code }: VersoPreviewProps) { + const [isLoading, setIsLoading] = useState(false); + const [previewedCode, setPreviewedCode] = useState(null); + const [hrefForIframe, setHrefForIframe] = useState(null); + const [error, setError] = useState(null); + + const loadCode = () => { + setIsLoading(true); + setError(null); + fetch("/verso/api/singlepage", { + method: "POST", + headers: { + "Content-Type": "application/json", + }, + body: JSON.stringify({ projectId: "Stable", fileContents: code }), + }) + .then((resp) => resp.json()) + .then((json) => { + console.log(json); + setIsLoading(false); + if (typeof json?.result !== "string") { + setError("Unexpected response from server."); + setPreviewedCode(code); + console.error(json); + return; + } + if (json.result !== "0") { + setError(json.output.join("")); + setPreviewedCode(code); + return; + } + setHrefForIframe(json.href); + setPreviewedCode(code); + }) + .catch((err) => { + setIsLoading(false); + setError("Unexpected response from server."); + setPreviewedCode(code); + console.error(err); + }); + }; + + const [lastTab, setLastTab] = useState(currentTab); + useEffect(() => { + if (lastTab === currentTab) return; + setLastTab(currentTab); + if (currentTab !== "preview") return; + if (code === previewedCode) return; + if (isLoading) return; + loadCode(); + }, [currentTab, lastTab]); + + return ( +
+ + {hrefForIframe && !error &&