Check-in [5ae5431e8f]

Not logged in

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

Overview
Comment:Fixed a few bugs in rendering of proofs (commas between antecedants, tabindexes on conclusions so they can be keyboard-focused).
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:5ae5431e8f8ddc5f6051ff16c43983da17039ee8
User & Date: andy 2015-04-16 21:59:28
Context
2015-04-16
21:59
Fixed a bug in fill that was duplicating _'s in the to-be-copied term. check-in: a992c2ca2e user: andy tags: trunk
21:59
Fixed a few bugs in rendering of proofs (commas between antecedants, tabindexes on conclusions so they can be keyboard-focused). check-in: 5ae5431e8f user: andy tags: trunk
2015-04-15
21:38
Fixed a bug in finding the subproofs of a case-type proof. check-in: f21f15e5e4 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to src/term_render.js.

376
377
378
379
380
381
382

383
384
385
386
387
388
389
...
390
391
392
393
394
395
396




397
398
399
400
401
402
403
                // to use custom styles for things like and, or, etc.
                chtml.addClass(conclusion.head);

                // Call the conclusion hook
                var conc = this.conclusionHook.call(conclusion, chtml, path);
                chtml = typeof conc !== "undefined" ? conc : chtml;
            }


            var entails = $("<span>&nbsp;\u22A2&nbsp;</span>");
            var conclusionLine = $("td",pr).eq(1);

            // If there are any, process the context
            if(context.length > 0) {
                var premiseHook = this.premiseHook;
................................................................................
                var renderGoal = _.bind(this.renderGoal,this);

                context.forEach(function(t,i) {
                    var premise = $(makeMath(renderGoal(t))).addClass("premise")
                    var prem = premiseHook.call(t, premise, path, i);
                    premise = typeof prem !== "undefined" ? prem : premise;
                    conclusionLine.append(premise);




                });

                conclusionLine.append(entails);
            }
            conclusionLine.append(chtml);

            // -------- Render the premises (subproofs) --------







>







 







>
>
>
>







376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
...
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
                // to use custom styles for things like and, or, etc.
                chtml.addClass(conclusion.head);

                // Call the conclusion hook
                var conc = this.conclusionHook.call(conclusion, chtml, path);
                chtml = typeof conc !== "undefined" ? conc : chtml;
            }
            chtml.attr("tabindex", 0); // Allow conclusion to receive focus

            var entails = $("<span>&nbsp;\u22A2&nbsp;</span>");
            var conclusionLine = $("td",pr).eq(1);

            // If there are any, process the context
            if(context.length > 0) {
                var premiseHook = this.premiseHook;
................................................................................
                var renderGoal = _.bind(this.renderGoal,this);

                context.forEach(function(t,i) {
                    var premise = $(makeMath(renderGoal(t))).addClass("premise")
                    var prem = premiseHook.call(t, premise, path, i);
                    premise = typeof prem !== "undefined" ? prem : premise;
                    conclusionLine.append(premise);

                    // Separate with commas
                    if(i !== context.length-1)
                      conclusionLine.append("<span>, </span>");
                });

                conclusionLine.append(entails);
            }
            conclusionLine.append(chtml);

            // -------- Render the premises (subproofs) --------