Startsida Utforska Hjälp
Logga in
caryoscelus
/
agda
Bevaka 1
Stjärnmärk 0
Fork 0
Filer Ärenden 0 Pull-förfrågningar 0 Wiki
Träd: ce9b406819
Grenar Taggar
agda
/
test
/
LaTeXAndHTML
/
succeed
/
Issue2604.html

Issue2604.html 8.7 KB
Historik Rå

1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>Issue2604</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Andreas, 2017-06-16, issue #2604:</a>
    3. 

  3. <a id="38" class="Comment">-- Symbolic anchors in generated HTML.</a>
    4. 

  4. 

  5. <a id="78" class="Keyword">module</a> <a id="85" href="Issue2604.html" class="Module">Issue2604</a> <a id="95" class="Keyword">where</a>
    6. 

  6. 

  7. <a id="test1"></a><a id="102" href="Issue2604.html#102" class="Function">test1</a> <a id="108" class="Symbol">:</a> <a id="110" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>  <a id="116" class="Comment">-- Symbolic anchor</a>
    8. 

  8. <a id="135" href="Issue2604.html#102" class="Function">test1</a> <a id="141" class="Symbol">=</a> <a id="143" href="Issue2604.html#157" class="Function">bla</a>
    9. 

  9.   <a id="149" class="Keyword">where</a>
    10. 

  10.   <a id="157" href="Issue2604.html#157" class="Function">bla</a> <a id="161" class="Symbol">=</a> <a id="163" href="Agda.Primitive.html#311" class="Primitive">Set</a>   <a id="169" class="Comment">-- Position anchor</a>
    11. 

  11. 

  12. <a id="test2"></a><a id="189" href="Issue2604.html#189" class="Function">test2</a> <a id="195" class="Symbol">:</a> <a id="197" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>  <a id="203" class="Comment">-- Symbolic anchor</a>
    13. 

  13. <a id="222" href="Issue2604.html#189" class="Function">test2</a> <a id="228" class="Symbol">=</a> <a id="230" href="Issue2604.html#244" class="Function">bla</a>
    14. 

  14.   <a id="236" class="Keyword">where</a>
    15. 

  15.   <a id="244" href="Issue2604.html#244" class="Function">bla</a> <a id="248" class="Symbol">=</a> <a id="250" href="Agda.Primitive.html#311" class="Primitive">Set</a>   <a id="256" class="Comment">-- Position anchor</a>
    16. 

  16. 

  17. <a id="test3"></a><a id="276" href="Issue2604.html#276" class="Function">test3</a> <a id="282" class="Symbol">:</a> <a id="284" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>  <a id="290" class="Comment">-- Symbolic anchor</a>
    18. 

  18. <a id="309" href="Issue2604.html#276" class="Function">test3</a> <a id="315" class="Symbol">=</a> <a id="317" href="Issue2604.html#340" class="Function">bla</a>
    19. 

  19.   <a id="323" class="Keyword">module</a> <a id="M"></a><a id="330" href="Issue2604.html#330" class="Module">M</a> <a id="332" class="Keyword">where</a>
    20. 

  20.   <a id="M.bla"></a><a id="340" href="Issue2604.html#340" class="Function">bla</a> <a id="344" class="Symbol">=</a> <a id="346" href="Agda.Primitive.html#311" class="Primitive">Set</a>  <a id="351" class="Comment">-- Symbolic anchor</a>
    21. 

  21. 

  22. <a id="371" class="Keyword">module</a> <a id="NamedModule"></a><a id="378" href="Issue2604.html#378" class="Module">NamedModule</a> <a id="390" class="Keyword">where</a>
    23. 

  23.   <a id="NamedModule.test4"></a><a id="398" href="Issue2604.html#398" class="Function">test4</a> <a id="404" class="Symbol">:</a> <a id="406" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>  <a id="412" class="Comment">-- Symbolic anchor</a>
    24. 

  24.   <a id="433" href="Issue2604.html#398" class="Function">test4</a> <a id="439" class="Symbol">=</a> <a id="441" href="Issue2604.html#340" class="Function">M.bla</a>
    25. 

  25. 

  26. <a id="448" class="Keyword">module</a> <a id="455" href="Issue2604.html#455" class="Module">_</a> <a id="457" class="Keyword">where</a>
    27. 

  27.   <a id="465" href="Issue2604.html#465" class="Function">test5</a> <a id="471" class="Symbol">:</a> <a id="473" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>  <a id="479" class="Comment">-- Position anchor</a>
    28. 

  28.   <a id="500" href="Issue2604.html#465" class="Function">test5</a> <a id="506" class="Symbol">=</a> <a id="508" href="Issue2604.html#340" class="Function">M.bla</a>
    29. 

  29. 

  30. <a id="515" class="Comment">-- Testing whether # in anchors confuses the browsers.</a>
    31. 

  31. <a id="570" class="Comment">-- Not Firefox 54.0, at least (Andreas, 2017-06-20).</a>
    32. 

  32. <a id="623" class="Comment">-- However, the Nu Html Checker complains (someone else, later).</a>
    33. 

  33. 

  34. <a id="#"></a><a id="689" href="Issue2604.html#689" class="Function">#</a> <a id="691" class="Symbol">:</a> <a id="693" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    35. 

  35. <a id="698" href="Issue2604.html#689" class="Function">#</a> <a id="700" class="Symbol">=</a> <a id="702" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    36. 

  36. 

  37. <a id="#a"></a><a id="707" href="Issue2604.html#707" class="Function">#a</a> <a id="710" class="Symbol">:</a> <a id="712" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    38. 

  38. <a id="717" href="Issue2604.html#707" class="Function">#a</a> <a id="720" class="Symbol">=</a> <a id="722" href="Issue2604.html#689" class="Function">#</a>
    39. 

  39. 

  40. <a id="b#"></a><a id="725" href="Issue2604.html#725" class="Function">b#</a> <a id="728" class="Symbol">:</a> <a id="730" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    41. 

  41. <a id="735" href="Issue2604.html#725" class="Function">b#</a> <a id="738" class="Symbol">=</a> <a id="740" href="Issue2604.html#707" class="Function">#a</a>
    42. 

  42. 

  43. <a id="##"></a><a id="744" href="Issue2604.html#744" class="Function">##</a> <a id="747" class="Symbol">:</a> <a id="749" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    44. 

  44. <a id="754" href="Issue2604.html#744" class="Function">##</a> <a id="757" class="Symbol">=</a> <a id="759" href="Issue2604.html#725" class="Function">b#</a>
    45. 

  45. 

  46. <a id="763" class="Comment">-- The href attribute values #A and #%41 are (correctly?) treated as</a>
    47. 

  47. <a id="832" class="Comment">-- pointers to the same destination by Firefox 54.0. To point to %41</a>
    48. 

  48. <a id="901" class="Comment">-- one should use #%2541.</a>
    49. 

  49. 

  50. <a id="A"></a><a id="928" href="Issue2604.html#928" class="Function">A</a> <a id="930" class="Symbol">:</a> <a id="932" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    51. 

  51. <a id="937" href="Issue2604.html#928" class="Function">A</a> <a id="939" class="Symbol">=</a> <a id="941" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    52. 

  52. 

  53. <a id="%41"></a><a id="946" href="Issue2604.html#946" class="Function">%41</a> <a id="950" class="Symbol">:</a> <a id="952" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    54. 

  54. <a id="957" href="Issue2604.html#946" class="Function">%41</a> <a id="961" class="Symbol">=</a> <a id="963" href="Issue2604.html#928" class="Function">A</a>
    55. 

  55. 

  56. <a id="966" class="Comment">-- Ampersands may need to be encoded in some way. The blaze-html</a>
    57. 

  57. <a id="1031" class="Comment">-- library takes care of encoding id attribute values, and we manually</a>
    58. 

  58. <a id="1102" class="Comment">-- replace ampersands with %26 in the fragment parts of href attribute</a>
    59. 

  59. <a id="1173" class="Comment">-- values.</a>
    60. 

  60. 

  61. <a id="&amp;amp"></a><a id="1185" href="Issue2604.html#1185" class="Function">&amp;amp</a> <a id="1190" class="Symbol">:</a> <a id="1192" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    62. 

  62. <a id="1197" href="Issue2604.html#1185" class="Function">&amp;amp</a> <a id="1202" class="Symbol">=</a> <a id="1204" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    63. 

  63. 

  64. <a id="&amp;lt"></a><a id="1209" href="Issue2604.html#1209" class="Function">&amp;lt</a> <a id="1213" class="Symbol">:</a> <a id="1215" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    65. 

  65. <a id="1220" href="Issue2604.html#1209" class="Function">&amp;lt</a> <a id="1224" class="Symbol">=</a> <a id="1226" href="Issue2604.html#1185" class="Function">&amp;amp</a>
    66. 

  66. 

  67. <a id="1232" class="Comment">-- Test of fixity declarations. The id attribute value for the</a>
    68. 

  68. <a id="1295" class="Comment">-- operator in the fixity declaration should be unique.</a>
    69. 

  69. 

  70. <a id="1352" class="Keyword">infix</a> <a id="1358" class="Number">0</a> <a id="1360" href="Issue2604.html#1368" class="Function Operator">_%42∀_</a>
    71. 

  71. 

  72. <a id="_%42∀_"></a><a id="1368" href="Issue2604.html#1368" class="Function Operator">_%42∀_</a> <a id="1375" class="Symbol">:</a> <a id="1377" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    73. 

  73. <a id="1382" href="Issue2604.html#1368" class="Function Operator">_%42∀_</a> <a id="1389" class="Symbol">=</a> <a id="1391" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    74. 

  74. 

  75. <a id="1396" class="Comment">-- The following two variants of the character Ö should result in</a>
    76. 

  76. <a id="1462" class="Comment">-- distinct links.</a>
    77. 

  77. 

  78. <a id="Ö"></a><a id="1482" href="Issue2604.html#1482" class="Function">Ö</a> <a id="1484" class="Symbol">:</a> <a id="1486" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    79. 

  79. <a id="1491" href="Issue2604.html#1482" class="Function">Ö</a> <a id="1493" class="Symbol">=</a> <a id="1495" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    80. 

  80. 

  81. <a id="Ö"></a><a id="1500" href="Issue2604.html#1500" class="Function">Ö</a> <a id="1503" class="Symbol">:</a> <a id="1505" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    82. 

  82. <a id="1510" href="Issue2604.html#1500" class="Function">Ö</a> <a id="1513" class="Symbol">=</a> <a id="1515" href="Issue2604.html#1482" class="Function">Ö</a>
    83. 

  83. </pre></body></html>
    84.