Check-in [8cf949cd23]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Better rendering of goals vs. terms. Subgoals of AND, OR, and IMP are now rendered as goals rather than terms.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:8cf949cd23395db9adf86b4bac304f3e39e241a2
User & Date: andy 2015-04-14 14:00:20
Context
2015-04-14
14:00
Latest build results. check-in: b0c341eb78 user: andy tags: trunk
14:00
Better rendering of goals vs. terms. Subgoals of AND, OR, and IMP are now rendered as goals rather than terms. check-in: 8cf949cd23 user: andy tags: trunk
13:51
The REPL example now uses the client-side parser to check inputs for syntactical correctness. check-in: 0ce4e1a109 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to src/term_render.js.

58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
..
87
88
89
90
91
92
93


94
95
96
97







98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
...
117
118
119
120
121
122
123



124
125
126
127
128
129
130
        function makeMath(s,display) {
            var element = display ? $("<div></div>") : $("<span></span>");
            element.html(s);

            return element;
        }

        this.renderGoal = function(t) { return this.renderTerm(t,true); }

        this.renderTerm = function(t,isgoal) {

            function render(t,isgoal) {

                switch(t.tt()) {
                    case 'compound':
                        if(t.isAtom()) {
................................................................................
                                return "[" + 
                                       l.map(render).join(", ") +
                                       "]";
                            }
                            else if(t.head === "and" || t.head === "or") {
                                // As do AND and OR
                                var l = terms.toArray(t.body[0]);


                                args = l.map(render);

                                return specialNames[t.head](args);
                            }








                            // Else, render as a normal term:
                            // Render children
                            var args = t.body.map(render);

                            if(t.head in specialNames) {
                                // Render children+operator using the special name
                                return specialNames[t.head](args);
                            }
                            else {
                                var cls = isgoal ? 'goal' : 'comp';

                                return "<span class='" + cls + "'>" + t.head + 
                                    "</span>(" + args.join(", ") + ")";
                            }
                        }

                    // Variables are rendered in bold.
................................................................................
                        return "<span class='var'>" + renderName(t.name) + "</span>";
                }
            }

            return render(t,isgoal);
        }




        // Rules are terms of the form
        //   rule(Name,Head,and([body...]))
        //     ih(Name,Head,and([body...]))
        // They are rendered as tables with the head on the bottom row and 
        // the elements of the body on top
        this.renderRule = function(t) {
            var name = t.body[0];







<
<







 







>
>
|



>
>
>
>
>
>
>










|







 







>
>
>







58
59
60
61
62
63
64


65
66
67
68
69
70
71
..
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
...
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
        function makeMath(s,display) {
            var element = display ? $("<div></div>") : $("<span></span>");
            element.html(s);

            return element;
        }



        this.renderTerm = function(t,isgoal) {

            function render(t,isgoal) {

                switch(t.tt()) {
                    case 'compound':
                        if(t.isAtom()) {
................................................................................
                                return "[" + 
                                       l.map(render).join(", ") +
                                       "]";
                            }
                            else if(t.head === "and" || t.head === "or") {
                                // As do AND and OR
                                var l = terms.toArray(t.body[0]);

                                // Render subgoals as goals
                                args = l.map(_.bind(render,this,_,true));

                                return specialNames[t.head](args);
                            }
                            else if(t.head === "->") {
                              // Implication
                              var l = render(t.body[0],true);
                              var r = render(t.body[1],true);

                              return specialNames[t.head]([l,r]);
                            }

                            // Else, render as a normal term:
                            // Render children
                            var args = t.body.map(render);

                            if(t.head in specialNames) {
                                // Render children+operator using the special name
                                return specialNames[t.head](args);
                            }
                            else {
                                var cls = isgoal === true ? 'goal' : 'comp';

                                return "<span class='" + cls + "'>" + t.head + 
                                    "</span>(" + args.join(", ") + ")";
                            }
                        }

                    // Variables are rendered in bold.
................................................................................
                        return "<span class='var'>" + renderName(t.name) + "</span>";
                }
            }

            return render(t,isgoal);
        }


        this.renderGoal = _.bind(this.renderTerm,this,_,true);

        // Rules are terms of the form
        //   rule(Name,Head,and([body...]))
        //     ih(Name,Head,and([body...]))
        // They are rendered as tables with the head on the bottom row and 
        // the elements of the body on top
        this.renderRule = function(t) {
            var name = t.body[0];