the next generation of the in-browser educational proof assistant
1
fork

Configure Feed

Select the types of activity you want to include in your feed.

improve hoterm application rendering

Mio 35141915 29f63f2a

+20 -13
+20 -13
src/HOTermView.res
··· 1 - type props = {term: HOTerm.t, scope: array<string>} 2 1 open Util 3 2 type idx_props = {idx: int, scope: array<string>} 4 3 let viewVar = (props: idx_props) => ··· 33 32 [React.string(" "), e] 34 33 } 35 34 ) 36 - 35 + type props1 = {term: HOTerm.t, scope: array<string>, brackets: bool} 37 36 @react.componentWithProps 38 - let rec make = ({term, scope}) => 37 + let rec make1 = ({term, scope, brackets}) => 39 38 switch term { 40 39 | Var({idx}) => viewVar({idx, scope}) 41 40 | Symbol({name: s}) => <span className="term-const"> {React.string(s)} </span> ··· 48 47 switch HOTerm.strip(term) { 49 48 | (Symbol({name: "="}), args) if Array.length(args) == 2 => 50 49 <span className="term-equality"> 51 - {React.createElement(make, {term: args->Array.getUnsafe(0), scope})} 50 + {React.createElement(make1, {term: args->Array.getUnsafe(0), scope, brackets: true})} 52 51 {React.string("=")} 53 - {React.createElement(make, {term: args->Array.getUnsafe(1), scope})} 52 + {React.createElement(make1, {term: args->Array.getUnsafe(1), scope, brackets: true})} 54 53 </span> 55 54 | (func, args) => 56 - <span className="term-app"> 57 - {React.createElement(make, {term: func, scope})} 58 - <span className="term-app-telescope"> 59 - {args 60 - ->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i))) 55 + let xs = Array.concat([func], args) 56 + let a = 57 + <span className="term-app"> 58 + {xs 59 + ->Array.mapWithIndex((t, i) => 60 + React.createElement(make1, withKey({term: t, scope, brackets: true}, i)) 61 + ) 61 62 ->intersperse 62 - ->parenthesise 63 63 ->React.array} 64 64 </span> 65 - </span> 65 + if brackets { 66 + [a]->parenthesise->React.array 67 + } else { 68 + a 69 + } 66 70 } 67 71 | Lam({name, body}) => { 68 72 let newScope = Array.concat([name], scope) 69 73 <span className="term-lambda"> 70 74 {React.string(name)} 71 - {React.createElement(make, {term: body, scope: newScope})} 75 + {React.createElement(make1, {term: body, scope: newScope, brackets: false})} 72 76 </span> 73 77 } 74 78 | Unallowed => <p> {React.string("Internal error: unallowed")} </p> 75 79 } 80 + type props = {term: HOTerm.t, scope: array<string>} 81 + @react.componentWithProps 82 + let make = ({term, scope}) => make1({term, scope, brackets: false})