Admin/Mercurial/isabelle-style-1.3.1.diff
author wenzelm
Fri Nov 03 19:20:47 2017 +0100 (19 months ago)
changeset 66997 17eb23e43630
parent 42431 79ef651d88eb
permissions -rw-r--r--
avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0;
krauss@42431
     1
diff -Naur gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
krauss@42431
     2
--- gitweb/changelogentry.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
     3
+++ isabelle/changelogentry.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
     4
@@ -1,14 +1,12 @@
krauss@42431
     5
 <div>
krauss@42431
     6
-<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age} ago</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
krauss@42431
     7
-</div>
krauss@42431
     8
-<div class="title_text">
krauss@42431
     9
-<div class="log_link">
krauss@42431
    10
-<a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
krauss@42431
    11
-</div>
krauss@42431
    12
-<i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
krauss@42431
    13
+<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
krauss@42431
    14
+{author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
krauss@42431
    15
 </div>
krauss@42431
    16
 <div class="log_body">
krauss@42431
    17
 {desc|strip|escape|addbreaks|nonempty}
krauss@42431
    18
 <br/>
krauss@42431
    19
+<div class="files">
krauss@42431
    20
+{files}
krauss@42431
    21
+</div>
krauss@42431
    22
 <br/>
krauss@42431
    23
 </div>
krauss@42431
    24
diff -Naur gitweb/changeset.tmpl isabelle/changeset.tmpl
krauss@42431
    25
--- gitweb/changeset.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    26
+++ isabelle/changeset.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    27
@@ -29,7 +29,7 @@
krauss@42431
    28
 <div class="title_text">
krauss@42431
    29
 <table cellspacing="0">
krauss@42431
    30
 <tr><td>author</td><td>{author|obfuscate}</td></tr>
krauss@42431
    31
-<tr><td></td><td>{date|date} ({date|age} ago)</td></tr>
krauss@42431
    32
+<tr><td></td><td>{date|date} ({date|age})</td></tr>
krauss@42431
    33
 {branch%changesetbranch}
krauss@42431
    34
 <tr><td>changeset {rev}</td><td style="font-family:monospace">{node|short}</td></tr>
krauss@42431
    35
 {parent%changesetparent}
krauss@42431
    36
diff -Naur gitweb/fileannotate.tmpl isabelle/fileannotate.tmpl
krauss@42431
    37
--- gitweb/fileannotate.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    38
+++ isabelle/fileannotate.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    39
@@ -36,7 +36,7 @@
krauss@42431
    40
  <td>{author|obfuscate}</td></tr>
krauss@42431
    41
 <tr>
krauss@42431
    42
  <td></td>
krauss@42431
    43
- <td>{date|date} ({date|age} ago)</td></tr>
krauss@42431
    44
+ <td>{date|date} ({date|age})</td></tr>
krauss@42431
    45
 {branch%filerevbranch}
krauss@42431
    46
 <tr>
krauss@42431
    47
  <td>changeset {rev}</td>
krauss@42431
    48
diff -Naur gitweb/filerevision.tmpl isabelle/filerevision.tmpl
krauss@42431
    49
--- gitweb/filerevision.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    50
+++ isabelle/filerevision.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    51
@@ -36,7 +36,7 @@
krauss@42431
    52
  <td>{author|obfuscate}</td></tr>
krauss@42431
    53
 <tr>
krauss@42431
    54
  <td></td>
krauss@42431
    55
- <td>{date|date} ({date|age} ago)</td></tr>
krauss@42431
    56
+ <td>{date|date} ({date|age})</td></tr>
krauss@42431
    57
 {branch%filerevbranch}
krauss@42431
    58
 <tr>
krauss@42431
    59
  <td>changeset {rev}</td>
krauss@42431
    60
diff -Naur gitweb/graph.tmpl isabelle/graph.tmpl
krauss@42431
    61
--- gitweb/graph.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    62
+++ isabelle/graph.tmpl	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    63
@@ -63,7 +63,7 @@
krauss@42431
    64
 var revlink = '<li style="_STYLE"><span class="desc">';
krauss@42431
    65
 revlink += '<a class="list" href="{url}rev/_NODEID{sessionvars%urlparameter}" title="_NODEID"><b>_DESC</b></a>';
krauss@42431
    66
 revlink += '</span> _TAGS';
krauss@42431
    67
-revlink += '<span class="info">_DATE ago, by _USER</span></li>';
krauss@42431
    68
+revlink += '<span class="info">_DATE, by _USER</span></li>';
krauss@42431
    69
 
krauss@42431
    70
 graph.vertex = function(x, y, color, parity, cur) {
krauss@42431
    71
 	
krauss@42431
    72
diff -Naur gitweb/map isabelle/map
krauss@42431
    73
--- gitweb/map	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    74
+++ isabelle/map	2011-04-20 12:13:37.000000000 +0200
krauss@42431
    75
@@ -78,7 +78,7 @@
krauss@42431
    76
   <tr style="font-family:monospace" class="parity{parity}">
krauss@42431
    77
     <td class="linenr" style="text-align: right;">
krauss@42431
    78
       <a href="{url}annotate/{node|short}/{file|urlescape}{sessionvars%urlparameter}#l{targetline}"
krauss@42431
    79
-         title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
krauss@42431
    80
+         title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
krauss@42431
    81
     </td>
krauss@42431
    82
     <td><pre><a class="linenr" href="#{lineid}" id="{lineid}">{linenumber}</a></pre></td>
krauss@42431
    83
     <td><pre>{line|escape}</pre></td>
krauss@42431
    84
@@ -150,7 +150,7 @@
krauss@42431
    85
 tags = tags.tmpl
krauss@42431
    86
 tagentry = '
krauss@42431
    87
   <tr class="parity{parity}">
krauss@42431
    88
-    <td class="age"><i>{date|age} ago</i></td>
krauss@42431
    89
+    <td class="age"><i>{date|age}</i></td>
krauss@42431
    90
     <td><a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}"><b>{tag|escape}</b></a></td>
krauss@42431
    91
     <td class="link">
krauss@42431
    92
       <a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a> |
krauss@42431
    93
@@ -161,7 +161,7 @@
krauss@42431
    94
 branches = branches.tmpl
krauss@42431
    95
 branchentry = '
krauss@42431
    96
   <tr class="parity{parity}">
krauss@42431
    97
-    <td class="age"><i>{date|age} ago</i></td>
krauss@42431
    98
+    <td class="age"><i>{date|age}</i></td>
krauss@42431
    99
     <td><a class="list" href="{url}shortlog/{node|short}{sessionvars%urlparameter}"><b>{node|short}</b></a></td>
krauss@42431
   100
     <td class="{status}">{branch|escape}</td>
krauss@42431
   101
     <td class="link">
krauss@42431
   102
@@ -204,11 +204,12 @@
krauss@42431
   103
 inbranchtag = '<span class="inbranchtag" title="{name}">{name}</span> '
krauss@42431
   104
 shortlogentry = '
krauss@42431
   105
   <tr class="parity{parity}">
krauss@42431
   106
-    <td class="age"><i>{date|age} ago</i></td>
krauss@42431
   107
+    <td class="age"><i>{date|age}</i></td>
krauss@42431
   108
     <td><i>{author|person}</i></td>
krauss@42431
   109
+    <td><i>{date|shortdate}</i></td>
krauss@42431
   110
     <td>
krauss@42431
   111
       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
krauss@42431
   112
-        <b>{desc|strip|firstline|escape|nonempty}</b>
krauss@42431
   113
+        <b>{desc|strip|escape|nonempty}</b>
krauss@42431
   114
         <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span>
krauss@42431
   115
       </a>
krauss@42431
   116
     </td>
krauss@42431
   117
@@ -219,10 +220,12 @@
krauss@42431
   118
   </tr>'
krauss@42431
   119
 filelogentry = '
krauss@42431
   120
   <tr class="parity{parity}">
krauss@42431
   121
-    <td class="age"><i>{date|age} ago</i></td>
krauss@42431
   122
+    <td class="age"><i>{date|age}</i></td>
krauss@42431
   123
+    <td><i>{author|person}</i></td>
krauss@42431
   124
+    <td><i>{date|shortdate}</i></td>
krauss@42431
   125
     <td>
krauss@42431
   126
       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
krauss@42431
   127
-        <b>{desc|strip|firstline|escape|nonempty}</b>
krauss@42431
   128
+        <b>{desc|strip|escape|nonempty}</b>
krauss@42431
   129
       </a>
krauss@42431
   130
     </td>
krauss@42431
   131
     <td class="link">
krauss@42431
   132
@@ -238,7 +241,7 @@
krauss@42431
   133
     </td>
krauss@42431
   134
     <td>{description}</td>
krauss@42431
   135
     <td>{contact|obfuscate}</td>
krauss@42431
   136
-    <td class="age">{lastchange|age} ago</td>
krauss@42431
   137
+    <td class="age">{lastchange|age}</td>
krauss@42431
   138
     <td class="indexlinks">{archives%indexarchiveentry}</td>
krauss@42431
   139
     <td><div class="rss_logo"><a href="{url}rss-log">RSS</a> <a href="{url}atom-log">Atom</a></div></td>
krauss@42431
   140
   </tr>\n'