From: Stefano Zacchiroli Date: Thu, 26 Jan 2006 09:56:55 +0000 (+0000) Subject: - added components diagram with KLOCs X-Git-Tag: make_still_working~7765 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=37191f82d959769e24166fd8225e0ff86f717586;p=helm.git - added components diagram with KLOCs - fixed some dangling references --- diff --git a/helm/papers/matita/libraries-clusters.png b/helm/papers/matita/libraries-clusters.png new file mode 100644 index 000000000..d3e52763e Binary files /dev/null and b/helm/papers/matita/libraries-clusters.png differ diff --git a/helm/papers/matita/libraries-clusters.ps b/helm/papers/matita/libraries-clusters.ps new file mode 100644 index 000000000..ed37f5fe5 --- /dev/null +++ b/helm/papers/matita/libraries-clusters.ps @@ -0,0 +1,1820 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005) +%%For: (zacchiro) Stefano Zacchiroli,,, +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 1079 1753 +%%EndComments +save +%%BeginProlog +/DotDict 200 dict def +DotDict begin + +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + +%%BeginResource: procset graphviz 0 0 +/coord-font-family /Times-Roman def +/default-font-family /Times-Roman def +/coordfont coord-font-family findfont 8 scalefont def + +/InvScaleFactor 1.0 def +/set_scale { + dup 1 exch div /InvScaleFactor exch def + dup scale +} bind def + +% styles +/solid { [] 0 setdash } bind def +/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def +/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def +/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def +/bold { 2 setlinewidth } bind def +/filled { } bind def +/unfilled { } bind def +/rounded { } bind def +/diagonals { } bind def + +% hooks for setting color +/nodecolor { sethsbcolor } bind def +/edgecolor { sethsbcolor } bind def +/graphcolor { sethsbcolor } bind def +/nopcolor {pop pop pop} bind def + +/beginpage { % i j npages + /npages exch def + /j exch def + /i exch def + /str 10 string def + npages 1 gt { + gsave + coordfont setfont + 0 0 moveto + (\() show i str cvs show (,) show j str cvs show (\)) show + grestore + } if +} bind def + +/set_font { + findfont exch + scalefont setfont +} def + +% draw aligned label in bounding box aligned to current point +/alignedtext { % width adj text + /text exch def + /adj exch def + /width exch def + gsave + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if + [] 0 setdash + text show + grestore +} def + +/boxprim { % xcorner ycorner xsize ysize + 4 2 roll + moveto + 2 copy + exch 0 rlineto + 0 exch rlineto + pop neg 0 rlineto + closepath +} bind def + +/ellipse_path { + /ry exch def + /rx exch def + /y exch def + /x exch def + matrix currentmatrix + newpath + x y translate + rx ry scale + 0 0 1 0 360 arc + setmatrix +} bind def + +/endpage { showpage } bind def +/showpage { } def + +/layercolorseq + [ % layer color sequence - darkest to lightest + [0 0 0] + [.2 .8 .8] + [.4 .8 .8] + [.6 .8 .8] + [.8 .8 .8] + ] +def + +/layerlen layercolorseq length def + +/setlayer {/maxlayer exch def /curlayer exch def + layercolorseq curlayer 1 sub layerlen mod get + aload pop sethsbcolor + /nodecolor {nopcolor} def + /edgecolor {nopcolor} def + /graphcolor {nopcolor} def +} bind def + +/onlayer { curlayer ne {invis} if } def + +/onlayers { + /myupper exch def + /mylower exch def + curlayer mylower lt + curlayer myupper gt + or + {invis} if +} def + +/curlayer 0 def + +%%EndResource +%%EndProlog +%%BeginSetup +14 default-font-family set_font +1 setmiterlimit +% /arrowlength 10 def +% /arrowwidth 5 def + +% make sure pdfmark is harmless for PS-interpreters other than Distiller +/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse +% make '<<' and '>>' safe on PS Level 1 devices +/languagelevel where {pop languagelevel}{1} ifelse +2 lt { + userdict (<<) cvn ([) cvn load put + userdict (>>) cvn ([) cvn load put +} if + +%%EndSetup +%%Page: 1 1 +%%PageBoundingBox: 36 36 1079 1753 +%%PageOrientation: Portrait +gsave +35 35 1044 1718 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +24.00 /Times-Roman set_font +% cluster_presentation +gsave 10 dict begin +filled +0.000 0.000 1.000 sethsbcolor +0.000 0.000 0.929 sethsbcolor +newpath 486 1080 moveto +918 1080 lineto +918 1624 lineto +486 1624 lineto +closepath +fill +0.000 0.000 1.000 sethsbcolor +newpath 486 1080 moveto +918 1080 lineto +918 1624 lineto +486 1624 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 sethsbcolor +497 1090 moveto +(Terms at the content and presentation level) +[14.64 10.56 7.92 18.72 9.36 6 10.56 6.72 6 6.72 12 10.56 6 10.56 12 12 6.72 10.56 12 6.72 6 10.56 12 12 6 12 7.92 10.56 9.36 10.56 12 6.72 10.56 6.72 6.72 12 12 6 6.72 10.56 12 10.56 6.72] +xshow +end grestore +end grestore +% cluster_partially +gsave 10 dict begin +filled +0.000 0.000 1.000 sethsbcolor +0.000 0.000 0.929 sethsbcolor +newpath 68 1116 moveto +360 1116 lineto +360 1516 lineto +68 1516 lineto +closepath +fill +0.000 0.000 1.000 sethsbcolor +newpath 68 1116 moveto +360 1116 lineto +360 1516 lineto +68 1516 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 sethsbcolor +76 1490 moveto +(Partially specified terms) +[13.44 10.56 7.92 6.72 6.72 10.56 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] +xshow +end grestore +end grestore +% cluster_fully +gsave 10 dict begin +filled +0.000 0.000 1.000 sethsbcolor +0.000 0.000 0.929 sethsbcolor +newpath 280 416 moveto +574 416 lineto +574 1072 lineto +280 1072 lineto +closepath +fill +0.000 0.000 1.000 sethsbcolor +newpath 280 416 moveto +574 416 lineto +574 1072 lineto +280 1072 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 sethsbcolor +287 426 moveto +(Fully specified terms) +[13.44 12 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] +xshow +end grestore +end grestore +% cluster_utilities +gsave 10 dict begin +filled +0.000 0.000 1.000 sethsbcolor +0.000 0.000 0.929 sethsbcolor +newpath 582 16 moveto +1034 16 lineto +1034 560 lineto +582 560 lineto +closepath +fill +0.000 0.000 1.000 sethsbcolor +newpath 582 16 moveto +1034 16 lineto +1034 560 lineto +582 560 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 sethsbcolor +948 26 moveto +(Utilities) +[17.28 6.72 6.72 6.72 6.72 6.72 6.72 10.56 9.36] +xshow +end grestore +end grestore + +% acic_content +gsave 10 dict begin +610 1170 81 45 ellipse_path +stroke +gsave 10 dict begin +549 1176 moveto +(acic_content) +[10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72] +xshow +566 1148 moveto +(3.6 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% cic_acic +gsave 10 dict begin +353 890 64 45 ellipse_path +stroke +gsave 10 dict begin +313 896 moveto +(cic_acic) +[10.56 6.72 10.56 12 10.56 10.56 6.72 10.56] +xshow +309 868 moveto +(2.4 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% acic_content -> cic_acic +newpath 602 1124 moveto +593 1069 576 983 565 972 curveto +521 926 486 961 427 936 curveto +421 933 415 930 409 927 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 410 924 moveto +400 922 lineto +407 930 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 410 924 moveto +400 922 lineto +407 930 lineto +closepath +stroke +end grestore + +% cic_disambiguation +gsave 10 dict begin +610 1298 115 45 ellipse_path +stroke +gsave 10 dict begin +515 1304 moveto +(cic_disambiguation) +[10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12] +xshow +567 1276 moveto +(1.4 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% cic_disambiguation -> acic_content +newpath 610 1252 moveto +610 1244 610 1235 610 1226 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 614 1226 moveto +610 1216 lineto +607 1226 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 614 1226 moveto +610 1216 lineto +607 1226 lineto +closepath +stroke +end grestore + +% cic_unification +gsave 10 dict begin +259 1170 92 45 ellipse_path +stroke +gsave 10 dict begin +187 1176 moveto +(cic_unification) +[10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12] +xshow +215 1148 moveto +(3.4 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% cic_disambiguation -> cic_unification +newpath 525 1267 moveto +469 1247 399 1221 344 1201 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 345 1197 moveto +334 1197 lineto +342 1204 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 345 1197 moveto +334 1197 lineto +342 1204 lineto +closepath +stroke +end grestore + +% whelp +gsave 10 dict begin +497 1018 58 45 ellipse_path +stroke +gsave 10 dict begin +467 1024 moveto +(whelp) +[17.28 12 10.56 6.72 12] +xshow +459 996 moveto +(.3 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% cic_disambiguation -> whelp +newpath 553 1258 moveto +540 1246 527 1232 519 1216 curveto +497 1172 493 1116 493 1074 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 497 1074 moveto +493 1064 lineto +490 1074 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 497 1074 moveto +493 1064 lineto +490 1074 lineto +closepath +stroke +end grestore + +% content_pres +gsave 10 dict begin +827 1298 82 45 ellipse_path +stroke +gsave 10 dict begin +765 1304 moveto +(content_pres) +[10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] +xshow +783 1276 moveto +(4.5 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% content_pres -> acic_content +newpath 770 1265 moveto +741 1248 705 1226 675 1208 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 676 1205 moveto +666 1203 lineto +673 1211 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 676 1205 moveto +666 1203 lineto +673 1211 lineto +closepath +stroke +end grestore + +% utf8_macros +gsave 10 dict begin +944 506 81 45 ellipse_path +stroke +gsave 10 dict begin +883 512 moveto +(utf8_macros) +[12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36] +xshow +906 484 moveto +(.2 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% content_pres -> utf8_macros +newpath 842 1253 moveto +859 1198 885 1102 885 1018 curveto +885 1018 885 1018 885 762 curveto +885 691 907 612 924 561 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 927 562 moveto +927 551 lineto +921 560 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 927 562 moveto +927 551 lineto +921 560 lineto +closepath +stroke +end grestore + +% grafite_parser +gsave 10 dict begin +582 1570 87 45 ellipse_path +stroke +gsave 10 dict begin +515 1576 moveto +(grafite_parser) +[12 7.92 10.56 7.92 6.72 6.72 10.56 12 12 10.56 7.92 9.36 10.56 7.92] +xshow +539 1548 moveto +(1.8 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% lexicon +gsave 10 dict begin +610 1426 58 45 ellipse_path +stroke +gsave 10 dict begin +574 1432 moveto +(lexicon) +[6.72 10.56 12 6.72 10.56 12 12] +xshow +572 1404 moveto +(.8 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% grafite_parser -> lexicon +newpath 591 1524 moveto +593 1510 596 1495 599 1481 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 602 1481 moveto +601 1471 lineto +596 1480 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 602 1481 moveto +601 1471 lineto +596 1480 lineto +closepath +stroke +end grestore + +% grafite +gsave 10 dict begin +135 1298 58 45 ellipse_path +stroke +gsave 10 dict begin +103 1304 moveto +(grafite) +[12 7.92 10.56 7.92 6.72 6.72 10.56] +xshow +97 1276 moveto +(.5 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% grafite_parser -> grafite +newpath 524 1535 moveto +515 1531 504 1527 494 1524 curveto +476 1519 339 1527 323 1516 curveto +273 1477 323 1427 281 1380 curveto +256 1351 236 1364 203 1344 curveto +197 1340 193 1336 189 1333 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 192 1331 moveto +182 1326 lineto +187 1336 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 192 1331 moveto +182 1326 lineto +187 1336 lineto +closepath +stroke +end grestore + +% lexicon -> cic_disambiguation +newpath 610 1380 moveto +610 1372 610 1363 610 1354 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 614 1354 moveto +610 1344 lineto +607 1354 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 614 1354 moveto +610 1344 lineto +607 1354 lineto +closepath +stroke +end grestore + +% lexicon -> content_pres +newpath 657 1398 moveto +687 1381 728 1356 761 1337 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 763 1340 moveto +770 1332 lineto +760 1334 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 763 1340 moveto +770 1332 lineto +760 1334 lineto +closepath +stroke +end grestore + +% library +gsave 10 dict begin +353 1018 64 45 ellipse_path +stroke +gsave 10 dict begin +321 1024 moveto +(library) +[6.72 6.72 12 7.92 10.56 7.92 12] +xshow +309 996 moveto +(2.1 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% cic_unification -> library +newpath 286 1126 moveto +297 1108 311 1088 322 1069 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 325 1070 moveto +327 1060 lineto +319 1067 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 325 1070 moveto +327 1060 lineto +319 1067 lineto +closepath +stroke +end grestore + +% tactics +gsave 10 dict begin +282 1298 69 45 ellipse_path +stroke +gsave 10 dict begin +251 1304 moveto +(tactics) +[6.72 10.56 10.56 6.72 6.72 10.56 9.36] +xshow +233 1276 moveto +(10.0 klocs) +[12 12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% tactics -> cic_unification +newpath 274 1253 moveto +273 1244 271 1235 269 1226 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 272 1225 moveto +267 1216 lineto +266 1226 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 272 1225 moveto +267 1216 lineto +266 1226 lineto +closepath +stroke +end grestore + +% tactics -> whelp +newpath 230 1267 moveto +198 1247 161 1224 157 1216 curveto +129 1162 115 1123 157 1080 curveto +168 1069 413 1077 427 1072 curveto +436 1069 444 1065 452 1059 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 454 1062 moveto +460 1053 lineto +450 1056 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 454 1062 moveto +460 1053 lineto +450 1056 lineto +closepath +stroke +end grestore + +% cic +gsave 10 dict begin +353 634 64 45 ellipse_path +stroke +gsave 10 dict begin +339 640 moveto +(cic) +[10.56 6.72 10.56] +xshow +309 612 moveto +(4.2 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% grafite -> cic +newpath 122 1253 moveto +108 1198 86 1102 86 1018 curveto +86 1018 86 1018 86 890 curveto +86 869 86 861 96 844 curveto +110 822 230 728 301 674 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 303 677 moveto +309 668 lineto +299 671 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 303 677 moveto +309 668 lineto +299 671 lineto +closepath +stroke +end grestore + +% grafite_engine +gsave 10 dict begin +181 1426 90 45 ellipse_path +stroke +gsave 10 dict begin +111 1432 moveto +(grafite_engine) +[12 7.92 10.56 7.92 6.72 6.72 10.56 12 10.56 12 12 6.72 12 10.56] +xshow +138 1404 moveto +(1.2 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% grafite_engine -> tactics +newpath 191 1380 moveto +200 1364 213 1350 227 1338 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 229 1341 moveto +234 1331 lineto +224 1336 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 229 1341 moveto +234 1331 lineto +224 1336 lineto +closepath +stroke +end grestore + +% grafite_engine -> grafite +newpath 165 1381 moveto +162 1371 158 1361 155 1351 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 158 1350 moveto +151 1342 lineto +152 1353 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 158 1350 moveto +151 1342 lineto +152 1353 lineto +closepath +stroke +end grestore + +% urimanager +gsave 10 dict begin +380 506 76 45 ellipse_path +stroke +gsave 10 dict begin +324 512 moveto +(urimanager) +[12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92] +xshow +342 484 moveto +(.2 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% cic -> urimanager +newpath 363 589 moveto +364 580 366 570 368 561 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 371 561 moveto +370 551 lineto +365 560 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 371 561 moveto +370 551 lineto +365 560 lineto +closepath +stroke +end grestore + +% xml +gsave 10 dict begin +652 234 58 45 ellipse_path +stroke +gsave 10 dict begin +633 240 moveto +(xml) +[12 18.72 6.72] +xshow +614 212 moveto +(.5 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% cic -> xml +newpath 315 596 moveto +307 585 299 573 294 560 curveto +273 499 261 470 294 416 curveto +357 312 500 266 584 246 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 585 249 moveto +594 244 lineto +584 243 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 585 249 moveto +594 244 lineto +584 243 lineto +closepath +stroke +end grestore + +% cic_proof_checking +gsave 10 dict begin +405 762 116 45 ellipse_path +stroke +gsave 10 dict begin +309 768 moveto +(cic_proof_checking) +[10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12] +xshow +361 740 moveto +(5.8 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% cic_proof_checking -> cic +newpath 387 717 moveto +383 707 379 697 375 687 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 378 686 moveto +371 678 lineto +372 689 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 378 686 moveto +371 678 lineto +372 689 lineto +closepath +stroke +end grestore + +% getter +gsave 10 dict begin +501 634 64 45 ellipse_path +stroke +gsave 10 dict begin +473 640 moveto +(getter) +[12 10.56 6.72 6.72 10.56 7.92] +xshow +457 612 moveto +(2.0 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% cic_proof_checking -> getter +newpath 415 716 moveto +423 700 436 686 449 674 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 451 677 moveto +456 667 lineto +446 672 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 451 677 moveto +456 667 lineto +446 672 lineto +closepath +stroke +end grestore + +% getter -> urimanager +newpath 465 596 moveto +452 583 438 568 425 554 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 427 551 moveto +418 546 lineto +422 556 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 427 551 moveto +418 546 lineto +422 556 lineto +closepath +stroke +end grestore + +% registry +gsave 10 dict begin +789 362 58 45 ellipse_path +stroke +gsave 10 dict begin +751 368 moveto +(registry) +[7.92 10.56 12 6.72 9.36 6.72 7.92 12] +xshow +751 340 moveto +(.6 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% getter -> registry +newpath 504 588 moveto +510 537 527 456 581 416 curveto +594 406 707 412 721 408 curveto +727 406 733 403 739 400 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 741 403 moveto +748 395 lineto +738 397 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 741 403 moveto +748 395 lineto +738 397 lineto +closepath +stroke +end grestore + +% logger +gsave 10 dict begin +649 506 58 45 ellipse_path +stroke +gsave 10 dict begin +618 512 moveto +(logger) +[6.72 12 12 12 10.56 7.92] +xshow +611 484 moveto +(.1 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% getter -> logger +newpath 542 598 moveto +560 582 583 563 601 547 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 604 549 moveto +609 540 lineto +599 544 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 604 549 moveto +609 540 lineto +599 544 lineto +closepath +stroke +end grestore + +% metadata +gsave 10 dict begin +501 890 64 45 ellipse_path +stroke +gsave 10 dict begin +457 896 moveto +(metadata) +[18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] +xshow +458 868 moveto +(1.9 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% metadata -> cic +newpath 520 846 moveto +525 834 529 821 531 808 curveto +535 787 543 732 531 716 curveto +503 676 471 703 427 680 curveto +420 676 415 673 411 669 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 414 667 moveto +404 662 lineto +409 672 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 414 667 moveto +404 662 lineto +409 672 lineto +closepath +stroke +end grestore + +% hmysql +gsave 10 dict begin +785 506 58 45 ellipse_path +stroke +gsave 10 dict begin +749 512 moveto +(hmysql) +[12 18.72 12 9.36 12 6.72] +xshow +747 484 moveto +(.1 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% metadata -> hmysql +newpath 563 876 moveto +625 861 715 835 737 808 curveto +794 738 797 628 792 561 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 795 561 moveto +791 551 lineto +789 561 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 795 561 moveto +791 551 lineto +789 561 lineto +closepath +stroke +end grestore + +% whelp -> metadata +newpath 498 973 moveto +499 964 499 955 499 946 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 502 946 moveto +500 936 lineto +496 946 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 502 946 moveto +500 936 lineto +496 946 lineto +closepath +stroke +end grestore + +% library -> metadata +newpath 394 982 moveto +412 966 433 948 452 932 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 455 934 moveto +460 925 lineto +450 929 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 455 934 moveto +460 925 lineto +450 929 lineto +closepath +stroke +end grestore + +% library -> cic_acic +newpath 353 972 moveto +353 964 353 955 353 946 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 357 946 moveto +353 936 lineto +350 946 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 357 946 moveto +353 936 lineto +350 946 lineto +closepath +stroke +end grestore + +% cic_acic -> cic_proof_checking +newpath 371 846 moveto +375 836 379 826 383 816 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 386 818 moveto +387 807 lineto +380 815 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 386 818 moveto +387 807 lineto +380 815 lineto +closepath +stroke +end grestore + +% extlib +gsave 10 dict begin +654 106 63 45 ellipse_path +stroke +gsave 10 dict begin +626 112 moveto +(extlib) +[10.56 12 6.72 6.72 6.72 12] +xshow +611 84 moveto +(1.1 klocs) +[12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% hgdome +gsave 10 dict begin +651 362 60 45 ellipse_path +stroke +gsave 10 dict begin +611 368 moveto +(hgdome) +[12 12 12 12 18.72 10.56] +xshow +613 340 moveto +(.2 klocs) +[6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% hgdome -> xml +newpath 651 316 moveto +651 308 651 299 652 290 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 656 290 moveto +652 280 lineto +649 290 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 656 290 moveto +652 280 lineto +649 290 lineto +closepath +stroke +end grestore + +% hmysql -> registry +newpath 786 460 moveto +786 446 787 432 787 418 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 791 418 moveto +787 408 lineto +784 418 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 791 418 moveto +787 408 lineto +784 418 lineto +closepath +stroke +end grestore + +% registry -> xml +newpath 751 327 moveto +734 311 715 292 697 276 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 700 274 moveto +690 269 lineto +695 279 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 700 274 moveto +690 269 lineto +695 279 lineto +closepath +stroke +end grestore + +% xml -> extlib +newpath 653 188 moveto +653 180 653 171 653 162 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 657 162 moveto +653 152 lineto +650 162 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 657 162 moveto +653 152 lineto +650 162 lineto +closepath +stroke +end grestore + +% DependencyAnalyzer +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 748 1064 moveto +612 1064 lineto +612 972 lineto +748 972 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 748 1064 moveto +612 1064 lineto +612 972 lineto +748 972 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +620 1038 moveto +(Dependency) +[17.28 10.56 12 10.56 12 12 10.56 12 10.56 12] +xshow +636 1010 moveto +(Analyzer) +[17.28 12 10.56 6.72 12 10.56 10.56 7.92] +xshow +639 982 moveto +( .3 klocs) +[6 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% DependencyAnalyzer -> metadata +newpath 616 972 moveto +596 958 574 942 555 928 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 557 925 moveto +547 922 lineto +553 931 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 557 925 moveto +547 922 lineto +553 931 lineto +closepath +stroke +end grestore + +% Getter +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 680 794 moveto +582 794 lineto +582 730 lineto +680 730 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 680 794 moveto +582 794 lineto +582 730 lineto +680 730 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +601 768 moveto +(Getter) +[17.28 10.56 6.72 6.72 10.56 7.92] +xshow +590 740 moveto +( .3 klocs) +[6 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% Getter -> getter +newpath 598 730 moveto +582 714 563 695 546 678 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 549 676 moveto +539 671 lineto +544 681 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 549 676 moveto +539 671 lineto +544 681 lineto +closepath +stroke +end grestore + +% Matita +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 236 1716 moveto +126 1716 lineto +126 1652 lineto +236 1652 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 236 1716 moveto +126 1716 lineto +126 1652 lineto +236 1652 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +149 1690 moveto +(Matita) +[21.36 10.56 6.72 6.72 6.72 10.56] +xshow +134 1662 moveto +( 6.7 klocs) +[6 12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% Matita -> grafite_parser +newpath 236 1679 moveto +300 1673 408 1657 494 1624 curveto +503 1620 512 1616 520 1611 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 522 1614 moveto +529 1606 lineto +519 1608 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 522 1614 moveto +529 1606 lineto +519 1608 lineto +closepath +stroke +end grestore + +% Matita -> grafite_engine +newpath 181 1652 moveto +181 1610 181 1534 181 1482 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 185 1482 moveto +181 1472 lineto +178 1482 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 185 1482 moveto +181 1472 lineto +178 1482 lineto +closepath +stroke +end grestore + +% Matita -> hgdome +newpath 152 1652 moveto +125 1620 86 1568 64 1516 curveto +49 1478 48 1466 48 1426 curveto +48 1426 48 1426 48 634 curveto +48 493 150 477 276 416 curveto +328 391 487 374 580 367 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 580 370 moveto +590 366 lineto +580 364 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 580 370 moveto +590 366 lineto +580 364 lineto +closepath +stroke +end grestore + +% ProofChecker +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 270 922 moveto +114 922 lineto +114 858 lineto +270 858 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 270 922 moveto +114 922 lineto +114 858 lineto +270 858 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +122 896 moveto +(Proof Checker) +[13.44 7.92 12 12 7.92 6 16.08 12 10.56 10.56 12 10.56 7.92] +xshow +151 868 moveto +( .1 klocs) +[6 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% ProofChecker -> cic_proof_checking +newpath 245 858 moveto +271 842 304 823 332 805 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 334 808 moveto +341 800 lineto +331 802 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 334 808 moveto +341 800 lineto +331 802 lineto +closepath +stroke +end grestore + +% Uwobo +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 478 1458 moveto +368 1458 lineto +368 1394 lineto +478 1394 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 478 1458 moveto +368 1458 lineto +368 1394 lineto +478 1394 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +387 1432 moveto +(Uwobo) +[17.28 17.28 12 12 12] +xshow +376 1404 moveto +( 2.1 klocs) +[6 12 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% Uwobo -> content_pres +newpath 459 1394 moveto +466 1388 474 1384 482 1380 curveto +587 1335 627 1377 735 1344 curveto +743 1341 751 1338 759 1335 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 760 1338 moveto +768 1331 lineto +757 1332 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 760 1338 moveto +768 1331 lineto +757 1332 lineto +closepath +stroke +end grestore + +% Whelp +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 631 1716 moveto +533 1716 lineto +533 1652 lineto +631 1652 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 631 1716 moveto +533 1716 lineto +533 1652 lineto +631 1652 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +549 1690 moveto +(Whelp) +[22.56 12 10.56 6.72 12] +xshow +541 1662 moveto +( .6 klocs) +[6 6 12 6 12 6.72 12 10.56 9.36] +xshow +end grestore +end grestore + +% Whelp -> grafite_parser +newpath 582 1652 moveto +582 1644 582 1635 582 1626 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 586 1626 moveto +582 1616 lineto +579 1626 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 586 1626 moveto +582 1616 lineto +579 1626 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/helm/papers/matita/librariesCluster.ps b/helm/papers/matita/librariesCluster.ps deleted file mode 100644 index c6ee33271..000000000 --- a/helm/papers/matita/librariesCluster.ps +++ /dev/null @@ -1,1705 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005) -%%For: (sacerdot) Claudio Sacerdoti Coen,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: 35 35 933 1263 -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval - -EncodingVector - dup 306 /AE - dup 301 /Aacute - dup 302 /Acircumflex - dup 304 /Adieresis - dup 300 /Agrave - dup 305 /Aring - dup 303 /Atilde - dup 307 /Ccedilla - dup 311 /Eacute - dup 312 /Ecircumflex - dup 313 /Edieresis - dup 310 /Egrave - dup 315 /Iacute - dup 316 /Icircumflex - dup 317 /Idieresis - dup 314 /Igrave - dup 334 /Udieresis - dup 335 /Yacute - dup 376 /thorn - dup 337 /germandbls - dup 341 /aacute - dup 342 /acircumflex - dup 344 /adieresis - dup 346 /ae - dup 340 /agrave - dup 345 /aring - dup 347 /ccedilla - dup 351 /eacute - dup 352 /ecircumflex - dup 353 /edieresis - dup 350 /egrave - dup 355 /iacute - dup 356 /icircumflex - dup 357 /idieresis - dup 354 /igrave - dup 360 /dcroat - dup 361 /ntilde - dup 363 /oacute - dup 364 /ocircumflex - dup 366 /odieresis - dup 362 /ograve - dup 365 /otilde - dup 370 /oslash - dup 372 /uacute - dup 373 /ucircumflex - dup 374 /udieresis - dup 371 /ugrave - dup 375 /yacute - dup 377 /ydieresis - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -%%Page: 1 1 -%%PageBoundingBox: 36 36 933 1263 -%%PageOrientation: Portrait -gsave -35 35 898 1228 boxprim clip newpath -36 36 translate -0 0 1 beginpage -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor -24.00 /Times-Roman set_font -% cluster_presentation -gsave 10 dict begin -filled -0.000 0.000 1.000 sethsbcolor -0.000 0.000 0.929 sethsbcolor -newpath 436 778 moveto -865 778 lineto -865 1162 lineto -436 1162 lineto -closepath -fill -0.000 0.000 1.000 sethsbcolor -newpath 436 778 moveto -865 778 lineto -865 1162 lineto -436 1162 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 sethsbcolor -444 788 moveto -(Terms at the content and presentation level) -[14.64 10.56 7.92 18.72 9.36 6 10.56 6.72 6 6.72 12 10.56 6 10.56 12 12 6.72 10.56 12 6.72 6 10.56 12 12 6 12 7.92 10.56 9.36 10.56 12 6.72 10.56 6.72 6.72 12 12 6 6.72 10.56 12 10.56 6.72] -xshow -end grestore -end grestore -% cluster_partially -gsave 10 dict begin -filled -0.000 0.000 1.000 sethsbcolor -0.000 0.000 0.929 sethsbcolor -newpath 84 814 moveto -334 814 lineto -334 1094 lineto -84 1094 lineto -closepath -fill -0.000 0.000 1.000 sethsbcolor -newpath 84 814 moveto -334 814 lineto -334 1094 lineto -84 1094 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 sethsbcolor -92 1068 moveto -(Partially specified terms) -[13.44 10.56 7.92 6.72 6.72 10.56 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] -xshow -end grestore -end grestore -% cluster_fully -gsave 10 dict begin -filled -0.000 0.000 1.000 sethsbcolor -0.000 0.000 0.929 sethsbcolor -newpath 220 296 moveto -482 296 lineto -482 770 lineto -220 770 lineto -closepath -fill -0.000 0.000 1.000 sethsbcolor -newpath 220 296 moveto -482 296 lineto -482 770 lineto -220 770 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 sethsbcolor -227 306 moveto -(Fully specified terms) -[13.44 12 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] -xshow -end grestore -end grestore -% cluster_utilities -gsave 10 dict begin -filled -0.000 0.000 1.000 sethsbcolor -0.000 0.000 0.929 sethsbcolor -newpath 490 16 moveto -888 16 lineto -888 400 lineto -490 400 lineto -closepath -fill -0.000 0.000 1.000 sethsbcolor -newpath 490 16 moveto -888 16 lineto -888 400 lineto -490 400 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 sethsbcolor -802 26 moveto -(Utilities) -[17.28 6.72 6.72 6.72 6.72 6.72 6.72 10.56 9.36] -xshow -end grestore -end grestore - -% acic_content -gsave 10 dict begin -554 848 75 25 ellipse_path -stroke -gsave 10 dict begin -493 840 moveto -(acic_content) -[10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72] -xshow -end grestore -end grestore - -% cic_acic -gsave 10 dict begin -283 636 54 25 ellipse_path -stroke -gsave 10 dict begin -243 628 moveto -(cic_acic) -[10.56 6.72 10.56 12 10.56 10.56 6.72 10.56] -xshow -end grestore -end grestore - -% acic_content -> cic_acic -newpath 530 824 moveto -517 809 500 789 487 770 curveto -470 742 482 725 458 704 curveto -420 669 395 687 347 668 curveto -341 665 335 663 329 660 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 330 657 moveto -320 655 lineto -327 663 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 330 657 moveto -320 655 lineto -327 663 lineto -closepath -stroke -end grestore - -% cic_disambiguation -gsave 10 dict begin -554 936 109 25 ellipse_path -stroke -gsave 10 dict begin -459 928 moveto -(cic_disambiguation) -[10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12] -xshow -end grestore -end grestore - -% cic_disambiguation -> acic_content -newpath 554 910 moveto -554 902 554 893 554 884 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 558 884 moveto -554 874 lineto -551 884 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 558 884 moveto -554 874 lineto -551 884 lineto -closepath -stroke -end grestore - -% cic_unification -gsave 10 dict begin -239 848 86 25 ellipse_path -stroke -gsave 10 dict begin -167 840 moveto -(cic_unification) -[10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12] -xshow -end grestore -end grestore - -% cic_disambiguation -> cic_unification -newpath 484 916 moveto -433 902 364 883 312 869 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 313 866 moveto -302 866 lineto -311 872 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 313 866 moveto -302 866 lineto -311 872 lineto -closepath -stroke -end grestore - -% whelp -gsave 10 dict begin -404 736 44 25 ellipse_path -stroke -gsave 10 dict begin -374 728 moveto -(whelp) -[17.28 12 10.56 6.72 12] -xshow -end grestore -end grestore - -% cic_disambiguation -> whelp -newpath 513 912 moveto -498 902 481 889 469 874 curveto -444 843 426 801 415 771 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 418 770 moveto -412 761 lineto -412 772 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 418 770 moveto -412 761 lineto -412 772 lineto -closepath -stroke -end grestore - -% content_pres -gsave 10 dict begin -759 936 76 25 ellipse_path -stroke -gsave 10 dict begin -697 928 moveto -(content_pres) -[10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] -xshow -end grestore -end grestore - -% content_pres -> acic_content -newpath 712 916 moveto -681 903 642 886 610 872 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 612 869 moveto -601 868 lineto -609 875 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 612 869 moveto -601 868 lineto -609 875 lineto -closepath -stroke -end grestore - -% utf8_macros -gsave 10 dict begin -804 366 75 25 ellipse_path -stroke -gsave 10 dict begin -743 358 moveto -(utf8_macros) -[12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36] -xshow -end grestore -end grestore - -% content_pres -> utf8_macros -newpath 764 910 moveto -770 872 781 799 781 736 curveto -781 736 781 736 781 542 curveto -781 493 790 437 797 401 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 800 401 moveto -799 391 lineto -794 400 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 800 401 moveto -799 391 lineto -794 400 lineto -closepath -stroke -end grestore - -% grafite_parser -gsave 10 dict begin -526 1128 81 25 ellipse_path -stroke -gsave 10 dict begin -459 1120 moveto -(grafite_parser) -[12 7.92 10.56 7.92 6.72 6.72 10.56 12 12 10.56 7.92 9.36 10.56 7.92] -xshow -end grestore -end grestore - -% lexicon -gsave 10 dict begin -554 1024 50 25 ellipse_path -stroke -gsave 10 dict begin -518 1016 moveto -(lexicon) -[6.72 10.56 12 6.72 10.56 12 12] -xshow -end grestore -end grestore - -% grafite_parser -> lexicon -newpath 533 1103 moveto -536 1090 541 1074 545 1059 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 548 1059 moveto -547 1049 lineto -542 1058 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 548 1059 moveto -547 1049 lineto -542 1058 lineto -closepath -stroke -end grestore - -% grafite -gsave 10 dict begin -139 936 46 25 ellipse_path -stroke -gsave 10 dict begin -107 928 moveto -(grafite) -[12 7.92 10.56 7.92 6.72 6.72 10.56] -xshow -end grestore -end grestore - -% grafite_parser -> grafite -newpath 472 1108 moveto -463 1106 453 1103 444 1102 curveto -430 1099 324 1102 312 1094 curveto -276 1066 309 1031 277 998 curveto -250 968 231 980 195 962 curveto -192 960 189 958 186 956 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 188 953 moveto -178 950 lineto -184 959 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 188 953 moveto -178 950 lineto -184 959 lineto -closepath -stroke -end grestore - -% lexicon -> cic_disambiguation -newpath 554 998 moveto -554 990 554 981 554 972 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 558 972 moveto -554 962 lineto -551 972 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 558 972 moveto -554 962 lineto -551 972 lineto -closepath -stroke -end grestore - -% lexicon -> content_pres -newpath 593 1007 moveto -624 994 668 976 702 960 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 704 963 moveto -712 956 lineto -701 956 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 704 963 moveto -712 956 lineto -701 956 lineto -closepath -stroke -end grestore - -% library -gsave 10 dict begin -283 736 46 25 ellipse_path -stroke -gsave 10 dict begin -251 728 moveto -(library) -[6.72 6.72 12 7.92 10.56 7.92 12] -xshow -end grestore -end grestore - -% cic_unification -> library -newpath 249 823 moveto -255 808 263 788 269 771 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 273 772 moveto -273 761 lineto -266 769 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 273 772 moveto -273 761 lineto -266 769 lineto -closepath -stroke -end grestore - -% tactics -gsave 10 dict begin -250 936 45 25 ellipse_path -stroke -gsave 10 dict begin -219 928 moveto -(tactics) -[6.72 10.56 10.56 6.72 6.72 10.56 9.36] -xshow -end grestore -end grestore - -% tactics -> cic_unification -newpath 247 911 moveto -246 902 245 893 244 884 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 247 883 moveto -242 874 lineto -241 884 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 247 883 moveto -242 874 lineto -241 884 lineto -closepath -stroke -end grestore - -% tactics -> whelp -newpath 216 918 moveto -187 903 147 881 143 874 curveto -122 837 114 808 143 778 curveto -159 762 318 775 339 770 curveto -348 768 357 764 365 760 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 367 763 moveto -374 755 lineto -364 757 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 367 763 moveto -374 755 lineto -364 757 lineto -closepath -stroke -end grestore - -% cic -gsave 10 dict begin -339 454 28 25 ellipse_path -stroke -gsave 10 dict begin -325 446 moveto -(cic) -[10.56 6.72 10.56] -xshow -end grestore -end grestore - -% grafite -> cic -newpath 128 911 moveto -112 874 86 800 86 736 curveto -86 736 86 736 86 636 curveto -86 556 150 554 219 516 curveto -258 495 274 502 310 480 curveto -310 480 311 480 311 479 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 313 482 moveto -319 473 lineto -309 476 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 313 482 moveto -319 473 lineto -309 476 lineto -closepath -stroke -end grestore - -% grafite_engine -gsave 10 dict begin -183 1024 84 25 ellipse_path -stroke -gsave 10 dict begin -113 1016 moveto -(grafite_engine) -[12 7.92 10.56 7.92 6.72 6.72 10.56 12 10.56 12 12 6.72 12 10.56] -xshow -end grestore -end grestore - -% grafite_engine -> tactics -newpath 193 998 moveto -200 986 210 975 219 965 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 221 968 moveto -226 958 lineto -216 963 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 221 968 moveto -226 958 lineto -216 963 lineto -closepath -stroke -end grestore - -% grafite_engine -> grafite -newpath 170 999 moveto -165 990 160 980 156 970 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 159 968 moveto -151 961 lineto -153 971 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 159 968 moveto -151 961 lineto -153 971 lineto -closepath -stroke -end grestore - -% urimanager -gsave 10 dict begin -355 366 70 25 ellipse_path -stroke -gsave 10 dict begin -299 358 moveto -(urimanager) -[12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92] -xshow -end grestore -end grestore - -% cic -> urimanager -newpath 344 429 moveto -345 420 347 411 348 402 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 351 402 moveto -350 392 lineto -345 401 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 351 402 moveto -350 392 lineto -345 401 lineto -closepath -stroke -end grestore - -% xml -gsave 10 dict begin -553 174 33 25 ellipse_path -stroke -gsave 10 dict begin -534 166 moveto -(xml) -[12 18.72 6.72] -xshow -end grestore -end grestore - -% cic -> xml -newpath 314 440 moveto -300 431 283 417 275 400 curveto -256 358 250 334 275 296 curveto -327 216 445 188 509 178 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 509 181 moveto -519 177 lineto -509 175 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 509 181 moveto -519 177 lineto -509 175 lineto -closepath -stroke -end grestore - -% cic_proof_checking -gsave 10 dict begin -339 542 110 25 ellipse_path -stroke -gsave 10 dict begin -243 534 moveto -(cic_proof_checking) -[10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12] -xshow -end grestore -end grestore - -% cic_proof_checking -> cic -newpath 339 516 moveto -339 508 339 499 339 490 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 343 490 moveto -339 480 lineto -336 490 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 343 490 moveto -339 480 lineto -336 490 lineto -closepath -stroke -end grestore - -% getter -gsave 10 dict begin -431 454 42 25 ellipse_path -stroke -gsave 10 dict begin -403 446 moveto -(getter) -[12 10.56 6.72 6.72 10.56 7.92] -xshow -end grestore -end grestore - -% cic_proof_checking -> getter -newpath 349 516 moveto -361 501 377 487 391 477 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 393 480 moveto -400 472 lineto -390 474 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 393 480 moveto -400 472 lineto -390 474 lineto -closepath -stroke -end grestore - -% getter -> urimanager -newpath 411 431 moveto -403 421 392 409 383 398 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 386 396 moveto -376 391 lineto -381 401 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 386 396 moveto -376 391 lineto -381 401 lineto -closepath -stroke -end grestore - -% registry -gsave 10 dict begin -679 262 52 25 ellipse_path -stroke -gsave 10 dict begin -641 254 moveto -(registry) -[7.92 10.56 12 6.72 9.36 6.72 7.92 12] -xshow -end grestore -end grestore - -% getter -> registry -newpath 432 428 moveto -436 392 448 327 489 296 curveto -501 287 604 291 617 288 curveto -622 287 627 285 631 284 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 633 287 moveto -641 280 lineto -630 280 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 633 287 moveto -641 280 lineto -630 280 lineto -closepath -stroke -end grestore - -% logger -gsave 10 dict begin -544 366 45 25 ellipse_path -stroke -gsave 10 dict begin -513 358 moveto -(logger) -[6.72 12 12 12 10.56 7.92] -xshow -end grestore -end grestore - -% getter -> logger -newpath 457 434 moveto -472 422 492 406 509 393 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 511 396 moveto -517 387 lineto -507 390 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 511 396 moveto -517 387 lineto -507 390 lineto -closepath -stroke -end grestore - -% metadata -gsave 10 dict begin -415 636 58 25 ellipse_path -stroke -gsave 10 dict begin -371 628 moveto -(metadata) -[18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] -xshow -end grestore -end grestore - -% metadata -> cic -newpath 436 612 moveto -456 586 479 546 459 516 curveto -438 483 414 498 379 480 curveto -376 478 374 477 371 475 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 372 472 moveto -362 469 lineto -368 477 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 372 472 moveto -362 469 lineto -368 477 lineto -closepath -stroke -end grestore - -% hmysql -gsave 10 dict begin -659 366 50 25 ellipse_path -stroke -gsave 10 dict begin -623 358 moveto -(hmysql) -[12 18.72 12 9.36 12 6.72] -xshow -end grestore -end grestore - -% metadata -> hmysql -newpath 470 626 moveto -531 616 569 623 617 568 curveto -658 521 662 446 661 402 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 665 402 moveto -661 392 lineto -658 402 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 665 402 moveto -661 392 lineto -658 402 lineto -closepath -stroke -end grestore - -% whelp -> metadata -newpath 407 711 moveto -409 699 410 685 411 672 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 414 672 moveto -412 662 lineto -408 672 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 414 672 moveto -412 662 lineto -408 672 lineto -closepath -stroke -end grestore - -% library -> metadata -newpath 311 715 moveto -330 701 356 681 377 664 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 379 667 moveto -385 658 lineto -375 661 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 379 667 moveto -385 658 lineto -375 661 lineto -closepath -stroke -end grestore - -% library -> cic_acic -newpath 283 710 moveto -283 698 283 685 283 672 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 287 672 moveto -283 662 lineto -280 672 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 287 672 moveto -283 662 lineto -280 672 lineto -closepath -stroke -end grestore - -% cic_acic -> cic_proof_checking -newpath 298 611 moveto -304 600 312 587 319 576 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 322 577 moveto -324 567 lineto -316 574 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 322 577 moveto -324 567 lineto -316 574 lineto -closepath -stroke -end grestore - -% extlib -gsave 10 dict begin -553 86 42 25 ellipse_path -stroke -gsave 10 dict begin -525 78 moveto -(extlib) -[10.56 12 6.72 6.72 6.72 12] -xshow -end grestore -end grestore - -% hgdome -gsave 10 dict begin -553 262 54 25 ellipse_path -stroke -gsave 10 dict begin -513 254 moveto -(hgdome) -[12 12 12 12 18.72 10.56] -xshow -end grestore -end grestore - -% hgdome -> xml -newpath 553 236 moveto -553 228 553 219 553 210 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 557 210 moveto -553 200 lineto -550 210 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 557 210 moveto -553 200 lineto -550 210 lineto -closepath -stroke -end grestore - -% hmysql -> registry -newpath 664 341 moveto -666 328 669 312 672 298 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 675 298 moveto -674 288 lineto -669 297 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 675 298 moveto -674 288 lineto -669 297 lineto -closepath -stroke -end grestore - -% registry -> xml -newpath 649 241 moveto -630 228 605 211 586 197 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 588 194 moveto -578 191 lineto -584 200 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 588 194 moveto -578 191 lineto -584 200 lineto -closepath -stroke -end grestore - -% xml -> extlib -newpath 553 148 moveto -553 140 553 131 553 122 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 557 122 moveto -553 112 lineto -550 122 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 557 122 moveto -553 112 lineto -550 122 lineto -closepath -stroke -end grestore - -% DependencyAnalyzer -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 641 768 moveto -505 768 lineto -505 704 lineto -641 704 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 641 768 moveto -505 768 lineto -505 704 lineto -641 704 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -513 742 moveto -(Dependency) -[17.28 10.56 12 10.56 12 12 10.56 12 10.56 12] -xshow -529 714 moveto -(Analyzer) -[17.28 12 10.56 6.72 12 10.56 10.56 7.92] -xshow -end grestore -end grestore - -% DependencyAnalyzer -> metadata -newpath 522 704 moveto -501 691 477 675 457 662 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 458 659 moveto -448 657 lineto -455 665 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 458 659 moveto -448 657 lineto -455 665 lineto -closepath -stroke -end grestore - -% Getter -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 566 560 moveto -490 560 lineto -490 524 lineto -566 524 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 566 560 moveto -490 560 lineto -490 524 lineto -566 524 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -498 534 moveto -(Getter) -[17.28 10.56 6.72 6.72 10.56 7.92] -xshow -end grestore -end grestore - -% Getter -> getter -newpath 508 524 moveto -494 512 477 496 463 483 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 465 480 moveto -455 476 lineto -460 485 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 465 480 moveto -455 476 lineto -460 485 lineto -closepath -stroke -end grestore - -% Matita -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 222 1226 moveto -144 1226 lineto -144 1190 lineto -222 1190 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 222 1226 moveto -144 1226 lineto -144 1190 lineto -222 1190 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -151 1200 moveto -(Matita) -[21.36 10.56 6.72 6.72 6.72 10.56] -xshow -end grestore -end grestore - -% Matita -> grafite_parser -newpath 222 1204 moveto -274 1197 367 1184 444 1162 curveto -453 1159 461 1156 470 1153 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 471 1156 moveto -479 1149 lineto -468 1150 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 471 1156 moveto -479 1149 lineto -468 1150 lineto -closepath -stroke -end grestore - -% Matita -> grafite_engine -newpath 183 1190 moveto -183 1160 183 1099 183 1060 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 187 1060 moveto -183 1050 lineto -180 1060 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 187 1060 moveto -183 1050 lineto -180 1060 lineto -closepath -stroke -end grestore - -% Matita -> hgdome -newpath 157 1190 moveto -118 1160 48 1097 48 1024 curveto -48 1024 48 1024 48 454 curveto -48 351 123 338 216 296 curveto -263 274 404 267 488 263 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 488 267 moveto -498 263 lineto -488 260 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 488 267 moveto -498 263 lineto -488 260 lineto -closepath -stroke -end grestore - -% ProofChecker -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 210 668 moveto -114 668 lineto -114 604 lineto -210 604 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 210 668 moveto -114 668 lineto -114 604 lineto -210 604 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -135 642 moveto -(Proof) -[13.44 7.92 12 12 7.92] -xshow -122 614 moveto -(Checker) -[16.08 12 10.56 10.56 12 10.56 7.92] -xshow -end grestore -end grestore - -% ProofChecker -> cic_proof_checking -newpath 210 607 moveto -212 606 214 605 216 604 curveto -237 592 261 580 282 569 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 283 572 moveto -291 565 lineto -280 566 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 283 572 moveto -291 565 lineto -280 566 lineto -closepath -stroke -end grestore - -% Uwobo -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 428 1042 moveto -342 1042 lineto -342 1006 lineto -428 1006 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 428 1042 moveto -342 1042 lineto -342 1006 lineto -428 1006 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -349 1016 moveto -(Uwobo) -[17.28 17.28 12 12 12] -xshow -end grestore -end grestore - -% Uwobo -> content_pres -newpath 414 1006 moveto -420 1003 426 1000 432 998 curveto -535 963 568 985 673 962 curveto -680 961 686 959 693 957 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 694 960 moveto -703 954 lineto -692 954 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 694 960 moveto -703 954 lineto -692 954 lineto -closepath -stroke -end grestore - -% Whelp -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 566 1226 moveto -486 1226 lineto -486 1190 lineto -566 1190 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 566 1226 moveto -486 1226 lineto -486 1190 lineto -566 1190 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -493 1200 moveto -(Whelp) -[22.56 12 10.56 6.72 12] -xshow -end grestore -end grestore - -% Whelp -> grafite_parser -newpath 526 1190 moveto -526 1182 526 1173 526 1164 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 530 1164 moveto -526 1154 lineto -523 1164 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 530 1164 moveto -526 1154 lineto -523 1164 lineto -closepath -stroke -end grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -end -restore -%%EOF diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 82f3256e6..192117af5 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -298,9 +298,9 @@ allow other developers to quickly understand our code and contribute. \section{Architecture} \label{architettura} -\begin{figure}[ht] +\begin{figure}[!ht] \begin{center} - \includegraphics[width=0.9\textwidth]{librariesCluster.ps} + \includegraphics[width=0.9\textwidth,height=0.8\textheight]{libraries-clusters} \caption{\MATITA{} components} \label{fig:libraries} \end{center} @@ -700,10 +700,9 @@ in its script based authoring interface. In the remaining part of the paper we focus on the user view of \MATITA{}. This section is devoted to the aspects of the tool that arise from the -document centric approach to the library. Sect.~\ref{authoring} describes +document centric approach to the library. Sect.~\ref{sec:authoring} describes the peculiarities of the authoring interface. - The library of \MATITA{} comprises mathematical concepts (theorems, axioms, definitions) and notation. The concepts are authored sequentially using scripts that are (ordered) sequences of procedural commands. @@ -712,7 +711,7 @@ The only relation implicitly kept between the notions are the logical, acyclic dependencies among them. This way the library forms a global (and distributed) hypertext. Several useful operations can be implemented on the library only, regardless of the scripts. Examples of such operations -implemented in \MATITA{} are: searching and browing (see Sect.~\ref{sec:index}); +implemented in \MATITA{} are: searching and browing (see Sect.~\ref{sec:indexing}); disambiguation of content level terms (see Sect.~\ref{sec:disambiguation}); automatic proof searching (see Sect.~\ref{sec:automation}). @@ -730,7 +729,7 @@ fully restored. To implement the proposed versioning system on top of a standard one it is necessary to implement \emph{invalidation} first. Invalidation is the operation that locates and removes from the library all the concepts -that depend on a given one. As described in Sect.~\ref{sec:...}, removing +that depend on a given one. As described in Sect.~\ref{sec:libmanagement} removing a concept from the library also involves deleting its metadata from the database. @@ -740,7 +739,7 @@ development, you are free to change and invalidate part of the library without branching. Invalidation is still necessary to avoid using a concept that is no longer valid. So far, in \MATITA{} we address only this non collaborative scenario -(see Sect.~\ref{sec:decompilazione}). Collaborative development and versioning +(see Sect.~\ref{sec:libmanagement}). Collaborative development and versioning is still under design. Scripts are not seen as constituents of the library. They are not published @@ -758,6 +757,7 @@ of \MATITA{} related to library management and exploitation. \subsection{Indexing and searching} +\label{sec:indexing} \subsection{Disambiguation} \label{sec:disambiguation} @@ -1127,6 +1127,7 @@ no risk of introducing dangling references since the \MATITA{} user interface inhibit undoing a step which is not the last executed. \subsection{Automation} +\label{sec:automation} \subsection{Naming convention} A minor but not entirely negligible aspect of \MATITA{} is that of @@ -1194,6 +1195,7 @@ expression and the suffix \verb+_to_Prop+. In the above example, \verb+eqb_to_Prop+ is accepted. \section{The authoring interface} +\label{sec:authoring} \begin{figure}[t] \begin{center}