# HG changeset patch # User wenzelm # Date 1451419098 -3600 # Node ID 2548e7cc86fbf3e857bcd51bfbf2c9fda4aceedf # Parent 9c8fc56032e3618f5bd57217cfa99debb54a7a2f more arrow symbols; diff -r 9c8fc56032e3 -r 2548e7cc86fb NEWS --- a/NEWS Tue Dec 29 19:11:23 2015 +0100 +++ b/NEWS Tue Dec 29 20:58:18 2015 +0100 @@ -31,6 +31,18 @@ remains available under print mode "ASCII", but less important syntax has been removed (see below). +* Support for arrows of various lengths, with rendering in LaTeX and +Isabelle fonts: + + \ + \ + \ + \ + \ + \ + \ + \ + *** Prover IDE -- Isabelle/Scala/jEdit *** diff -r 9c8fc56032e3 -r 2548e7cc86fb etc/abbrevs --- a/etc/abbrevs Tue Dec 29 19:11:23 2015 +0100 +++ b/etc/abbrevs Tue Dec 29 20:58:18 2015 +0100 @@ -1,5 +1,5 @@ (* additional abbreviations for syntactic completion *) (*prevent replacement of very long arrows*) -"--->" = "--->" +"----->" = "----->" "===>" = "===>" diff -r 9c8fc56032e3 -r 2548e7cc86fb etc/symbols --- a/etc/symbols Tue Dec 29 19:11:23 2015 +0100 +++ b/etc/symbols Tue Dec 29 20:58:18 2015 +0100 @@ -156,8 +156,12 @@ \ code: 0x002124 group: letter \ code: 0x002190 group: arrow abbrev: <. \ code: 0x0027f5 group: arrow abbrev: <. +\ code: 0x00290e group: arrow abbrev: <. +\ code: 0x0021e0 group: arrow abbrev: <. \ code: 0x002192 group: arrow abbrev: .> abbrev: -> \ code: 0x0027f6 group: arrow abbrev: .> abbrev: --> +\ code: 0x00290f group: arrow abbrev: .> abbrev: ---> +\ code: 0x0021e2 group: arrow abbrev: .> abbrev: ----> \ code: 0x0021d0 group: arrow abbrev: <. \ code: 0x0027f8 group: arrow abbrev: <. \ code: 0x0021d2 group: arrow abbrev: .> abbrev: => diff -r 9c8fc56032e3 -r 2548e7cc86fb lib/fonts/IsabelleText.sfd --- a/lib/fonts/IsabelleText.sfd Tue Dec 29 19:11:23 2015 +0100 +++ b/lib/fonts/IsabelleText.sfd Tue Dec 29 20:58:18 2015 +0100 @@ -19,7 +19,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050361371 -ModificationTime: 1446896286 +ModificationTime: 1451417325 PfmFamily: 17 TTFWeight: 400 TTFWidth: 5 @@ -2241,11 +2241,11 @@ DisplaySize: -96 AntiAlias: 1 FitToEm: 1 -WinInfo: 9864 18 16 +WinInfo: 10278 18 16 BeginPrivate: 0 EndPrivate TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144 -BeginChars: 1114189 1398 +BeginChars: 1114189 1399 StartChar: u10000 Encoding: 65536 65536 0 @@ -54601,34 +54601,68 @@ StartChar: uni21E0 Encoding: 8672 8672 1077 -Width: 1233 -Flags: W -LayerCount: 2 -Fore -SplineSet -545 643 m 1,0,-1 - 545.001 478.998 l 1,1,-1 - 287 479 l 9,2,-1 - 447 319 l 1,3,-1 - 357 229 l 1,4,-1 - 66 520 l 9,5,-1 - 66 602 l 17,6,-1 - 357 893 l 1,7,-1 - 447 803 l 1,8,-1 - 287 643 l 17,9,-1 - 545 643 l 1,0,-1 -670.001 479.001 m 1,10,-1 - 670 642.999 l 1,11,-1 - 856.999 643 l 1,12,-1 - 856.999 478.998 l 1,13,-1 - 670.001 479.001 l 1,10,-1 -980.001 479.001 m 1,14,-1 - 980.001 642.997 l 1,15,-1 - 1167 643 l 1,16,-1 - 1167 479 l 1,17,-1 - 980.001 479.001 l 1,14,-1 -EndSplineSet -Validated: 1 +Width: 6063 +VWidth: 2220 +Flags: W +HStem: 511 88<394 5848.81> +VStem: 563 71<166.706 257.064> +LayerCount: 2 +Fore +SplineSet +5782 511.5 m 6,0,-1 + 2172 511 l 2,1,2 + 2147.74 511.152 l 0,3,4 + 2137.01 511.244 l 1,5,6 + 2122 511 l 2,7,-1 + 2101 511 l 1,8,-1 + 394 511 l 1,9,10 + 452 469 452 469 501 412 c 128,-1,11 + 550 355 550 355 577 308 c 128,-1,12 + 604 261 604 261 619 228 c 128,-1,13 + 634 195 634 195 634 186 c 0,14,15 + 634 172 634 172 624 166 c 128,-1,16 + 614 160 614 160 601 160 c 0,17,18 + 584 160 584 160 577.5 166.5 c 128,-1,19 + 571 173 571 173 563 191 c 0,20,21 + 512 301 512 301 437 383.5 c 0,22,23 + 368.667 458.667 368.667 458.667 234 526 c 0,24,25 + 228 529 228 529 223.5 532 c 128,-1,26 + 219 535 219 535 215.5 538 c 128,-1,27 + 212 541 212 541 210 545 c 128,-1,28 + 208 549 208 549 208 555 c 128,-1,29 + 208 561 208 561 208.5 564 c 128,-1,30 + 209 567 209 567 215 571.5 c 128,-1,31 + 221 576 221 576 222.5 577 c 128,-1,32 + 224 578 224 578 239 586 c 0,33,34 + 302 616 302 616 355 655.5 c 128,-1,35 + 408 695 408 695 440 728 c 0,36,37 + 472 762 472 762 500 805 c 0,38,39 + 531.719 853.711 531.719 853.711 539.5 871.5 c 0,40,41 + 558.722 915.443 558.722 915.443 565 928 c 0,42,43 + 569 936 569 936 570.5 938.5 c 128,-1,44 + 572 941 572 941 580 945.5 c 128,-1,45 + 588 950 588 950 601 950 c 0,46,47 + 615 950 615 950 624.5 943.5 c 128,-1,48 + 634 937 634 937 634 924 c 0,49,50 + 634 915 634 915 619 882 c 128,-1,51 + 604 849 604 849 577 802 c 128,-1,52 + 550 755 550 755 501 698.5 c 128,-1,53 + 452 642 452 642 394 599 c 1,54,-1 + 2101 599 l 1,55,-1 + 2122 599 l 2,56,57 + 2136.92 598.968 l 1,58,59 + 2148.11 598.97 l 0,60,-1 + 2172 599 l 2,61,-1 + 5782 599.5 l 6,62,63 + 5797.84 599.502 5797.84 599.502 5807.5 599 c 132,-1,64 + 5817 598.5 5817 598.5 5830 594.5 c 132,-1,65 + 5843 590.5 5843 590.5 5849 581 c 132,-1,66 + 5855 571.5 5855 571.5 5855 555.5 c 132,-1,67 + 5855 539.5 5855 539.5 5849 530 c 132,-1,68 + 5843 520.5 5843 520.5 5830 516.5 c 132,-1,69 + 5817 512.5 5817 512.5 5807.5 512 c 4,70,71 + 5798.64 511.502 5798.64 511.502 5782 511.5 c 6,0,-1 +EndSplineSet EndChar StartChar: uni21E1 @@ -54665,34 +54699,68 @@ StartChar: uni21E2 Encoding: 8674 8674 1079 -Width: 1233 -Flags: W -LayerCount: 2 -Fore -SplineSet -688 643 m 1,0,-1 - 946 643 l 9,1,-1 - 786 803 l 1,2,-1 - 876 893 l 1,3,-1 - 1167 602 l 9,4,-1 - 1167 520 l 17,5,-1 - 876 229 l 1,6,-1 - 786 319 l 1,7,-1 - 946 479 l 17,8,-1 - 687.999 478.998 l 1,9,-1 - 688 643 l 1,0,-1 -562.999 479.001 m 1,10,-1 - 376.001 478.998 l 1,11,-1 - 376.001 643 l 1,12,-1 - 563 642.999 l 1,13,-1 - 562.999 479.001 l 1,10,-1 -252.999 479.001 m 1,14,-1 - 66 479 l 1,15,-1 - 66 643 l 1,16,-1 - 252.999 642.997 l 1,17,-1 - 252.999 479.001 l 1,14,-1 -EndSplineSet -Validated: 1 +Width: 6062 +VWidth: 2220 +Flags: W +HStem: 511.5 88<218.705 5664> +VStem: 5424 71<849.469 944.029> +LayerCount: 2 +Fore +SplineSet +2694 511.5 m 2,0,-1 + 285 511 l 2,1,2 + 269.114 510.997 269.114 510.997 260 511.5 c 128,-1,3 + 251 512 251 512 238 516 c 128,-1,4 + 225 520 225 520 218.5 529.5 c 128,-1,5 + 212 539 212 539 212 555 c 128,-1,6 + 212 571 212 571 218.5 580.5 c 128,-1,7 + 225 590 225 590 238 594 c 128,-1,8 + 251 598 251 598 260 598.5 c 128,-1,9 + 268.974 598.997 268.974 598.997 285 599 c 2,10,-1 + 2694 599.5 l 2,11,12 + 2713.46 599.458 l 0,13,-1 + 2724.83 599.208 l 0,14,15 + 2735 599.5 l 2,16,-1 + 2756 599.5 l 1,17,-1 + 5664 599.25 l 5,18,19 + 5606 641.25 5606 641.25 5556.5 698.25 c 132,-1,20 + 5507 755.25 5507 755.25 5480 802.25 c 132,-1,21 + 5453 849.25 5453 849.25 5438.5 882.25 c 132,-1,22 + 5424 915.25 5424 915.25 5424 924.25 c 4,23,24 + 5424 938.25 5424 938.25 5434 944.25 c 132,-1,25 + 5444 950.25 5444 950.25 5457 950.25 c 4,26,27 + 5474 950.25 5474 950.25 5481 944.25 c 4,28,29 + 5487 937.25 5487 937.25 5495 919.25 c 4,30,31 + 5526 848.25 5526 848.25 5569 788.25 c 4,32,33 + 5609 731.25 5609 731.25 5655 691.75 c 132,-1,34 + 5701 652.25 5701 652.25 5742 626.75 c 132,-1,35 + 5783 601.25 5783 601.25 5834 577.25 c 5,36,37 + 5837 577.25 5837 577.25 5843.5 571.25 c 132,-1,38 + 5850 565.25 5850 565.25 5850 555.25 c 4,39,40 + 5850 544.25 5850 544.25 5845 539.25 c 132,-1,41 + 5840 534.25 5840 534.25 5819 524.25 c 4,42,43 + 5773 502.25 5773 502.25 5732.5 475.75 c 132,-1,44 + 5692 449.25 5692 449.25 5663 424.75 c 132,-1,45 + 5634 400.25 5634 400.25 5607.5 369.25 c 132,-1,46 + 5581 338.25 5581 338.25 5565 316.25 c 132,-1,47 + 5549 294.25 5549 294.25 5532.5 264.25 c 4,48,49 + 5511.31 225.717 5511.31 225.717 5509.5 220.25 c 4,50,51 + 5504.63 205.505 5504.63 205.505 5493 182.25 c 4,52,53 + 5489 174.25 5489 174.25 5487 171.75 c 132,-1,54 + 5485 169.25 5485 169.25 5477 164.25 c 4,55,56 + 5469 160.25 5469 160.25 5457 160.25 c 4,57,58 + 5443 160.25 5443 160.25 5433.5 166.75 c 132,-1,59 + 5424 173.25 5424 173.25 5424 186.25 c 4,60,61 + 5424 195.25 5424 195.25 5438.5 228.25 c 132,-1,62 + 5453 261.25 5453 261.25 5480 308.25 c 132,-1,63 + 5507 355.25 5507 355.25 5556.5 412.25 c 132,-1,64 + 5606 469.25 5606 469.25 5664 511.25 c 5,65,-1 + 2756 511.5 l 1,66,-1 + 2735 511.5 l 2,67,68 + 2725.08 511.875 l 0,69,70 + 2715.96 511.875 l 0,71,-1 + 2694 511.5 l 2,0,-1 +EndSplineSet EndChar StartChar: uni21E3 @@ -62017,7 +62085,7 @@ EndChar StartChar: uni2756 -Encoding: 10070 10070 1397 +Encoding: 10070 10070 1396 Width: 1233 Flags: W LayerCount: 2 @@ -62045,5 +62113,137 @@ 358 254 l 1,12,-1 EndSplineSet EndChar + +StartChar: uni290E +Encoding: 10510 10510 1397 +Width: 4863 +VWidth: 2220 +Flags: W +HStem: 511 88<394 4648.81> +VStem: 563 71<166.706 257.064> +LayerCount: 2 +Fore +SplineSet +4582 511.5 m 2,0,-1 + 2172 511 l 2,1,2 + 2147.74 511.152 l 0,3,4 + 2137.01 511.244 l 1,5,6 + 2122 511 l 2,7,-1 + 2101 511 l 1,8,-1 + 394 511 l 1,9,10 + 452 469 452 469 501 412 c 128,-1,11 + 550 355 550 355 577 308 c 128,-1,12 + 604 261 604 261 619 228 c 128,-1,13 + 634 195 634 195 634 186 c 0,14,15 + 634 172 634 172 624 166 c 128,-1,16 + 614 160 614 160 601 160 c 0,17,18 + 584 160 584 160 577.5 166.5 c 128,-1,19 + 571 173 571 173 563 191 c 0,20,21 + 512 301 512 301 437 383.5 c 0,22,23 + 368.667 458.667 368.667 458.667 234 526 c 0,24,25 + 228 529 228 529 223.5 532 c 128,-1,26 + 219 535 219 535 215.5 538 c 128,-1,27 + 212 541 212 541 210 545 c 128,-1,28 + 208 549 208 549 208 555 c 128,-1,29 + 208 561 208 561 208.5 564 c 128,-1,30 + 209 567 209 567 215 571.5 c 128,-1,31 + 221 576 221 576 222.5 577 c 128,-1,32 + 224 578 224 578 239 586 c 0,33,34 + 302 616 302 616 355 655.5 c 128,-1,35 + 408 695 408 695 440 728 c 0,36,37 + 472 762 472 762 500 805 c 0,38,39 + 531.719 853.711 531.719 853.711 539.5 871.5 c 0,40,41 + 558.722 915.443 558.722 915.443 565 928 c 0,42,43 + 569 936 569 936 570.5 938.5 c 128,-1,44 + 572 941 572 941 580 945.5 c 128,-1,45 + 588 950 588 950 601 950 c 0,46,47 + 615 950 615 950 624.5 943.5 c 128,-1,48 + 634 937 634 937 634 924 c 0,49,50 + 634 915 634 915 619 882 c 128,-1,51 + 604 849 604 849 577 802 c 128,-1,52 + 550 755 550 755 501 698.5 c 128,-1,53 + 452 642 452 642 394 599 c 1,54,-1 + 2101 599 l 1,55,-1 + 2122 599 l 2,56,57 + 2136.92 598.968 l 1,58,59 + 2148.11 598.97 l 0,60,-1 + 2172 599 l 2,61,-1 + 4582 599.5 l 2,62,63 + 4597.93 599.503 4597.93 599.503 4607.5 599 c 128,-1,64 + 4617 598.5 4617 598.5 4630 594.5 c 128,-1,65 + 4643 590.5 4643 590.5 4649 581 c 128,-1,66 + 4655 571.5 4655 571.5 4655 555.5 c 128,-1,67 + 4655 539.5 4655 539.5 4649 530 c 128,-1,68 + 4643 520.5 4643 520.5 4630 516.5 c 128,-1,69 + 4617 512.5 4617 512.5 4607.5 512 c 0,70,71 + 4598.38 511.503 4598.38 511.503 4582 511.5 c 2,0,-1 +EndSplineSet +EndChar + +StartChar: uni290F +Encoding: 10511 10511 1398 +Width: 4862 +VWidth: 2220 +Flags: W +HStem: 511 88<218.705 4464> +VStem: 4224 71<849.719 944.279> +LayerCount: 2 +Fore +SplineSet +2694 511.5 m 6,0,-1 + 285 511 l 2,1,2 + 269.087 510.997 269.087 510.997 260 511.5 c 128,-1,3 + 251 512 251 512 238 516 c 128,-1,4 + 225 520 225 520 218.5 529.5 c 128,-1,5 + 212 539 212 539 212 555 c 128,-1,6 + 212 571 212 571 218.5 580.5 c 128,-1,7 + 225 590 225 590 238 594 c 128,-1,8 + 251 598 251 598 260 598.5 c 128,-1,9 + 268.974 598.997 268.974 598.997 285 599 c 2,10,-1 + 2694 599.5 l 2,11,12 + 2713.46 599.458 l 0,13,-1 + 2724.83 599.208 l 0,14,15 + 2735 599.5 l 2,16,-1 + 2756 599.5 l 1,17,-1 + 4464 599.5 l 1,18,19 + 4406 641.5 4406 641.5 4356.5 698.5 c 128,-1,20 + 4307 755.5 4307 755.5 4280 802.5 c 128,-1,21 + 4253 849.5 4253 849.5 4238.5 882.5 c 128,-1,22 + 4224 915.5 4224 915.5 4224 924.5 c 0,23,24 + 4224 938.5 4224 938.5 4234 944.5 c 128,-1,25 + 4244 950.5 4244 950.5 4257 950.5 c 0,26,27 + 4274 950.5 4274 950.5 4281 944.5 c 0,28,29 + 4287 937.5 4287 937.5 4295 919.5 c 0,30,31 + 4326 848.5 4326 848.5 4369 788.5 c 0,32,33 + 4409 731.5 4409 731.5 4455 692 c 128,-1,34 + 4501 652.5 4501 652.5 4542 627 c 128,-1,35 + 4583 601.5 4583 601.5 4634 577.5 c 1,36,37 + 4637 577.5 4637 577.5 4643.5 571.5 c 128,-1,38 + 4650 565.5 4650 565.5 4650 555.5 c 0,39,40 + 4650 544.5 4650 544.5 4645 539.5 c 128,-1,41 + 4640 534.5 4640 534.5 4619 524.5 c 0,42,43 + 4573 502.5 4573 502.5 4532.5 476 c 128,-1,44 + 4492 449.5 4492 449.5 4463 425 c 128,-1,45 + 4434 400.5 4434 400.5 4407.5 369.5 c 128,-1,46 + 4381 338.5 4381 338.5 4365 316.5 c 128,-1,47 + 4349 294.5 4349 294.5 4332.5 264.5 c 0,48,49 + 4311.31 225.967 4311.31 225.967 4309.5 220.5 c 0,50,51 + 4304.63 205.755 4304.63 205.755 4293 182.5 c 0,52,53 + 4289 174.5 4289 174.5 4287 172 c 128,-1,54 + 4285 169.5 4285 169.5 4277 164.5 c 0,55,56 + 4269 160.5 4269 160.5 4257 160.5 c 0,57,58 + 4243 160.5 4243 160.5 4233.5 167 c 128,-1,59 + 4224 173.5 4224 173.5 4224 186.5 c 0,60,61 + 4224 195.5 4224 195.5 4238.5 228.5 c 128,-1,62 + 4253 261.5 4253 261.5 4280 308.5 c 128,-1,63 + 4307 355.5 4307 355.5 4356.5 412.5 c 128,-1,64 + 4406 469.5 4406 469.5 4464 511.5 c 1,65,-1 + 2756 511.5 l 5,66,-1 + 2735 511.5 l 6,67,68 + 2725.08 511.875 l 4,69,70 + 2715.96 511.875 l 4,71,-1 + 2694 511.5 l 6,0,-1 +EndSplineSet +EndChar EndChars EndSplineFont diff -r 9c8fc56032e3 -r 2548e7cc86fb lib/fonts/IsabelleTextBold.sfd --- a/lib/fonts/IsabelleTextBold.sfd Tue Dec 29 19:11:23 2015 +0100 +++ b/lib/fonts/IsabelleTextBold.sfd Tue Dec 29 20:58:18 2015 +0100 @@ -20,7 +20,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050374980 -ModificationTime: 1446896348 +ModificationTime: 1451417467 PfmFamily: 17 TTFWeight: 700 TTFWidth: 5 @@ -1678,10 +1678,10 @@ DisplaySize: -96 AntiAlias: 1 FitToEm: 1 -WinInfo: 9996 21 15 +WinInfo: 8568 21 15 BeginPrivate: 0 EndPrivate -BeginChars: 1114115 1389 +BeginChars: 1114115 1391 StartChar: .notdef Encoding: 1114112 -1 0 @@ -48157,32 +48157,83 @@ StartChar: uni21E0 Encoding: 8672 8672 1077 -Width: 1233 -Flags: W -LayerCount: 2 -Fore -SplineSet -545 673 m 1,0,-1 - 545 449 l 1,1,-1 - 347 449 l 1,2,-1 - 477 319 l 1,3,-1 - 357 199 l 1,4,-1 - 66 490 l 1,5,-1 - 66 632 l 1,6,-1 - 357 923 l 1,7,-1 - 477 803 l 1,8,-1 - 347 673 l 1,9,-1 - 545 673 l 1,0,-1 -670 449 m 1,10,-1 - 670 673 l 1,11,-1 - 857 673 l 1,12,-1 - 857 449 l 1,13,-1 - 670 449 l 1,10,-1 -980 449 m 1,14,-1 - 980 673 l 1,15,-1 - 1167 673 l 1,16,-1 - 1167 449 l 1,17,-1 - 980 449 l 1,14,-1 +Width: 6063 +VWidth: 2220 +Flags: W +HStem: 460 190<526.64 5893.39> +LayerCount: 2 +Fore +SplineSet +5782.01 460.5 m 2,0,-1 + 2171.84 460 l 1,1,-1 + 2147.36 460.154 l 1,2,-1 + 2137.21 460.241 l 1,3,-1 + 2122.41 460 l 1,4,-1 + 526.64 460 l 1,5,6 + 533.536 452.388 533.536 452.388 539.674 445.246 c 0,7,8 + 591.818 384.59 591.818 384.59 621.222 333.404 c 0,9,10 + 649.427 284.306 649.427 284.306 665.429 249.104 c 0,11,12 + 667.284 245.025 667.284 245.025 671.437 236.4 c 128,-1,13 + 675.589 227.776 675.589 227.776 677.162 223.965 c 128,-1,14 + 678.735 220.155 678.735 220.155 681.046 213.392 c 128,-1,15 + 683.357 206.629 683.357 206.629 684.178 200.206 c 128,-1,16 + 685 193.783 685 193.783 685 186 c 0,17,18 + 685 168.111 685 168.111 676.078 150.264 c 128,-1,19 + 667.155 132.417 667.155 132.417 650.239 122.268 c 0,20,21 + 628.126 109 628.126 109 601 109 c 0,22,23 + 562.875 109 562.875 109 541.438 130.438 c 0,24,25 + 528.24 143.635 528.24 143.635 516.561 169.916 c 0,26,27 + 469.006 272.477 469.006 272.477 399.263 349.194 c 0,28,29 + 337.335 417.314 337.335 417.314 211.192 480.384 c 0,30,31 + 202.353 484.803 202.353 484.803 195.21 489.565 c 128,-1,32 + 188.149 494.273 188.149 494.273 182.31 499.278 c 0,33,34 + 170.991 508.98 170.991 508.98 164.384 522.192 c 0,35,36 + 157 536.96 157 536.96 157 555 c 0,37,38 + 157 565.221 157 565.221 158.194 572.384 c 0,39,40 + 159.313 579.101 159.313 579.101 161.486 584.891 c 128,-1,41 + 163.659 590.682 163.659 590.682 165.713 594.27 c 128,-1,42 + 167.767 597.858 167.767 597.858 171.056 601.384 c 128,-1,43 + 174.346 604.91 174.346 604.91 176.034 606.284 c 128,-1,44 + 177.722 607.658 177.722 607.658 180.939 609.888 c 128,-1,45 + 184.156 612.117 184.156 612.117 184.4 612.3 c 0,46,47 + 191.536 617.651 191.536 617.651 194.21 619.435 c 0,48,49 + 197.794 621.824 197.794 621.824 215 631 c 2,50,-1 + 216.025 631.547 l 1,51,-1 + 217.073 632.046 l 2,52,53 + 275.547 659.891 275.547 659.891 324.524 696.392 c 0,54,55 + 373.814 733.128 373.814 733.128 403.127 763.236 c 0,56,57 + 432.003 794.039 432.003 794.039 457.262 832.829 c 0,58,59 + 486.682 878.009 486.682 878.009 492.775 891.939 c 0,60,61 + 512.518 937.077 512.518 937.077 519.384 950.808 c 0,62,63 + 524.259 960.558 524.259 960.558 526.768 964.739 c 0,64,65 + 531.023 971.832 531.023 971.832 535.597 976.772 c 128,-1,66 + 540.171 981.711 540.171 981.711 542.525 983.359 c 128,-1,67 + 544.879 985.007 544.879 985.007 549.608 987.293 c 128,-1,68 + 554.336 989.579 554.336 989.579 554.997 989.95 c 0,69,70 + 574.642 1001 574.642 1001 601 1001 c 0,71,72 + 630.778 1001 630.778 1001 653.299 985.591 c 0,73,74 + 685 963.9 685 963.9 685 924 c 0,75,76 + 685 916.203 685 916.203 684.179 909.776 c 128,-1,77 + 683.357 903.348 683.357 903.348 681.052 896.6 c 128,-1,78 + 678.746 889.851 678.746 889.851 677.167 886.032 c 128,-1,79 + 675.589 882.212 675.589 882.212 671.444 873.611 c 128,-1,80 + 667.298 865.01 667.298 865.01 665.429 860.896 c 0,81,82 + 649.428 825.698 649.428 825.698 621.222 776.596 c 0,83,84 + 591.768 725.32 591.768 725.32 539.529 665.086 c 0,85,86 + 533.058 657.623 533.058 657.623 526.091 650 c 1,87,-1 + 2122.05 650 l 1,88,-1 + 2136.97 649.968 l 1,89,-1 + 2148.09 649.97 l 1,90,-1 + 2171.98 650 l 1,91,-1 + 5781.99 650.5 l 2,92,93 + 5799.17 650.502 5799.17 650.502 5810.19 649.929 c 0,94,95 + 5825.98 649.098 5825.98 649.098 5845 643.245 c 0,96,97 + 5876.03 633.694 5876.03 633.694 5892.12 608.234 c 0,98,99 + 5906 586.265 5906 586.265 5906 555.5 c 128,-1,100 + 5906 524.735 5906 524.735 5892.12 502.766 c 0,101,102 + 5876.03 477.308 5876.03 477.308 5845 467.755 c 0,103,104 + 5825.98 461.902 5825.98 461.902 5810.27 461.075 c 0,105,106 + 5800.07 460.503 5800.07 460.503 5782.01 460.5 c 2,0,-1 EndSplineSet EndChar @@ -48219,32 +48270,76 @@ StartChar: uni21E2 Encoding: 8674 8674 1079 -Width: 1233 -Flags: W -LayerCount: 2 -Fore -SplineSet -688 673 m 1,0,-1 - 886 673 l 1,1,-1 - 756 803 l 1,2,-1 - 876 923 l 1,3,-1 - 1167 632 l 1,4,-1 - 1167 490 l 1,5,-1 - 876 199 l 1,6,-1 - 756 319 l 1,7,-1 - 886 449 l 1,8,-1 - 688 449 l 1,9,-1 - 688 673 l 1,0,-1 -563 449 m 1,10,-1 - 376 449 l 1,11,-1 - 376 673 l 1,12,-1 - 563 673 l 1,13,-1 - 563 449 l 1,10,-1 -253 449 m 1,14,-1 - 66 449 l 1,15,-1 - 66 673 l 1,16,-1 - 253 673 l 1,17,-1 - 253 449 l 1,14,-1 +Width: 6062 +VWidth: 2220 +Flags: W +HStem: 460.5 190<174.096 5530.96> +LayerCount: 2 +Fore +SplineSet +5855.56 623.662 m 0,0,1 + 5867.07 618.897 5867.07 618.897 5878.09 608.726 c 0,2,3 + 5901 587.581 5901 587.581 5901 555.25 c 0,4,5 + 5901 523.127 5901 523.127 5881.06 503.188 c 0,6,7 + 5869.86 491.98 5869.86 491.98 5840.97 478.223 c 0,8,9 + 5798.13 457.739 5798.13 457.739 5760.42 433.074 c 128,-1,10 + 5722.52 408.279 5722.52 408.279 5695.91 385.792 c 0,11,12 + 5670.09 363.974 5670.09 363.974 5646.25 336.111 c 0,13,14 + 5621.13 306.707 5621.13 306.707 5606.25 286.253 c 0,15,16 + 5592.15 266.881 5592.15 266.881 5577.19 239.672 c 0,17,18 + 5561.46 211.073 5561.46 211.073 5557.28 202.326 c 1,19,20 + 5551.19 184.575 5551.19 184.575 5538.62 159.442 c 0,21,22 + 5532.2 146.614 5532.2 146.614 5526.82 139.891 c 0,23,24 + 5519.4 130.606 5519.4 130.606 5504.03 121.002 c 2,25,-1 + 5499.81 118.634 l 2,26,27 + 5481.04 109.25 5481.04 109.25 5457 109.25 c 0,28,29 + 5427.22 109.25 5427.22 109.25 5404.7 124.659 c 0,30,31 + 5373 146.352 5373 146.352 5373 186.25 c 0,32,33 + 5373 193.878 5373 193.878 5373.77 200.169 c 128,-1,34 + 5374.55 206.46 5374.55 206.46 5376.78 213.179 c 128,-1,35 + 5379 219.899 5379 219.899 5380.48 223.633 c 128,-1,36 + 5381.96 227.367 5381.96 227.367 5386 236.044 c 128,-1,37 + 5390.04 244.722 5390.04 244.722 5391.81 248.766 c 0,38,39 + 5407.41 284.269 5407.41 284.269 5435.78 333.654 c 0,40,41 + 5465.25 384.958 5465.25 384.958 5517.99 445.69 c 0,42,43 + 5524.23 452.878 5524.23 452.878 5530.99 460.261 c 1,44,-1 + 2734.04 460.5 l 1,45,-1 + 2724.12 460.875 l 1,46,-1 + 2716.39 460.875 l 1,47,-1 + 2694.44 460.5 l 1,48,-1 + 285.011 460 l 2,49,50 + 267.713 459.996 267.713 459.996 257.171 460.579 c 0,51,52 + 241.952 461.424 241.952 461.424 223.002 467.255 c 0,53,54 + 192.97 476.496 192.97 476.496 176.409 500.701 c 0,55,56 + 161 523.223 161 523.223 161 555 c 128,-1,57 + 161 586.777 161 586.777 176.409 609.299 c 0,58,59 + 192.971 633.505 192.971 633.505 223.002 642.745 c 0,60,61 + 241.954 648.576 241.954 648.576 257.181 649.422 c 0,62,63 + 267.571 649.997 267.571 649.997 284.989 650 c 2,64,-1 + 2694.05 650.5 l 1,65,-1 + 2714.07 650.457 l 1,66,-1 + 2724.66 650.224 l 1,67,-1 + 2734.27 650.5 l 1,68,-1 + 5530.96 650.261 l 1,69,70 + 5524.24 657.616 5524.24 657.616 5517.99 664.81 c 0,71,72 + 5465.25 725.541 5465.25 725.541 5435.78 776.846 c 0,73,74 + 5407.41 826.241 5407.41 826.241 5391.81 861.734 c 0,75,76 + 5390.06 865.726 5390.06 865.726 5386.01 874.44 c 128,-1,77 + 5381.96 883.154 5381.96 883.154 5380.49 886.873 c 128,-1,78 + 5379.02 890.591 5379.02 890.591 5376.78 897.332 c 128,-1,79 + 5374.55 904.072 5374.55 904.072 5373.78 910.357 c 128,-1,80 + 5373 916.642 5373 916.642 5373 924.25 c 0,81,82 + 5373 942.139 5373 942.139 5381.92 959.986 c 128,-1,83 + 5390.85 977.833 5390.85 977.833 5407.76 987.982 c 0,84,85 + 5429.87 1001.25 5429.87 1001.25 5457 1001.25 c 0,86,87 + 5492.87 1001.25 5492.87 1001.25 5514.19 982.972 c 2,88,-1 + 5517.17 980.419 l 1,89,-1 + 5519.72 977.44 l 2,90,91 + 5530.57 964.788 5530.57 964.788 5541.67 939.806 c 0,92,93 + 5570.54 873.646 5570.54 873.646 5610.61 817.737 c 0,94,95 + 5647.05 765.794 5647.05 765.794 5688.23 730.442 c 0,96,97 + 5731.27 693.483 5731.27 693.483 5768.94 670.057 c 0,98,99 + 5806.14 646.919 5806.14 646.919 5855.56 623.662 c 0,0,1 EndSplineSet EndChar @@ -68287,5 +68382,162 @@ 358 254 l 1,12,-1 EndSplineSet EndChar + +StartChar: uni290E +Encoding: 10510 10510 1389 +Width: 4863 +VWidth: 2220 +Flags: W +HStem: 460 190<526.64 4693.39> +LayerCount: 2 +Fore +SplineSet +4582.01 460.5 m 2,0,-1 + 2171.85 460 l 1,1,-1 + 2147.36 460.154 l 1,2,-1 + 2137.21 460.241 l 1,3,-1 + 2122.41 460 l 1,4,-1 + 526.64 460 l 1,5,6 + 533.536 452.388 533.536 452.388 539.674 445.246 c 0,7,8 + 591.818 384.59 591.818 384.59 621.222 333.404 c 0,9,10 + 649.427 284.306 649.427 284.306 665.429 249.104 c 0,11,12 + 667.284 245.025 667.284 245.025 671.437 236.4 c 128,-1,13 + 675.589 227.776 675.589 227.776 677.162 223.965 c 128,-1,14 + 678.735 220.155 678.735 220.155 681.046 213.392 c 128,-1,15 + 683.357 206.629 683.357 206.629 684.178 200.206 c 128,-1,16 + 685 193.783 685 193.783 685 186 c 0,17,18 + 685 168.111 685 168.111 676.078 150.264 c 128,-1,19 + 667.155 132.417 667.155 132.417 650.239 122.268 c 0,20,21 + 628.126 109 628.126 109 601 109 c 0,22,23 + 562.875 109 562.875 109 541.438 130.438 c 0,24,25 + 528.24 143.635 528.24 143.635 516.561 169.916 c 0,26,27 + 469.006 272.477 469.006 272.477 399.263 349.194 c 0,28,29 + 337.335 417.314 337.335 417.314 211.192 480.384 c 0,30,31 + 202.353 484.803 202.353 484.803 195.21 489.565 c 128,-1,32 + 188.149 494.273 188.149 494.273 182.31 499.278 c 0,33,34 + 170.991 508.98 170.991 508.98 164.384 522.192 c 0,35,36 + 157 536.96 157 536.96 157 555 c 0,37,38 + 157 565.221 157 565.221 158.194 572.384 c 0,39,40 + 159.313 579.101 159.313 579.101 161.486 584.891 c 128,-1,41 + 163.659 590.682 163.659 590.682 165.713 594.27 c 128,-1,42 + 167.767 597.858 167.767 597.858 171.056 601.384 c 128,-1,43 + 174.346 604.91 174.346 604.91 176.034 606.284 c 128,-1,44 + 177.722 607.658 177.722 607.658 180.939 609.888 c 128,-1,45 + 184.156 612.117 184.156 612.117 184.4 612.3 c 0,46,47 + 191.536 617.651 191.536 617.651 194.21 619.435 c 0,48,49 + 197.794 621.824 197.794 621.824 215 631 c 2,50,-1 + 216.025 631.547 l 1,51,-1 + 217.073 632.046 l 2,52,53 + 275.547 659.891 275.547 659.891 324.524 696.392 c 0,54,55 + 373.814 733.128 373.814 733.128 403.127 763.236 c 0,56,57 + 432.003 794.039 432.003 794.039 457.262 832.829 c 0,58,59 + 486.682 878.009 486.682 878.009 492.775 891.939 c 0,60,61 + 512.518 937.077 512.518 937.077 519.384 950.808 c 0,62,63 + 524.259 960.558 524.259 960.558 526.768 964.739 c 0,64,65 + 531.023 971.832 531.023 971.832 535.597 976.772 c 128,-1,66 + 540.171 981.711 540.171 981.711 542.525 983.359 c 128,-1,67 + 544.879 985.007 544.879 985.007 549.608 987.293 c 128,-1,68 + 554.336 989.579 554.336 989.579 554.997 989.95 c 0,69,70 + 574.642 1001 574.642 1001 601 1001 c 0,71,72 + 630.778 1001 630.778 1001 653.299 985.591 c 0,73,74 + 685 963.9 685 963.9 685 924 c 0,75,76 + 685 916.203 685 916.203 684.179 909.776 c 128,-1,77 + 683.357 903.348 683.357 903.348 681.052 896.6 c 128,-1,78 + 678.746 889.851 678.746 889.851 677.167 886.032 c 128,-1,79 + 675.589 882.212 675.589 882.212 671.444 873.611 c 128,-1,80 + 667.298 865.01 667.298 865.01 665.429 860.896 c 0,81,82 + 649.428 825.698 649.428 825.698 621.222 776.596 c 0,83,84 + 591.768 725.32 591.768 725.32 539.529 665.086 c 0,85,86 + 533.058 657.623 533.058 657.623 526.091 650 c 1,87,-1 + 2122.05 650 l 1,88,-1 + 2136.97 649.968 l 1,89,-1 + 2148.09 649.97 l 1,90,-1 + 2171.98 650 l 1,91,-1 + 4581.99 650.5 l 2,92,93 + 4599.28 650.503 4599.28 650.503 4610.18 649.93 c 0,94,95 + 4625.98 649.098 4625.98 649.098 4645 643.245 c 0,96,97 + 4676.03 633.694 4676.03 633.694 4692.12 608.234 c 0,98,99 + 4706 586.265 4706 586.265 4706 555.5 c 128,-1,100 + 4706 524.735 4706 524.735 4692.12 502.766 c 0,101,102 + 4676.04 477.308 4676.04 477.308 4645 467.755 c 0,103,104 + 4625.98 461.902 4625.98 461.902 4610.23 461.073 c 0,105,106 + 4599.77 460.504 4599.77 460.504 4582.01 460.5 c 2,0,-1 +EndSplineSet +EndChar + +StartChar: uni290F +Encoding: 10511 10511 1390 +Width: 4862 +VWidth: 2220 +Flags: W +HStem: 460 190<173.656 4330.97> +LayerCount: 2 +Fore +SplineSet +4655.56 623.912 m 0,0,1 + 4667.07 619.147 4667.07 619.147 4678.09 608.976 c 0,2,3 + 4701 587.831 4701 587.831 4701 555.5 c 0,4,5 + 4701 523.377 4701 523.377 4681.06 503.438 c 0,6,7 + 4669.86 492.23 4669.86 492.23 4640.97 478.473 c 0,8,9 + 4598.13 457.989 4598.13 457.989 4560.42 433.324 c 128,-1,10 + 4522.52 408.528 4522.52 408.528 4495.91 386.042 c 0,11,12 + 4470.1 364.224 4470.1 364.224 4446.25 336.361 c 0,13,14 + 4421.13 306.958 4421.13 306.958 4406.25 286.503 c 0,15,16 + 4392.15 267.13 4392.15 267.13 4377.19 239.922 c 0,17,18 + 4361.46 211.319 4361.46 211.319 4357.28 202.576 c 1,19,20 + 4351.19 184.828 4351.19 184.828 4338.62 159.692 c 0,21,22 + 4332.2 146.864 4332.2 146.864 4326.82 140.141 c 0,23,24 + 4319.4 130.857 4319.4 130.857 4304.03 121.252 c 2,25,-1 + 4299.81 118.884 l 2,26,27 + 4281.04 109.5 4281.04 109.5 4257 109.5 c 0,28,29 + 4227.22 109.5 4227.22 109.5 4204.7 124.909 c 0,30,31 + 4173 146.602 4173 146.602 4173 186.5 c 0,32,33 + 4173 194.128 4173 194.128 4173.78 200.419 c 128,-1,34 + 4174.55 206.71 4174.55 206.71 4176.78 213.429 c 128,-1,35 + 4179 220.149 4179 220.149 4180.48 223.883 c 128,-1,36 + 4181.97 227.617 4181.97 227.617 4186 236.294 c 128,-1,37 + 4190.03 244.972 4190.03 244.972 4191.81 249.016 c 0,38,39 + 4207.41 284.517 4207.41 284.517 4235.78 333.904 c 0,40,41 + 4265.25 385.208 4265.25 385.208 4317.99 445.94 c 0,42,43 + 4324.24 453.129 4324.24 453.129 4330.97 460.5 c 1,44,-1 + 2734.04 460.5 l 1,45,-1 + 2724.12 460.875 l 1,46,-1 + 2716.39 460.875 l 1,47,-1 + 2694.44 460.5 l 1,48,-1 + 285.011 460 l 2,49,50 + 267.683 459.996 267.683 459.996 257.171 460.579 c 0,51,52 + 241.952 461.424 241.952 461.424 223.002 467.255 c 0,53,54 + 192.97 476.496 192.97 476.496 176.409 500.701 c 0,55,56 + 161 523.223 161 523.223 161 555 c 128,-1,57 + 161 586.777 161 586.777 176.409 609.299 c 0,58,59 + 192.971 633.505 192.971 633.505 223.002 642.745 c 0,60,61 + 241.954 648.576 241.954 648.576 257.181 649.422 c 0,62,63 + 267.571 649.997 267.571 649.997 284.989 650 c 2,64,-1 + 2694.05 650.5 l 1,65,-1 + 2714.07 650.457 l 1,66,-1 + 2724.66 650.224 l 1,67,-1 + 2734.27 650.5 l 1,68,-1 + 4330.97 650.5 l 1,69,70 + 4324.24 657.862 4324.24 657.862 4317.99 665.06 c 0,71,72 + 4265.25 725.789 4265.25 725.789 4235.78 777.096 c 0,73,74 + 4207.41 826.49 4207.41 826.49 4191.81 861.984 c 0,75,76 + 4190.06 865.977 4190.06 865.977 4186.01 874.69 c 128,-1,77 + 4181.96 883.404 4181.96 883.404 4180.49 887.123 c 128,-1,78 + 4179.02 890.842 4179.02 890.842 4176.78 897.582 c 128,-1,79 + 4174.55 904.322 4174.55 904.322 4173.78 910.607 c 128,-1,80 + 4173 916.893 4173 916.893 4173 924.5 c 0,81,82 + 4173 942.389 4173 942.389 4181.92 960.236 c 128,-1,83 + 4190.85 978.083 4190.85 978.083 4207.76 988.232 c 0,84,85 + 4229.87 1001.5 4229.87 1001.5 4257 1001.5 c 0,86,87 + 4292.87 1001.5 4292.87 1001.5 4314.19 983.222 c 2,88,-1 + 4317.17 980.669 l 1,89,-1 + 4319.72 977.69 l 2,90,91 + 4330.57 965.038 4330.57 965.038 4341.67 940.056 c 0,92,93 + 4370.54 873.895 4370.54 873.895 4410.61 817.987 c 0,94,95 + 4447.05 766.044 4447.05 766.044 4488.23 730.692 c 0,96,97 + 4531.27 693.732 4531.27 693.732 4568.94 670.307 c 0,98,99 + 4606.14 647.169 4606.14 647.169 4655.56 623.912 c 0,0,1 +EndSplineSet +EndChar EndChars EndSplineFont diff -r 9c8fc56032e3 -r 2548e7cc86fb lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Tue Dec 29 19:11:23 2015 +0100 +++ b/lib/texinputs/isabellesym.sty Tue Dec 29 20:58:18 2015 +0100 @@ -158,8 +158,12 @@ \newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}} \newcommand{\isasymleftarrow}{\isamath{\leftarrow}} \newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}} +\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}} %requires amsmath +\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}} %requires amsmath \newcommand{\isasymrightarrow}{\isamath{\rightarrow}} \newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}} +\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath +\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath \newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}} \newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}} \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}} diff -r 9c8fc56032e3 -r 2548e7cc86fb src/Doc/Isar_Ref/document/root.tex --- a/src/Doc/Isar_Ref/document/root.tex Tue Dec 29 19:11:23 2015 +0100 +++ b/src/Doc/Isar_Ref/document/root.tex Tue Dec 29 20:58:18 2015 +0100 @@ -1,6 +1,7 @@ \documentclass[12pt,a4paper,fleqn]{report} \usepackage{lmodern} \usepackage[T1]{fontenc} +\usepackage{amsmath} \usepackage{amssymb} \usepackage{wasysym} \usepackage{eurosym}