the next generation of the in-browser educational proof assistant
fixed some react weirdities
+47
-25
+21
-8
src/Editable.res
+21
-8
src/Editable.res
···
20
20
21
21
module type COMPONENT = {
22
22
module Ports : PORTS
23
-
type props = { content: string, imports: Ports.t, onChange: (string,~exports:Ports.t) => () }
23
+
type props = { content: string, imports: Ports.t, onChange: (string,~exports:Ports.t) => (), onLoad: (~exports:Ports.t) => () }
24
24
let make : props => React.element
25
-
let
26
25
}
27
26
28
27
module Config = (
···
47
46
let onChange= (e) => {
48
47
let target = JsxEvent.Form.target(e)
49
48
let value: string = target["value"]
50
-
setStyle(_ => deserialise(value))
51
-
props.onChange(value,~exports={Ports.facts: Dict.make(), ruleStyle:Some(style)})
49
+
let sty = deserialise(value)
50
+
setStyle(_ => sty)
51
+
52
+
props.onChange(value,~exports={Ports.facts: Dict.make(), ruleStyle:Some(sty)})
52
53
}
53
54
[Gentzen,Linear,Hybrid]->Array.map(n =>
54
55
<input type_="radio" id={"style_"->String.concat(String.make(n))} name="style" onChange value={String.make(n)} checked={style==n}/>
···
141
142
let make = (props ) => {
142
143
switch deserialise(props.content) {
143
144
| Ok(s) => {
144
-
props.onLoad(~exports= {Ports.facts: s, ruleStyle: None});
145
+
React.useEffect(() => {
146
+
// Run effects
147
+
props.onLoad(~exports= {Ports.facts: s, ruleStyle: None});
148
+
None // or Some(() => {})
149
+
}, [])
150
+
145
151
<div className={"axiom-set axiom-set-"->String.concat(String.make(props.imports.ruleStyle->Option.getOr(Hybrid)))}>
146
-
{ Dict.toArray(s)->Array.map(((n,r)) =>
147
-
<RuleView rule={r} scope={[]} style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
152
+
{ Dict.toArray(s)->Array.mapWithIndex(((n,r), i) =>
153
+
<RuleView rule={r} scope={[]} key={String.make(i)} style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
148
154
{React.string(n)}
149
155
//<Name content={n} onChange={(_) => Error("BLAH!")} />
150
156
</RuleView>)
···
152
158
}
153
159
</div>
154
160
}
155
-
| Error(e) => <div className="error"> {React.string(e)} </div>
161
+
| Error(e) => {
162
+
React.useEffect(() => {
163
+
// Run effects
164
+
props.onLoad(~exports= {Ports.facts: Dict.make(), ruleStyle: None});
165
+
None // or Some(() => {})
166
+
}, [])
167
+
<div className="error"> {React.string(e)} </div>
168
+
}
156
169
}
157
170
}
158
171
}
+1
-1
src/Method.res
+1
-1
src/Method.res
+7
-6
src/RuleView.res
+7
-6
src/RuleView.res
···
1
1
open Signatures
2
+
open Util
2
3
type style = Gentzen | Linear | Hybrid
3
4
module Make = (
4
5
Term : TERM,
···
29
30
{if Array.length(arr) > 0 { <span className="rule-binders">{React.array(arr)}</span> }
30
31
else { React.string("") }}
31
32
{React.array(premises
32
-
->Array.map(p=><span className="rule-context">
33
-
{make({rule:p, scope,children:React.string(""),style:props.style})}</span>)
33
+
->Array.mapWithIndex((p,i)=><span className="rule-context">
34
+
{React.createElement(make,withKey({rule:p, scope,children:React.string(""),style:props.style}, i))}</span>)
34
35
->Array.flatMapWithIndex( (e, i) =>
35
36
if i == 0 {
36
37
[e]
···
55
56
let arr = vars->Array.map(JudgmentView.TermView.makeMeta)
56
57
Array.reverse(arr)
57
58
let scope = vars->Array.concat(props.scope->Option.getOr([]))
58
-
<table className="inference">
59
+
<table className="inference"><tbody>
59
60
<tr><td className="rule-cell rule-binderbox" rowSpan=3>{React.array(arr)}</td>
60
61
{React.array(premises->Array.map(p=>
61
62
<td className="rule-cell rule-premise">
···
77
78
<td colSpan={premises->Array.length + 1} className="rule-cell rule-hypothetical-conclusion">
78
79
<JudgmentView judgment={conclusion} scope={scope} />
79
80
</td>
80
-
</tr></table>
81
+
</tr></tbody></table>
81
82
}
82
83
}
83
84
module TopLevel = (Premise : RULE_COMPONENT) => {
···
86
87
let arr = vars->Array.map(JudgmentView.TermView.makeMeta)
87
88
Array.reverse(arr)
88
89
let scope = vars->Array.concat(props.scope->Option.getOr([]))
89
-
<div className="axiom"><table className="inference">
90
+
<div className="axiom"><table className="inference"><tbody>
90
91
<tr><td className="rule-cell rule-binderbox" rowSpan=2>{React.array(arr)}</td>
91
92
{React.array(premises->Array.map(p=>
92
93
<td className="rule-cell rule-premise">
···
105
106
<td colSpan={premises->Array.length + 1} className="rule-cell rule-conclusion">
106
107
<JudgmentView judgment={conclusion} scope={scope} />
107
108
</td>
108
-
</tr></table></div>
109
+
</tr></tbody></table></div>
109
110
}
110
111
}
111
112
module Gentzen = TopLevel(Hypothetical(Inline))
+10
-7
src/SExpView.res
+10
-7
src/SExpView.res
···
1
1
type props = {term: SExp.t, scope: array<string>}
2
-
3
-
let viewVar = (idx, scope:array<string>) => switch scope[idx] {
4
-
| Some(n) if Array.indexOf(scope,n) == idx =>
2
+
open Util
3
+
type idx_props = {idx:int, scope:array<string>}
4
+
let viewVar = (props : idx_props) => switch props.scope[props.idx] {
5
+
| Some(n) if Array.indexOf(props.scope,n) == props.idx =>
5
6
<span className="term-metavar">
6
7
{ React.string(n)}
7
8
</span>
8
9
| _ =>
9
10
<span className="term-metavar-unnamed">
10
-
{React.string("\\")} { React.int(idx) }
11
+
{React.string("\\")} { React.int(props.idx) }
11
12
</span>
12
13
}
13
14
···
28
29
29
30
let intersperse = (a) =>
30
31
a->Array.flatMapWithIndex((e, i) => if i == 0 { [e] } else { [React.string(" "),e] })
32
+
31
33
32
34
@react.componentWithProps
33
35
let rec make = ({term, scope}) => switch term {
34
36
| Compound({subexps:bits}) => {
35
37
<span className="term-compound">
36
38
{bits
37
-
->Array.map(t => make({term:t,scope}))
39
+
->Array.mapWithIndex( (t, i) =>
40
+
React.createElement(make,withKey({term:t,scope },i)))
38
41
->intersperse->parenthesise->React.array}
39
42
</span>
40
43
}
41
-
| Var({idx:idx}) => viewVar(idx,scope)
44
+
| Var({idx:idx}) => viewVar({idx,scope})
42
45
| Symbol({name:s}) => <span className="term-const"> { React.string(s) } </span>
43
46
| Schematic({schematic:s, allowed:vs}) =>
44
47
<span className="term-schematic">
45
48
{React.string("?")} {React.int(s)}
46
49
<span className="term-schematic-telescope">
47
50
{vs
48
-
->Array.map(v => viewVar(v,scope))
51
+
->Array.mapWithIndex( (v,i) => React.createElement(viewVar, withKey({idx:v,scope},i)))
49
52
->intersperse->parenthesise->React.array}
50
53
</span>
51
54
</span>
+3
-3
src/Scratch.res
+3
-3
src/Scratch.res
···
1
1
open Editable
2
2
open Method
3
-
4
-
module AxiomS = TextAreaEditor(AxiomSet(SExp,SExp,SExpJView))
3
+
open Util
4
+
module AxiomS = AxiomSet(SExp,SExp,SExpJView)
5
5
module DerivationsOrLemmas = Combine(SExp,SExp,Derivation(SExp,SExp),Lemma(SExp,SExp))
6
-
module TheoremS = TextAreaEditor(Theorem(SExp,SExp,SExpJView,DerivationsOrLemmas))
6
+
module TheoremS = Theorem(SExp,SExp,SExpJView,DerivationsOrLemmas)
7
7
module Conf = Config(SExp,SExp)
8
8
//module RuleSExpTE = RuleSetSB(SExp,SExp,SExpJView)
9
9
//module RuleSExpView = WithTextArea(RuleSExpTE)