Skip to content

Commit

Permalink
chore: bump Std; json% has been upstreamed
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Oct 24, 2023
1 parent 857a06c commit 5382e38
Show file tree
Hide file tree
Showing 7 changed files with 6 additions and 119 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -3,3 +3,4 @@
# JavaScript build artefacts.
/widget/dist
/widget/node_modules
lakefile.olean
1 change: 0 additions & 1 deletion ProofWidgets.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,5 @@ import ProofWidgets.Component.Panel.SelectionPanel
import ProofWidgets.Component.PenroseDiagram
import ProofWidgets.Component.Recharts
import ProofWidgets.Data.Html
import ProofWidgets.Data.Json
import ProofWidgets.Data.Svg
import ProofWidgets.Presentation.Expr
3 changes: 1 addition & 2 deletions ProofWidgets/Compat.lean
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
import Lean.Attributes
import Lean.Widget.UserWidget

import ProofWidgets.Data.Json
import Std.Data.Json

/-!
A compatibility layer aimed at redefining the user widget API in terms of modules and components.
Expand Down
94 changes: 0 additions & 94 deletions ProofWidgets/Data/Json.lean

This file was deleted.

1 change: 0 additions & 1 deletion ProofWidgets/Data/Svg.lean
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
import ProofWidgets.Data.Json
import ProofWidgets.Data.Html

namespace ProofWidgets
Expand Down
18 changes: 0 additions & 18 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -96,24 +96,6 @@ open scoped ProofWidgets.Jsx

See the `Jsx.lean` and `ExprPresentation.lean` demos.

### `json%` syntax

JSON-like syntax. Invoke with `json%`, escape with `$( _ )`

```lean
import ProofWidgets.Data.Json
open scoped ProofWidgets.Json
#eval json% {
hello : "world",
cheese : ["edam", "cheddar", {kind : "spicy", rank : 100.2}],
lemonCount : 100e30,
isCool : true,
isBug : null,
lookACalc: $(23 + 54 * 2)
}
```

### Support for libraries

We have good support for building diagrams with [Penrose](https://penrose.cs.cmu.edu/), and expose
Expand Down
7 changes: 4 additions & 3 deletions lake-manifest.json
Original file line number Diff line number Diff line change
@@ -1,11 +1,12 @@
{"version": 5,
{"version": 6,
"packagesDir": "lake-packages",
"packages":
[{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "e8c27f7d90ee71470558efd1bc197fe55068c748",
"rev": "f91a64c789426debe48827ae6ef9efc8fa96bfcc",
"opts": {},
"name": "std",
"inputRev?": "main",
"inherited": false}}]}
"inherited": false}}],
"name": "proofwidgets"}

0 comments on commit 5382e38

Please sign in to comment.