Skip to content

Commit 2326189

Browse files
committed
Minor Changes
1 parent cb6e601 commit 2326189

2 files changed

Lines changed: 13 additions & 22 deletions

File tree

‎playground/index.md‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ description: Try LiquidJava refinements and typestates directly in your browser.
88

99
# Playground
1010

11-
Edit an example and select **Verify** to check it with LiquidJava. Verification runs in your browser; your code is not sent to a server. The first check downloads the verifier and may take a moment.
11+
Run the LiquidJava verification directly in your browser. Edit an example and select **Verify**.
1212

1313
<link rel="stylesheet" href="{{ '/playground/editor.css' | relative_url }}">
1414
<div id="lj-playground" class="lj-playground" data-runtime="{{ '/playground/runtime/' | relative_url }}">
@@ -23,7 +23,7 @@ Edit an example and select **Verify** to check it with LiquidJava. Verification
2323
<option value="state">Object states</option>
2424
</select>
2525
</div>
26-
<button id="lj-reset" type="button">Reset example</button>
26+
<button id="lj-reset" type="button">Reset</button>
2727
</div>
2828
<button id="lj-verify" type="button" disabled>Verify</button>
2929
</div>
@@ -35,6 +35,4 @@ Edit an example and select **Verify** to check it with LiquidJava. Verification
3535
<noscript>Enable JavaScript to use the playground.</noscript>
3636
</div>
3737

38-
The playground checks one Java file using Java 8 syntax, with the bundled LiquidJava annotations and core Java types. External dependencies are not supported. For projects, use the [VS Code extension]({{ '/vscode-extension/' | relative_url }}).
39-
4038
<script type="module" src="{{ '/playground/runtime/editor.js' | relative_url }}"></script>

‎scripts/playground/examples.mjs‎

Lines changed: 11 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,57 +1,50 @@
11
export const examples = {
2-
positive: `import liquidjava.specification.Refinement;
2+
positive: `import liquidjava.specification.*;
33
44
class Example {
55
void positiveNumbers() {
66
@Refinement("_ > 0")
7-
int count = 5;
8-
9-
// try changing 5 to -1
7+
int count = -1;
108
}
119
}
1210
`,
13-
bounds: `import liquidjava.specification.Refinement;
11+
bounds: `import liquidjava.specification.*;
1412
1513
class Example {
1614
void setPercentage(@Refinement("_ >= 0 && _ <= 100") int percentage) {}
1715
1816
void demo() {
19-
setPercentage(75);
20-
// try changing 75 to 150
17+
setPercentage(125);
2118
}
2219
}
2320
`,
24-
alias: `import liquidjava.specification.Refinement;
25-
import liquidjava.specification.RefinementAlias;
21+
alias: `import liquidjava.specification.*;
2622
2723
@RefinementAlias("Positive(int x) { x > 0 }")
2824
class Example {
2925
void demo() {
3026
@Refinement("Positive(_)")
31-
int amount = 10;
32-
// try changing 10 to 0
27+
int amount = 0;
3328
}
3429
}
3530
`,
36-
state: `import liquidjava.specification.StateSet;
37-
import liquidjava.specification.StateRefinement;
31+
state: `import liquidjava.specification.*;
3832
3933
@StateSet({"open", "closed"})
4034
class Example {
41-
@StateRefinement(to = "open(this)")
35+
@StateRefinement(to="open(this)")
4236
Example() {}
4337
44-
@StateRefinement(from = "open(this)", to = "closed(this)")
38+
@StateRefinement(from="open(this)", to="closed(this)")
4539
void close() {}
4640
47-
@StateRefinement(from = "open(this)")
41+
@StateRefinement(from="open(this)")
4842
void read() {}
4943
5044
static void demo() {
5145
Example resource = new Example();
52-
resource.read();
5346
resource.close();
54-
// try adding resource.read() after close()
47+
resource.read();
5548
}
5649
}
5750
`

0 commit comments

Comments
 (0)