Check-in [98ef3fd317]

Not logged in

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

Overview
Comment:Added support for rendering inductive goals with the up/down arrows.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:98ef3fd3178e3c09487cf6b5dc238903645bd770
User & Date: andy 2015-04-14 20:49:15
Context
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
20:21
Added a specialized version of the nat specification, for demonstration purposes. check-in: 4a035bbfc0 user: andy tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to src/term_render.js.

    57     57           // rendering itself.
    58     58           function makeMath(s,display) {
    59     59               var element = display ? $("<div></div>") : $("<span></span>");
    60     60               element.html(s);
    61     61   
    62     62               return element;
    63     63           }
           64  +
           65  +        // Render the head of a compound. All this does is check for the 
           66  +        // presence of a trailing \sml or \big and render the head as 
           67  +        // inductive, as appropriate.
           68  +        function renderHead(h) {
           69  +            var m;
           70  +            if(m = h.match(/(.+)\\big$/))
           71  +                return m[1] + "<span class='ind-up'>&uarr;</span>";
           72  +            else if(m = h.match(/(.+)\\sml$/))
           73  +                return m[1] + "<span class='ind-down'>&darr;</span>";
           74  +            else
           75  +                return h; // Nothing special
           76  +        }
    64     77   
    65     78           this.renderTerm = function(t,isgoal) {
    66     79   
    67     80               function render(t,isgoal) {
    68     81   
    69     82                   switch(t.tt()) {
    70     83                       case 'compound':
................................................................................
   108    121                               var args = t.body.map(render);
   109    122   
   110    123                               if(t.head in specialNames) {
   111    124                                   // Render children+operator using the special name
   112    125                                   return specialNames[t.head](args);
   113    126                               }
   114    127                               else {
          128  +                                var head = renderHead(t.head);
   115    129                                   var cls = isgoal === true ? 'goal' : 'comp';
   116    130   
   117         -                                return "<span class='" + cls + "'>" + t.head + 
          131  +                                return "<span class='" + cls + "'>" + head + 
   118    132                                       "</span>(" + args.join(", ") + ")";
   119    133                               }
   120    134                           }
   121    135   
   122    136                       // Variables are rendered in bold.
   123    137                       case 'variable':
   124    138                           return "<span class='var'>" + renderName(t.name) + "</span>";
................................................................................
   221    235            *   conclusionHook -- The same, but for the conclusion.
   222    236            *
   223    237            * Note that you have to pass a target element, which *must* already
   224    238            * be part of the document, because jQuery/FireFox have trouble 
   225    239            * constructing nested tables on un-inserted elements. Eventually this
   226    240            * will be remedied by using divs with CSS table layout classes.
   227    241            */
   228         -        this.renderProof = function(t) {
   229         -
   230         -            var renderProof = _.bind(this.renderProof,this);
          242  +        this.renderProof = function(t, path) {
          243  +            path = path === undefined ? [] : path;
   231    244   
   232    245               // Get the human-readable name of a derivation step (rule)
   233    246               function getProofName(proof) {
   234    247                   var t = proof.body[3].head;
   235    248                   if(t !== "case")
   236    249                       return {
   237    250                           trivial : "\u22A4-R",
................................................................................
   317    330                               '<tr class="pline"><td></td></tr>' +
   318    331                               '<tr class="cline"><td></td></tr>' +
   319    332                             '</table></span>');
   320    333   
   321    334               // -------- Construct conclusion line --------
   322    335               // Render conclusion, and call the hook for it.
   323    336               conclusion = $(makeMath(this.renderGoal(conclusion))).addClass("conclusion");
   324         -            var conc = this.conclusionHook(conclusion);
          337  +            var conc = this.conclusionHook(conclusion, path);
   325    338               conclusion = typeof conc !== "undefined" ? conc : conclusion;
   326    339   
   327    340               var entails = $("<span>&nbsp;\u22A2&nbsp;</span>");
   328    341               var conclusionLine = $("td",proof).eq(1);
   329    342   
   330    343               // If there are any, process the context
   331    344               if(context.length > 0) {
   332         -                var premiseHook = this.premiseHook;
          345  +                var premiseHook = _.bind(this.premiseHook, this);
   333    346                   context.forEach(function(t) {
   334    347                       var premise = $(makeMath(renderGoal(t))).addClass("premise")
   335         -                    var prem = premiseHook(premise);
          348  +                    var prem = premiseHook(premise, path);
   336    349                       premise = typeof prem !== "undefined" ? prem : 
   337    350                       conclusionLine.append(premise);
   338    351                   });
   339    352   
   340    353                   conclusionLine.append(entails);
   341    354               }
   342    355               conclusionLine.append(conclusion);
   343    356   
   344    357               // -------- Render the premises (subproofs) --------
   345    358               var premiseLine = $("td",proof).eq(0);
   346    359               if(subproofs.length > 0) {
   347    360                   // Render all sub-proofs, add to premises
   348         -                subproofs.forEach(function(p) {
   349         -                    premiseLine.append(renderProof(p));
          361  +                var renderProof = _.bind(this.renderProof,this);
          362  +                subproofs.forEach(function(p,i) {
          363  +                    var newpath = path.concat(i);
          364  +                    premiseLine.append(renderProof(p, newpath));
   350    365                   });
   351    366               }
   352    367               else
   353    368                   premiseLine.html("&nbsp;"); // Axiomatic
   354    369   
   355    370               return proof;
   356    371           }