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 Side-by-Side Diffs Ignore Whitespace Patch

Changes to res/base.css.

    33     33   /* Rules have a line between the top and bottom rows. */
    34     34   table.rule {
    35     35     display: inline-table;
    36     36     border-collapse: collapse;
    37     37     margin: 8px 1em;
    38     38     vertical-align: bottom;
    39     39   }
           40  +
           41  +table.rule caption {
           42  +  caption-side: left;
           43  +  vertical-align: middle;
           44  +  font-size: 10pt;
           45  +  margin-right: 2px;
           46  +  font-variant: small-caps;
           47  +}
           48  +
    40     49   table.rule tr { 
    41     50     border: solid;
    42     51     border-width: 1px 0;
    43     52   }
    44     53   
    45     54   table.rule tr:first-child {
    46     55     border-top: none;

Changes to src/term_render.js.

   155    155               var head = t.body[1];
   156    156               var body = terms.toArray(t.body[2].body[0]);
   157    157   
   158    158               var renderTerm = _.bind(this.renderTerm,this);
   159    159               var renderGoal = _.bind(this.renderGoal,this);
   160    160   
   161    161               var rule = $("<table class='rule'>" + 
          162  +                           "<caption>" + name + "</caption>" +
   162    163                              "<tr class='pline'><td></td></tr>" + 
   163    164                              "<tr class='cline'><td></td></tr></table>");
   164    165   
   165    166               // If the only element of the body is "true", then the rule is an
   166    167               // axiom and we don't put anything above the line
   167    168               if(!(body.length == 1 && body[0].isAtom() && body[0].head === 'true')) {
   168    169                   // For each premise, append it to the first row of the table
................................................................................
   323    324                   return $("<span>?</span>");
   324    325   
   325    326               var context = terms.toArray(t.body[1]);
   326    327               var subproofs = getSubProofs(t);
   327    328               var rulename = getProofName(t);
   328    329   
   329    330               var proof = $('<span><table class="rule proof tab">' + 
          331  +                            //<caption>RuleName</caption>
   330    332                               '<tr class="pline"><td></td></tr>' +
   331    333                               '<tr class="cline"><td></td></tr>' +
   332    334                             '</table></span>');
   333    335   
   334    336               // -------- Construct conclusion line --------
   335    337               // Render conclusion, and call the hook for it.
   336    338               conclusion = $(makeMath(this.renderGoal(conclusion))).addClass("conclusion");