Check-in [0672529592]

Not logged in

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

Overview
Comment:Added support for rendering rule names next to rules (as table captions). Names are *not* rendered on rule applications in derivations, mostly because names are not stored in the proof tree.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:06725295929676a38593864b4067e6cf70ba227c
User & Date: andy 2015-04-14 21:05:07
Context
2015-04-15
11:12
Added some utilities for working with proof terms (extracting subproofs, getting proof goals, navigating through proofs on a path, etc.) check-in: e902cf4ec5 user: andy tags: trunk
2015-04-14
21:05
Added support for rendering rule names next to rules (as table captions). Names are *not* rendered on rule applications in derivations, mostly because names are not stored in the proof tree. check-in: 0672529592 user: andy tags: trunk
20:49
Added support for rendering inductive goals with the up/down arrows. check-in: 98ef3fd317 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to res/base.css.

33
34
35
36
37
38
39









40
41
42
43
44
45
46
/* Rules have a line between the top and bottom rows. */
table.rule {
  display: inline-table;
  border-collapse: collapse;
  margin: 8px 1em;
  vertical-align: bottom;
}









table.rule tr { 
  border: solid;
  border-width: 1px 0;
}

table.rule tr:first-child {
  border-top: none;







>
>
>
>
>
>
>
>
>







33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
/* Rules have a line between the top and bottom rows. */
table.rule {
  display: inline-table;
  border-collapse: collapse;
  margin: 8px 1em;
  vertical-align: bottom;
}

table.rule caption {
  caption-side: left;
  vertical-align: middle;
  font-size: 10pt;
  margin-right: 2px;
  font-variant: small-caps;
}

table.rule tr { 
  border: solid;
  border-width: 1px 0;
}

table.rule tr:first-child {
  border-top: none;

Changes to src/term_render.js.

155
156
157
158
159
160
161

162
163
164
165
166
167
168
...
323
324
325
326
327
328
329

330
331
332
333
334
335
336
            var head = t.body[1];
            var body = terms.toArray(t.body[2].body[0]);

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

            var rule = $("<table class='rule'>" + 

                           "<tr class='pline'><td></td></tr>" + 
                           "<tr class='cline'><td></td></tr></table>");

            // If the only element of the body is "true", then the rule is an
            // axiom and we don't put anything above the line
            if(!(body.length == 1 && body[0].isAtom() && body[0].head === 'true')) {
                // For each premise, append it to the first row of the table
................................................................................
                return $("<span>?</span>");

            var context = terms.toArray(t.body[1]);
            var subproofs = getSubProofs(t);
            var rulename = getProofName(t);

            var proof = $('<span><table class="rule proof tab">' + 

                            '<tr class="pline"><td></td></tr>' +
                            '<tr class="cline"><td></td></tr>' +
                          '</table></span>');

            // -------- Construct conclusion line --------
            // Render conclusion, and call the hook for it.
            conclusion = $(makeMath(this.renderGoal(conclusion))).addClass("conclusion");







>







 







>







155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
...
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
            var head = t.body[1];
            var body = terms.toArray(t.body[2].body[0]);

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

            var rule = $("<table class='rule'>" + 
                           "<caption>" + name + "</caption>" +
                           "<tr class='pline'><td></td></tr>" + 
                           "<tr class='cline'><td></td></tr></table>");

            // If the only element of the body is "true", then the rule is an
            // axiom and we don't put anything above the line
            if(!(body.length == 1 && body[0].isAtom() && body[0].head === 'true')) {
                // For each premise, append it to the first row of the table
................................................................................
                return $("<span>?</span>");

            var context = terms.toArray(t.body[1]);
            var subproofs = getSubProofs(t);
            var rulename = getProofName(t);

            var proof = $('<span><table class="rule proof tab">' + 
                            //<caption>RuleName</caption>
                            '<tr class="pline"><td></td></tr>' +
                            '<tr class="cline"><td></td></tr>' +
                          '</table></span>');

            // -------- Construct conclusion line --------
            // Render conclusion, and call the hook for it.
            conclusion = $(makeMath(this.renderGoal(conclusion))).addClass("conclusion");