Check-in [9c0eace5aa]

Not logged in

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

Overview
Comment:Some additional styles for rendering of derivations.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:9c0eace5aac265fd234ccae2a56be4fad6733781
User & Date: andy 2015-04-15 21:37:20
Context
2015-04-15
21:37
Updated to use the new inductive (vertical-bar) goal encoding. check-in: 5f036d068a user: andy tags: trunk
21:37
Some additional styles for rendering of derivations. check-in: 9c0eace5aa user: andy tags: trunk
21:36
Changed the encoding for inductive goals from \size to |size. The backslash was getting lost in the string encoding in some places. check-in: 23db977deb user: andy tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to res/base.css.

    40     40   
    41     41   table.rule caption {
    42     42     caption-side: left;
    43     43     vertical-align: middle;
    44     44     font-size: 10pt;
    45     45     margin-right: 2px;
    46     46     font-variant: small-caps;
           47  +  color: gray;
    47     48   }
    48     49   
    49     50   table.rule tr { 
    50     51     border: solid;
    51     52     border-width: 1px 0;
    52     53   }
    53     54   
................................................................................
    66     67   table.rule span.MathJax {
    67     68       margin-left: .5em;
    68     69       margin-right: .5em;
    69     70   }
    70     71   
    71     72   .premise, .conclusion {
    72     73     border-radius: 4px;
           74  +  cursor: default;
           75  +}
           76  +
           77  +.premise:hover, .conclusion:hover {
           78  +  background: #E3ECF2;
           79  +
           80  +  /* preventDefault in the event handler doesn't prevent Firefox from 
           81  +     selecting text on double-click. This does. */
           82  +  -moz-user-select: none;
           83  +}
           84  +
           85  +/* On disjunctive conclusions we inhibit hover highlighting, as this will be
           86  +   handled by the code. In the future, all highlighting will probably be 
           87  +   handled through code rather than through CSS. */
           88  +.conclusion.or:hover {
           89  +  background: inherit;
    73     90   }
    74     91   
    75     92   .rule-premise {
    76     93     margin-left: 1em;
    77     94     margin-right: 1em;
    78     95   }
    79     96   
................................................................................
    90    107     font-size: 12pt;
    91    108   }
    92    109   
    93    110   sub {
    94    111     vertical-align: sub;
    95    112     font-size: 10pt;
    96    113   }
          114  +
          115  +.ind-up, .ind-down {
          116  +  vertical-align: super;
          117  +  font-size: 10pt;
          118  +}
    97    119   
    98    120   .cline, .pline {
    99    121     line-height: 1.5;
   100    122   }
   101    123