Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/Mercurial/isabelle-style-1.3.1.diff
author paulson <lp15@cam.ac.uk>
Mon, 18 Aug 2025 22:37:21 +0100
changeset 83011 d35875d530a2
parent 42431 79ef651d88eb
permissions -rw-r--r--
Simple facts about Lebesgue integration
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42431
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
     1
 
diff -Naur gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
     2
 
--- gitweb/changelogentry.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
     3
 
+++ isabelle/changelogentry.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
     4
 
@@ -1,14 +1,12 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
     5
 
 <div>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
     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>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
     7
 
-</div>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
     8
 
-<div class="title_text">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
     9
 
-<div class="log_link">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    10
 
-<a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    11
 
-</div>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    12
 
-<i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    13
 
+<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    14
 
+{author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    15
 
 </div>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    16
 
 <div class="log_body">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    17
 
 {desc|strip|escape|addbreaks|nonempty}
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    18
 
 <br/>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    19
 
+<div class="files">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    20
 
+{files}
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    21
 
+</div>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    22
 
 <br/>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    23
 
 </div>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    24
 
diff -Naur gitweb/changeset.tmpl isabelle/changeset.tmpl
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    25
 
--- gitweb/changeset.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    26
 
+++ isabelle/changeset.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    27
 
@@ -29,7 +29,7 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    28
 
 <div class="title_text">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    29
 
 <table cellspacing="0">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    30
 
 <tr><td>author</td><td>{author|obfuscate}</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    31
 
-<tr><td></td><td>{date|date} ({date|age} ago)</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    32
 
+<tr><td></td><td>{date|date} ({date|age})</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    33
 
 {branch%changesetbranch}
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    34
 
 <tr><td>changeset {rev}</td><td style="font-family:monospace">{node|short}</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    35
 
 {parent%changesetparent}
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    36
 
diff -Naur gitweb/fileannotate.tmpl isabelle/fileannotate.tmpl
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    37
 
--- gitweb/fileannotate.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    38
 
+++ isabelle/fileannotate.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    39
 
@@ -36,7 +36,7 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    40
 
  <td>{author|obfuscate}</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    41
 
 <tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    42
 
  <td></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    43
 
- <td>{date|date} ({date|age} ago)</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    44
 
+ <td>{date|date} ({date|age})</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    45
 
 {branch%filerevbranch}
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    46
 
 <tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    47
 
  <td>changeset {rev}</td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    48
 
diff -Naur gitweb/filerevision.tmpl isabelle/filerevision.tmpl
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    49
 
--- gitweb/filerevision.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    50
 
+++ isabelle/filerevision.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    51
 
@@ -36,7 +36,7 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    52
 
  <td>{author|obfuscate}</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    53
 
 <tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    54
 
  <td></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    55
 
- <td>{date|date} ({date|age} ago)</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    56
 
+ <td>{date|date} ({date|age})</td></tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    57
 
 {branch%filerevbranch}
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    58
 
 <tr>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    59
 
  <td>changeset {rev}</td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    60
 
diff -Naur gitweb/graph.tmpl isabelle/graph.tmpl
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    61
 
--- gitweb/graph.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    62
 
+++ isabelle/graph.tmpl	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    63
 
@@ -63,7 +63,7 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    64
 
 var revlink = '<li style="_STYLE"><span class="desc">';
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    65
 
 revlink += '<a class="list" href="{url}rev/_NODEID{sessionvars%urlparameter}" title="_NODEID"><b>_DESC</b></a>';
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    66
 
 revlink += '</span> _TAGS';
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    67
 
-revlink += '<span class="info">_DATE ago, by _USER</span></li>';
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    68
 
+revlink += '<span class="info">_DATE, by _USER</span></li>';
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    69
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    70
 
 graph.vertex = function(x, y, color, parity, cur) {
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    71
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    72
 
diff -Naur gitweb/map isabelle/map
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    73
 
--- gitweb/map	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    74
 
+++ isabelle/map	2011-04-20 12:13:37.000000000 +0200
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    75
 
@@ -78,7 +78,7 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    76
 
   <tr style="font-family:monospace" class="parity{parity}">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    77
 
     <td class="linenr" style="text-align: right;">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    78
 
       <a href="{url}annotate/{node|short}/{file|urlescape}{sessionvars%urlparameter}#l{targetline}"
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    79
 
-         title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}</a>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    80
 
+         title="{node|short}: {desc|escape}">{author|user}@{rev}</a>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    81
 
     </td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    82
 
     <td><pre><a class="linenr" href="#{lineid}" id="{lineid}">{linenumber}</a></pre></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    83
 
     <td><pre>{line|escape}</pre></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    84
 
@@ -150,7 +150,7 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    85
 
 tags = tags.tmpl
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    86
 
 tagentry = '
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    87
 
   <tr class="parity{parity}">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    88
 
-    <td class="age"><i>{date|age} ago</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    89
 
+    <td class="age"><i>{date|age}</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    90
 
     <td><a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}"><b>{tag|escape}</b></a></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    91
 
     <td class="link">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    92
 
       <a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a> |
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    93
 
@@ -161,7 +161,7 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    94
 
 branches = branches.tmpl
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    95
 
 branchentry = '
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    96
 
   <tr class="parity{parity}">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    97
 
-    <td class="age"><i>{date|age} ago</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    98
 
+    <td class="age"><i>{date|age}</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
    99
 
     <td><a class="list" href="{url}shortlog/{node|short}{sessionvars%urlparameter}"><b>{node|short}</b></a></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   100
 
     <td class="{status}">{branch|escape}</td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   101
 
     <td class="link">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   102
 
@@ -204,11 +204,12 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   103
 
 inbranchtag = '<span class="inbranchtag" title="{name}">{name}</span> '
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   104
 
 shortlogentry = '
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   105
 
   <tr class="parity{parity}">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   106
 
-    <td class="age"><i>{date|age} ago</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   107
 
+    <td class="age"><i>{date|age}</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   108
 
     <td><i>{author|person}</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   109
 
+    <td><i>{date|shortdate}</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   110
 
     <td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   111
 
       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   112
 
-        <b>{desc|strip|firstline|escape|nonempty}</b>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   113
 
+        <b>{desc|strip|escape|nonempty}</b>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   114
 
         <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   115
 
       </a>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   116
 
     </td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   117
 
@@ -219,10 +220,12 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   118
 
   </tr>'
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   119
 
 filelogentry = '
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   120
 
   <tr class="parity{parity}">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   121
 
-    <td class="age"><i>{date|age} ago</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   122
 
+    <td class="age"><i>{date|age}</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   123
 
+    <td><i>{author|person}</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   124
 
+    <td><i>{date|shortdate}</i></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   125
 
     <td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   126
 
       <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   127
 
-        <b>{desc|strip|firstline|escape|nonempty}</b>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   128
 
+        <b>{desc|strip|escape|nonempty}</b>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   129
 
       </a>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   130
 
     </td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   131
 
     <td class="link">
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   132
 
@@ -238,7 +241,7 @@
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   133
 
     </td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   134
 
     <td>{description}</td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   135
 
     <td>{contact|obfuscate}</td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   136
 
-    <td class="age">{lastchange|age} ago</td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   137
 
+    <td class="age">{lastchange|age}</td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   138
 
     <td class="indexlinks">{archives%indexarchiveentry}</td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   139
 
     <td><div class="rss_logo"><a href="{url}rss-log">RSS</a> <a href="{url}atom-log">Atom</a></div></td>
79ef651d88eb use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
krauss
parents: 42430
diff changeset 
   140
 
   </tr>\n'
isabelle