From 86e145f723eb60663d47f2d06e1a28e5e782d2f0 Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 27 Aug 2018 14:39:34 +0200 Subject: [PATCH] - restructuring in IsaDOF : factoring out create_and_check_docitem - correction IsaDofApplication side_by_side figure commented in and works. - reaactivated open_monitor. - changing types of monitor traces : simpler calculation now, but more obscure type - first simulation of monitor trace construction. --- Isa_DOF.thy | 73 +++++++++++++--------- examples/math_exam/FormSheet.pdf | Bin 47217 -> 51088 bytes examples/scholarly/IsaDofApplications.thy | 14 ++--- test/conceptual/Attributes.thy | 26 +++++++- 4 files changed, 75 insertions(+), 38 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 8f27b370..a8137b07 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -442,7 +442,7 @@ type meta_args_t = (((string * Position.T) * (string * Position.T) option) * ((string * Position.T) * string) list) -fun meta_args_2_string thy (((lab, _), cid_opt), attr_list) = +fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) = (* for the moment naive, i.e. without textual normalization of attribute names and adapted term printing *) let val l = "label = "^ (enclose "{" "}" lab) @@ -526,10 +526,8 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) val generalize_term = Term.map_types (generalize_typ 0) fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t fun instantiate_term S t = Term_Subst.map_types_same (Term_Subst.instantiateT S) (t) - val _ = (SPY5:=thy) fun read_assn (lhs, _:Position.T, opr, rhs) term = - let val _ = (SPY6:=lhs) - val info_opt = DOF_core.get_attribute_info cid_long + let val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy val (ln,lnt,lnu,lnut) = case info_opt of NONE => error ("unknown attribute >" @@ -572,42 +570,48 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) end in Sign.certify_term thy (fold read_assn S term) end + + +fun create_and_check_docitem oid pos cid_pos doc_attrs thy = + let val id = serial (); + val _ = Position.report pos (docref_markup true oid id pos); + (* creates a markup label for this position and reports it to the PIDE framework; + this label is used as jump-target for point-and-click feature. *) + val cid_long = check_classref cid_pos thy + val defaults_init = base_default_term cid_long thy + fun conv (na, _(*ty*), term) = (Binding.name_of na, Binding.pos_of na, "=", term); + val S = map conv (DOF_core.get_attribute_defaults cid_long thy); + val (defaults, _(*ty*), _) = calc_update_term thy cid_long S defaults_init; + fun markup2string x = XML.content_of (YXML.parse_body x) + fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) + val assns' = map conv_attrs doc_attrs + val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults + in thy |> DOF_core.define_object_global (oid, {pos = pos, + thy_name = Context.theory_name thy, + value = value_term, + id = id, + cid = cid_long}) + end + + fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta_args_t, xstring_opt:(xstring * Position.T) option), toks:Input.source) : Toplevel.transition -> Toplevel.transition = let - val id = serial (); - val _ = Position.report pos (docref_markup true oid id pos); - (* creates a markup label for this position and reports it to the PIDE framework; - this label is used as jump-target for point-and-click feature. *) - fun enrich_trans thy = - let val cid_long = check_classref cid_pos thy - val defaults_init = base_default_term cid_long thy - fun conv (na, _(*ty*), term) = (Binding.name_of na, Binding.pos_of na, "=", term); - val S = map conv (DOF_core.get_attribute_defaults cid_long thy); - val (defaults, _(*ty*), _) = calc_update_term thy cid_long S defaults_init; - fun markup2string x = XML.content_of (YXML.parse_body x) - fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) - val assns' = map conv_attrs doc_attrs - (* NEW : *) - val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults - (* OLD : - val value_term = (fold convert assns defaults) |> (infer_type thy) *) - in thy |> DOF_core.define_object_global (oid, {pos = pos, - thy_name = Context.theory_name thy, - value = value_term, - id = id, - cid = cid_long}) - end fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy) (* as side-effect, generates markup *) in - Toplevel.theory(enrich_trans #> check_text) + Toplevel.theory(create_and_check_docitem oid pos cid_pos doc_attrs #> check_text) (* Thanks Frederic Tuong! ! ! *) end; + +fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) = + Toplevel.theory(create_and_check_docitem oid pos cid_pos doc_attrs) + + fun update_instance_command (((oid:string,pos),cid_pos), doc_attrs: (((string*Position.T)*string)*string)list) : Toplevel.transition -> Toplevel.transition = @@ -693,12 +697,17 @@ val _ = "declare document reference" (attributes >> (fn (((oid,pos),cid),doc_attrs) => (Toplevel.theory (DOF_core.declare_object_global oid)))); - +(* val _ = Outer_Syntax.command @{command_keyword "open_monitor*"} "open a document reference monitor" (attributes >> (fn (((oid,pos),cid),doc_attrs) => (Toplevel.theory (DOF_core.declare_object_global oid)))); +*) +val _ = + Outer_Syntax.command @{command_keyword "open_monitor*"} + "open a document reference monitor" + (attributes >> open_monitor_command); val _ = Outer_Syntax.command @{command_keyword "close_monitor*"} @@ -1032,7 +1041,11 @@ doc_class side_by_side_figure = figure + anchor2 :: "string" caption2 :: "string" -(* dito the future monitor: figure - block *) +doc_class figure_group = + trace :: "doc_class rexp list" <= "[]" + anchor :: "string" + caption :: "string" + where "\figure\\<^sup>+" (* dito the future table *) diff --git a/examples/math_exam/FormSheet.pdf b/examples/math_exam/FormSheet.pdf index 7cdcfca01cb32cedaaa798bce23f805a9a6ab8d9..300e888d639410f75a4f32bd599c4a5e16f4464e 100644 GIT binary patch delta 14918 zcmaib2RN4B|9?nilT9|s$g?~Hk-hiI3Ym|rkd-{Lw|ML=WRL8Xy;oKuvPVK>lkum| z_%7moulIRg=leG1s|c)8;p^q{*9|ey^4Dp~hp^Q#$^kfx z7-#?vTe%l5+0O>L?dB1-skw!zIhv4w6MY^30!>0NQ*KT67y|= z@c5)1f#_Lkit--Xd<;Us6^)5c-0|`~80|$*g#kh9P-LMb!-t8y0R)n>$H6~xiNyqO zgldN|KCoWE@fxKz_dZ2E7KFT+bgoZ6n8C)Pe5Lh8F8_ATz2}VEjq|}&`J=tm+V;iI z`jsuAQ7F^vF^U;DJ>!t^$1_>qz&0X=$K3-`hGqBHh3TyHBId#zTc|E@2U$qQJcqAQ z#zvyc3Z93u-;^FkvN({0S$eTJ-xiSJ;v(%}Cau3alT#BQ^ptX+LD&WfdyHyYQ-G3M4z*6REB8C~C_pp4o4} zLg{%(O7QZvkh>zD8;cev?Lt9;zHxNl1PkUBU%#Hw;Es{gAXBK2Qnqka`{adDg%RDz z9#TPMEJfvQJ_6998mqohM2@#VVNdepbPH0$LSIUJbDdE8vxqvLnXRd#lY^PD%~i|p zu@xRa{BoSG8bBBVtxEg9+yyg1q2))nj4;rSB)7`H5maMfz{=kc4P4!vNLv2qP?tZT ziosz1B?o@ygRn4@u<$>+p+IyYJtO*ro)80c*}6yZk1aw%OneGvwiZs7Oi)BQ{cV3d zWyIfRf}lXqzx}V|U)iq5#3w5*E@td#X37M;5~9Xr@DCI0AEy5Zg#pXI-zm9{0Yqo; zkaK|lhm@ba{v!nnL#y7SKyUL9pp869n8Z}&6xGzY#TC`nfdD2xDLY#y2{T6%2c*4| zodXjLgns2&gn4;Wy~lmyFJ81g>a{lPN|oAwBJh)N<-vcAgZyOrI{-i?82^8tK};~{ zf1kljFjzU#i-J)UcGd4n77PIZ|Lgr#=byt1fg}DUUP-tjLg7%rzeE_iDNW{vs)VMF zrZSo^oemQQM{}jSU)`?U`1{4jbfg{>4q@U`cQUilx|GBBP{s^tVd;d&4+JyuDH^+K zBTX;I4ag7pJ1|m6YqLwMuLkfJ*Z&#O|F{kZper)qs9RmN7v_vn*2b(o#IjY(F%RX- zc#m&7^VpZZVmC3_pzarEfy-2xS>sR{+9$^|8e3P+u zg5;_Y`EZ-)S?8ub1=0-0wE)ubf|S(T%{A5((uwC!R@9n&Dn_58e~29_9ujY*Tc7LZ z^3fl@ZwQ2xpmxV!B99SSgXg^SNYp~tISTuFC5k}khO9k|^Cc$X8|by=G_+#wowC~o zj|`(y%8YII&4wON99dhsOS~zu)413~Z)?_{sD8-Fl}Y>_m;2f%|C$kz=#Q+EVPDDO z0PI^nTG9lxfR9GS%^UVSz-9n~V7Bv=z?{~-+m^bu0e|;ae8P1X^6aN&g1x!Z7TqMK zk!C1c{~9viPL$NN`X5AN76JvU;XN@v*V zX&Lrb)F)At&S2aHnCsrViJ%?eT^%I7^N_~-nf0r_SEJKuy}>oay^qO*99B1hH+n*9 zIcrxPZoSE=O^b&*tO6J#lENv{yO7^=>Y(2Nzb(JEj@dky!j>cZL40t!zNzjYMeJErUt91O^G>NETi!U6Pkp=+ z>cu@4hJnXC2&q(Gu^rQ~x==wM9wL{DjC3nhsK<*6;ii6C)~V^3{o^0_UpL3Smy;_| z>4Ub?o&)b=h`F{j?y1Id-|qFuRz#|rbB}5Y#7M>DCuYiN*~Hi$o~DI(M@ty)l!1%JN60~f?%8{C<6Yv4qfe(!;s)~>x8?v4Ns{9WhZ7QzEXuJ zV2ahY2fk?ztvB{R789^1PHbfe$b7my^u-8e7suEC!@Gem6v4T{umQzw+ce+JoAK;1 zqO{a2eV3{CI-_*xeZV_0zAgSV+UWJqM&F|PeHsqQosPARm7mqN&3s9JKGYS^@Derb z{64ly=f$SnUS-EF;)PpQXO+y0%D#QuF9nLAYWWwHvOjOvxKF9L1DI?9zhany|M}|Bj(^jxY+p0}#6Pf*`i-f=tze zqHYec$LO_NO03jEUpR_GV|kld>nUBY?b6h|=y#oNAFd;ghHLk%pIztZ$Xwvm)o!(d z-{^XK&WEd<@_3|uwc}6}o4a%XXLu*SMqlWrfW0@4uF4OlWLB*co40fXrMRff=Xi}+ z0dtZ^+-_c>L7x}WT~$4(;_@*Z(kVurK~gi>%Ai^DG_ng8C1$c?mB4p5jQKpMrbL2} znAKX0wMhi8-kCBkzhOx4j87@_{7So^a!nriq0QVCmy|jHf1CIyTK_dcg+D_&ibE^# z;yOQMfipYO*O+9q8W1)YKS+kczRO;jE+Mz1r$iSYvd*C^L zc}!5*^9d}x{V}ueg-20G0$*CLyR=eHyv!6NrkZE15wo=B4tUtZvcT+OOv|CHwzxz> zlcU>xy;kNnYtx;rNckmjaQ2D{O|%bf`hi+k-tHK;6Y;wUPw(^lFA{Y6QED5^2UvcZ z$5VL+c?Rkwfg$ZK9m@70nlG^}IyF~s1XJRe@0ZB|Wgb|SOb#5^T<6g&Ey4Tod? zmIOv%xM`%rh;LrPv}m0Sv0Gwti<46LvI*WDZ@JeM(W$)|x_Qp|5wvd}<@m2z*S&fq zRg$Uv_ylow>V00uIHD1BJW#-vYH_>4YuJ^xf?(+8e7or2r z1HulXjzE_Dnye$#G-Vt&jQenIqapOkfuw%lg(r1Xz;ImK$8;Z8S;392Nw|a1 zvJ7GkC(MS{nJz=}d20HEt8?o$y2P!{6OttX;tO_POtv|SqZKEX03N8c?_NP?e90*| z>EznOP7YM$luJ`K<3gUP9ie)jO3tyv>F@hxlt+>LcOA!iWVy1v%`AhxM!P;@4|wx( z0-%kJjWSWkBwS)2?|L6`CHd7&3VZA1Q;Ci8D8t;HKhLd&Kd-x$Dq&LW|CJ?YvMb5Y z(A~{3v`}we`rMe05rB_EgJ#)wXJe1amv|`)jSgt)-kHC=J|LW7TPnDK?;etDIvr-u zMuo@@Ya_JEGsdtIpL*)!r`ywZ$MpN7G^3?RX*!#IKLNj33ePmy)Z?4!M4H@Z6Vj38 z(#>$=!(^pKN0)xWP0=9yqCR4Gc^Sw$L6_o)VJkC<9`EKXUKkYsJ6$qPmOC*qF+MO7s>Jkr;$MYVSjo&rP(A27ycvc= zwXrXS4%OL_?!NWl!bqZ=!~*Y(zX9Pu(=;yXxl>ZkpMeZ(&95bhQce8Qu1hLo>CYG~ z9IHkDtor3v?23y@s(Q4W&z1moFBwFwUrfNWS?`pxh5iBdIV#Bs+R2pHfeL;V`5-h< z&}5E3Y!Rj5-ezFwEGJ*o6>^rTvLqpyfnEDJrF?u{0@i-jfB-Q_H#a3S-RP&7` zt~4flpiu$iQ*X_QOu<(vMr|*f#jJBAtZ)j_pR;-K?kQD!X=ughi|44_@l-(Sg`oTl zsSnKYZSAgEV4&i*Bti`1n`7v3)3tS2)IwdKM;HsNIE2;~l5FlS7R{mJjICKnf@Ex} zPTWEOq(P?AS%gu+~AD3*^D_cgCZc`F)Ga1)ii`(lDZoSwr z47WF9u`P6?lhV7(s{bs6#Q8HpE504xykwA!1+#t_kPj6_(s))N?)sg__emqYu?veW zfx}Iy^;pt_X%^onb~lW-6qz^VB?R#21wtq9FgNTKh}U>hwh|hKZ>v#NcAlQ@(JiJ3ji6|$#661eIvBEwei)s##^G0)7$`8$%@=VIe5 z3kW#;{tw#Jn#5_MY}rWb*FDot+UCJxan`7@^>Q`!3T*cjH5e>LK3lEi4IN=;L2Q`d zLR;Z&H=j_}jr`ZL&^1cZ^rVv?r z(plklLZ9iLjS!&xTph8`^H5p!y{hT{E~~cST8>nB`>K`)T6h4mfUNf=uV>7Y6KF<# z`*=UnlWFlm28+mhtCET_o!AxL%90+vCtJN!mUM~WXi&63H}MkTLmcY>#|ZeSrHVzV zq{35LQ!~?bM*q}xWQ`$xeqFGoNuE| zpZY8K7&O6W-&Cwx#AG`-4?HfVqLc4Ky^d|O8ATrt^HU94jPl3bKokuwJH!~}J*y=N z>XAJ~K6C$w>fWtSCReQ@coI7h)vLpFv*a!AW;@m$y})GIfVvGQAHVq3!E!INM^?eT zsn*QUCu*R(k9k~Of+UNfU1FgL59bE5+A{LSHM;Qi8AgeVBcUU)v3U`E1B7PnL?Jv~S*p%E&7vGF&sA_Jv-)ysQ;%`7(sZtR@uH?aR-p3}rO5Dy z#Xh^n!-kyIqFDoXSy@jB-SL=WgXcMXe528@lG6EeED;8sk1w7dkC?j{WB>;=7WVF+ zcXw2$W(cRag>(RBa6D#wlCI6%eFABwos`*j7I#1V9!2Sb@o?VY_QMwenZgZ7fY8t= zso0BYE;nkxs&VYM%y$cWK0<7+-p_liYu9hM6|i04-w{GYUlok&`f?yI0|o{ht#Xg&AL_?+C-lL+yJT?CZ$%^=4dlCZ$t%gH zg(4H96lX~k!_0eNJb~qpJ7H9s5$Q!kK>#VP_)O#t<->T3*((tyokBxFW$ltgI=p5g zm4jo?s=3=FCxfQn2dvtAz%J@99OAY-4;z1c{ajI`v+iU6lIh10d^NqHE5_3*&lP1gI&Nn2&6q%RJ6x&T`eSwZ5iIa~Za$zo(iy zD;91{m!l&5)=YA$&Unf`dgpGRHZOgU^j+r#ysf&(^Lf@XUha3?9&O9F$S>N*HLI(_ zCgh%X6g}}^U4Hv=`yGbNjC~F9*ky@e^guc<^3{txS>P`qqkbABq$B9y`wHe zQE6Q4mR`h`UYrlQ+~wbR^!>R*E?=CsgQhMM;e!xzMuK`52wA>#wY|ug;F*f3npl+d zf|C+V3`dyg@Rg8UYb)6_#=2}3`ZU#-?n5e50kO-T!)qt{kK#guQLXS@!eNeb)m!GC zeG&PY#7VO-PiIU;NGsU#D+L{o?>(6+EawP4r zi*D^d_S15FG@|2Zo^L2o29C<_N0%9bm9v61`o+RNvA;tAk#WZYcZ1K+Cn=SBun|*zB5$=yx)mI;#=wOQkfolV3m0@CsLTsvEvdO->V!4Vu~1ZW*6A zATtRvPHfEW-*>Ejqq4N~`FJ;u6utDV_vFU0QIzzcYP3<*s>9Povt^6js!H;m7=e_S zXX_Ca)%OfG4ko7+q16#tvNOXokD~<>d1F(vi{zSF%I_);;Oj+CucP&BgyR~CzInMcl z|FX+^f$B{d_X~cmpFjD5jK=7e`na*UnNLy$qYIDJkde3d9Xd8@3DGbx3uRXmL0xn3 z+(oH6Qtb!1F(!M*5V1=e+73*O8lCBT$(TPU0-*M|McKxf=RwzS?NFT9GH(zsFvF7S zlMh{Ytc;yMZ;ME?1gGz8i=&D}k#mdDcF-JY@OTS795*2MyeTtmZT_`4iYOJE)LcDD zk8{Vol*^Tx;1yA}iu??(J=x|4P75WVRYUBMNeJ`DyxS4pR(obktkLsrl*TpzuO=&- z*!}DN>sd>h)t2LzQ0Wk{+0#XiqZ;abxZ_4 z0Vy$3MG47K=v^Q9QkdGSsqOHH-^BEpHQf(20N+s)$&DC@oEe+2Wllwy8dccZ^?U%n zg%Pi9`)5~?#sP)LD*(cNluf_D3cX(2pvlK_JI88=cc)68C0soA%&sg)4%?7+QL<@* zCq}ozzG1_$SLbm|^NJ)Y7BzS}j-v&(G2Rd#nlP$|oVf-g0@D^Oj`+{Jw?kutjFT1U z%0m$C4b2UM_l&nJQ13l^AI-h_PSBKgp>IYdOaQ^D!g)ljM3{Qh6D6%zh^v*DpqBd* zdoFvps+GLPN9sFyb{pgg);3uKtz4Qh3qh+(J7zk@A`qwG?uWVk8tS;YHrM2l9+KD) z0>$f@=6eeC=CFu`XG+1i`wD9m2L=by2h!oIuWP7_lMB33rtxeU zv%6}s^!W~N7`7`fK0zJP9TRy9HlYo=n|hiGK4pDX+s|**dLcgbIHpu?LbiODt7vi+ z$$PQ5V9%2A{$)%liNOTHX9(SoVf>VeI?8#2c5QCBci09;RdUbk5B6lXIUnkXp{>r& z3>(CaT@1cWLvlJwiq6eV_Svu6w=yPcZ?;NXyk5I)7v@L znxVs-g5Nq*0*fRmFnJKV%0Xl+K-HEl;B7%6|e8EvJ5cvUg4139enair$pL3 zF}i9`2{E`5wFvdFJq>WvaolQP;RGLmN=nKVViTQ7YJ*XeSr2DYOf|>#a&^oLazs0e zSeeK}%N$MG_=AkZX;eI3-SvM-4kAXlcz=d z!mx8MbWKk9gVi)78TEb2_(JbY&UPBIt=-GLE_L&PABGb%w((h1hDV z*h0`f;t>EUjwF=^B>u#|vajJ?E4Ry-q5tp#?TwEWV;>5j9RZKTvKhE$$MWjK&4YW_ ztz!rA_o{5m2tE177jJ*h-KfJ)zaA6BV89J>=Ud&)h>C4 zj*L_am(?2K$kFS~T?LsHJrv+gp$HM+HH)RxRY<-ct={}`t%vQ#I$hwMnwRd;LN_z> z-!ImNf9lcrl)_$_+{W+&?zRm;7U2y`c zN38xK#s2f_#liD=nKE4feTDcOE`p2ElCJFvAOR}w6x24tX^V+S8Ioi6moFi00~h-n zf7AqSFh~mc&x2Yww5ac0>{F*A{O5xW&0WVYd39thE&Qm9>!b*@4GG)$wL7-=e@d2* zFVUt>JzEFr!~Ew@49$=HRj02z5M{h$Zr=|37&xDFX@`Ho;|XxE6G5Bf&2nkuBh-qj zfA)2n;^_dvPMdoB0oaP0wu(|yv@2FLNOEu9gQQMI-Zt<5LDl;9g$}R;ounY14zIr4Q*e>R&%mB3chF(zBJUD@G(&Ip>Dh?$~B8O3s}xnlNG(bV|b!`Udw2HRQr{2P2Xo?9k1V_ z;S?F@kBkz~EeQ_}3klIqYsLwxwDeF3ewFT1Fp}{2aZ}~J67Y#%a*>k7z%lA;%TdH4 z&MZyg(;xb)=~--o_%x!~A3HjvCOJ&3NBE|3uCX>4s~vTnK9bT-eRDoOsb;Ds zP7mnvWgBl#fRs^ghq^1`Q=X0ezR%8fySPia7Hsm;7yHP6g>P%_zL!CZJh6^ zh$+$-U+UZjm6gBVDRkF018Tif6d{gaXw7_?FYdZ=P54$WoFv|_OYE$_MLAy1oVe&o zNY+aQ%0)N8QzwwNd%Jrw+rsHP~a-TAqlPhK~nf!Ph;)}&o_L4Oo9YNya7>+z|*?Rw}E8LNU8^RR?P zVFLo>AQsKR7hE0xQ5SZ{vd9J3?`;8xM3$5-lu9Z7p{=@o1K8D5#l?7=Cz?c^-N#*A zl|zwfz%()=S4J6T**}>0_7R%rJ`>8n(?k5`3f0o8qU>A6^bh8&pA$_2gD5p3b6IdA z`Jb%so+agsJ+s^3R-R8amjC#AalvA}FLh={zlJk4tR{Lqz<*pb#%;e3`t6fW?Y_j1 zyylLs)M=G(1-NT_+dc0E;_Iic5YC8}=qH`SM#i=x;KL^Glkch=H;MMKgy!$6_PD znwL>6QKBr%r$dO(=}Pm`^BfYgp60Q4vBx~*qF#sv<2}T&FN~LTV*Auj6j)7nyF257 zli3LGWa5M5?4hu32LXyQr;gw%lpFY|e;7SFj*gBhDG98QEY~gHIi1XHnf!W4CWow@ z$%cH`sBPkX+6RH&)HU~=wX++~H6F_q+MOi6Ys~yc-l(k`1Z4D7PkmH%65c%9B;Qe^ z?HpY=Q*Y}cxWLL|a<{=kXR2<5Frun)=kaW8-87q{a@UiW*M{Zl0cUnTeW)cyHeUJ_ z*;`|wQUuce2&78hbt%6FrV*XkbmMXV?}p{NFHO#<4W?jWxMl&P1HST)+F=|7v;$xmsLiC5$Vv{X%omeIF8i`Ls8a!=mv?QXE40CQ8 z;nwhTMfb|!3dE4f!$XK2S+HZ6(k&aK&acesmL`CakrD>_$#=LjQnz6brYK9Sjj$$l zN_E4aC*tP(?u_{Q1Rg)6^_xXpkRqe^E20fZS|zu%4hZ68pGOh8Lr{-{3VSy(G=utA zUKb8Tx6NjkYlh7XwFOE_>P)KE-lT?&Sni+0dd3tzey^^Ofk=F2`|$*TtG9rhlVmdFq% z>JOwmi`HH6r1LobH>X)os~nS4fP;e!7OSD zE`A`zs3@+YC82PMAyE4t5CS;l5<H9sZ% zq{0yY?&16t^OFeX2mcGrfdBLFK0gG29;T;5t9X*2PkCZ#@I*9NOTp_J&PIn$Z&cO7uh?% zS1>Tc=4dVK#+VRbaI|{q}NuX-4sNOeB?6Q z`~o-$2_7p&I(9{WcDlLT-Z=L{eYb6$b2p9f!0++-TA0l432YV&U|(f=wr_V+@%R?w z;Kd~(3WVC`WNWr~fKN_cT8J~$h_)2Hue$kVr*~mviLl&?&qp&qRurCtjXO)ar@?!HoxOv9!N-K>&g8kV!lp(>zqJMU7@&LNY@2{X2U0#Nj(Nvk9|8 z;vnF2yI1`(AT}N)wpo^0U!}Qjmu9IdQPw52IP0LI{x!w6p@?U=+(lKs1kw(DHRbKt zP=6yv!6nd=&bN|mziGW})nJJl$8b)cB|rV>cAe>(<(uDdV#B6&3cF0+m?-VJ#?n<; zFC3s&rFt@O4|Cb&O5d{r9ZIn4h5Pmq#11Lh`7b70IG+i%YG%F&%U$IvDAe~`Cez*s z{EFM_7i%^>Jz{9@HbMH?m41wawwAun(-tGqf%j1tW}!tl(1Cg-s*Q9??Hi=5W;&9? z;zJAP@u`f7XCALyRZvXWF-}StQIaE#g(DONr|&K~4sy;pxVQP(CZXy$;(r9vJSO%@i4sNjniE{LrEp z1?B~5!CZxlZ|26XRn0B(f#1sDBu#mY07DG9)Tt*I(wt$+U`BbIZ<6ZW1}Z}h4(r`l z7y}raE0#CRm!D~qW&8d0e=MuA}5l6ivaic@Dgkt%}yE2w_Gi&$UT0-Cj8}4qDNK3{TsG3J;BEA ztM^2rl$5OaKZ8Jr`L|0C^^I*&ORu#`FySZT4i4ZO9Jl*d8Wy zgGz>PW@_Dt{1JPt%5`zqS!rXM)8y_Q`5|oOjEif@K3Mj6QKia^SsBk5-}X$YP)6DX zr0k$y;b?A~xiaKG9eV*_ChlXkG`LwXPfg!-F2aiWEI5Hzgw+u9c40Hn<@GYVTY?9f z!W<^7;o#VCJOfjvL$wg6Vf1Wsk(EEaWm{QFXcX)V zx<78YYq_Zh9Vj8(-=Tw5%GemTnAQ#okI>>fCZJ*Z(SsqE#gHzQU|`+3^sK$*rhF-+ z^(Vx@XLppW7Q`GRh5D6~LBi_BY;hxqYiz!L#+NEXU>46Rj`;t@vA z)bx5qt>7->KH{tJR~vW4yYLygi{RRTpwj1)U67NWz8#w5t{v`I7?d^mRn0{DpAj{< zTWu6#iw_a)QdWUU(_vMzDf_VM^7EJhvIviEdP*kaR$N=CHT3JCi8%}3%<>8e;2oo^b1i9>Z`#K7h%Pjk7e6#w%w?vQxsB_3co$5L{x28%th=aXOs%VXn4NgIes|cew=29m`Cc z8Ka!By4KZwQ@tY3u?(wh;#E$keHrRI8?s-?1r8-7Er~hx?NgLr`*;T7ahlNJXA!ip znpr>ZJB@@7xE-QqjG{U9!~x{CuiBd#u4|KG1(Q#Qs5#O_w5ipf3I}Z@;)w;lrDD}= z4LiFtf%&c>nyJR`o4wt&7QdKAnb`PjVGnl8eMwM9Wuej)f&+!dWx zGo+cQGc|>aof@$L!NCg}B%T_phqj-u$vrz#mnnMG7{t98hC(>eei7?nF z^Ly@JC0kf@my@tkF<^Kz2%GB5z62Sld`yJ7n(++FxDB(P{Dkhhum{aW5msw^J($1c zZdj*z4MDJ~tdmEH3>$oam|vI&t|v*+W~F8@ixLOTwwuilg7)QAw8;?Fz)udlH}x6*gKpwRvnEp*Pm1+ zVig#5l%C?f*|nEf-s1GIxG?qQUVLiu{+QY(JJ|k%jabcz7Re)fdEAfftSK+;c{}wp znHsi7QR1${1itISG{!&%*o|81ObSik&($~QPxM459OZGJFGdbNsKGEf;KJoQ-XpP1 zerZ2?hqVE6$vYW3d{2|~k#iD>Z7qdw+$`DUZuXUA?oN*Y@9kh^;`tabiR}+lU+s>? zP9|-WiUJMakJB8!TMZPxFRFb@MHtoyd_STd_j_W`*Dv6POp;9>(KFPoy~VFSYiam) zqx-vJ5dX`hTAch`t8URc63tNygzS-@u~_Y`ro8P@TEjS`_4kdNslH8UpZw0SE-=-1 zz3@(O#>oUCtQd|*pq0XmXHQzd!m8X9E~Lh*MvH7+x2JuMQFs>~W>PLAFV`2Qm5GHa zNSdU2cR+P;%)PJrW|_OYOw_O^&s`#bCAR`_&Zi^aNP5ux{ff$wZ2)qgon0A=~c@o+43qd)c_Hb%C~hD zS)K*)W`nXa*TwqX1=*I2uo9wgla)V1IjgC7HT~FXVjNEz>FeX-UYYbmBtp7n-UDLk z{DR3@`dd1A{?jYEfaRK?3wR zgxgO(L#;U5JP}-?1N#=pyLxi+b+@DP;}gQZcg*jnRI~%06ci;L?Monoke+64I_^@s zr2aXw+{(8?A9D3_H}Z{z(e8pAK>OUs-Ihzu7~}WtZcE;mjQsF^qkddgq;U(`p5*U` z=HC-M>Sz;X_S6x%Q>F0+x|T?W@(@6^ip#c5D(m^*md5Wa+kYLdl(wjVNP~B^B5A@# zqY^C3*ao>qC@J0|oK)RaGtdKEvT{$^_{szwKq2zBGMzteeTXMk=rYU9tD|m9Qz?HO z{{R?E8TTqJrU14wN#M-<(Kg_e$2#`m3K^gy%fUT|YB9n9j?r4h zWClL$jONjdrcb3^c;diQHZ6ZiSP023$1ZD_3mmHQppHi4K`d z$(eR^g$J(|mbw<9I-*XzJBQx13_VbmR@qk>n23M7Vyrp%^8U`4pHRD-_u;le?K+2B zCd&me*pw&X&!YEdA$C=qfx!qko*C|6#}5!-^t%$s<T(k#@Ec#!hBTh`+(|igu>|eg3~n+10_! z91p;RfT9aa>8Rld;ANqDburm8;r(m?z(4>1JzMIC4MG4e&C`C%j=D7EcPJ!_=5)g9~ywr%ZmTEzCaM*()3^D0T6%bK>v8lf`a~GC=dv`Ea`vk!VkXM3iyo% zC3_$%M5DMl0 zV@RNvuKcd}GJ=0(1qcZGBQjtR;7=OlYR~2BLj5N}`F{<~)oTz0`lk{I_)mdQ;2)_B zMnM1Y_;QZ^O1p|b2zGT^=<51EV?Z#_ABrIW#2-kct2n6!0l1s^80RJCz1AMs{ zpng{j;r}!I5X7ZvzZnQYfPSZ4PVhg+7zP6TVKfZH|4#%_|Ev!{;Gc;E0wWN=M*#wX z|B;wL1OoDV1TW?NIdfo_F8}HX3UF!lA4|?9?T;yTxhz~QjaS#d!vq9E|5(C+Ksfjh zV-RrY?}-k)1PVf#e$K!D2t*+MNWx3+K)(yTT*vbBIkWkH&;Co=<<94?QGmeV;LBX#`z17&MA&~iJ2@C%93;bcgrc{rnT_Bupeex27-3=zh4TYV5vCw0#1wJ)(c?!zFX=F0JfZ(D%U_$Y Yj!wo7PCvh$mvamVz+-2ZRF=Z~f44oE!T2$(27#25qr0`EyBmOuyGrDS`St$=&>}bJ z(RXkOt2(gcuH*kFiALdbqWN)tT!N~Uac^D`3&uNQHsbQ;1sQSkoPV2u`N7`&5F>7G zfWUtStIiEx(&R!95Y$)UQPy6+4y@_>nLg4PdfdL~~2B4<(n`Nwhrr{In<{G0ar-kf@SijF#f-$)Z}z z&*vkt5s!NHw`(g0&0UMeIO249hP3fx@7#ZVuw76^M{IUaLL>#ByTr_|;QcqYnwXc7 zPCM1?LDC9;5nELCdixF};=6LMfwCg~n;Yp78(Wdxv zB6&zd(%n#~&b^5b*k!ud`x6yphbJS@I>4<8HHHV?m|rA>1M#gLt=!yQt<4=SMotzF z@L_`I^LjA=Az)}Axdi(kP4Z8B00d;udmaCx7qqp{=O120O5Ak0Am{x=`MaM0Vq(7? zz@cbf1}3x@1IcyR`G^m#&qs)-Z0&f@{XPILSe3~TjxY2(1~421{#WlJkc+?!0RjqA zQj+Fw)>Z&G;#Wk*{|ce=)yOdrz$$0X@*CHIXaFAt2l)TeLtfH5pH@{$v=bj8nnaZx zTSr@7Lq#8LR8EhB_&a}e1s^9`!ej>n0XmoD{VhRU;f|g%<;F%_IMGC_@YCS_lL`XO zWu}WtyhDX~U4=PFI}f;VU5ahetRg?*AuRF%e)(T@pg8iyjk z?tz|;W7Z`+KQ?7AP>A(Sa}#XIJext)4|uiueGb@nH2CmhUqaCR8o_I~X8tH@%+grVkPyK7DqxcztjpbQ>$7n_5C3 zd;^8`?o4E<6}HjZx@)XT)Tnoo!?4D?oNSa#C677E(v8!xdFxT=+FSl<5)V~zWlnD9 zK2{f@V!C`xrig5|xWtNz8?{oxeelH3XlK@s0&*%T5*f{U>BOGFnc8&x#*xYxtvXPzBMR-S9Lbp`2?AkQ+hCinv1FO5FPgJRd+aw&$<+JBsd%{`f|5+yv^24c%W7a{xsgNsin}mN@-r@ z90k9Y|@C0-_9N>B+e4ZmOxAggrjhY=aGe50(_{2h!U)s{V`%sh6@;>ROv}vKD zrCm}>hU9+F-n+ce%%m2&U!RPEB6ZXLxf!K3MJKz$ceXA9CDpyLLO$OI>-W+0RxGHI zR>Fq1$8%>DXj{!66y_N0-J>LjZJ5q9+RhK%aRwurw|Q}xlT&pvmH6{ET|1N_xnDAjADMrj`eVp?Uy8g_@KC#Wn>SbJ=XN)B=`zpuJKK-u z$Q};|Bb`Z!HBM1-^y8f}SZ53(I4pyx0ysizX~;}x8%P7VrI?@6lsV7#af&2($Skxk zbW_6n#zE)qHsx%XT*y#+&D`pozQJ=@`A{K6`faWpYZA9s0x_BsL*N}{K{Jf~kGPF< zpa*Bb!oZIPGj)W9F4VIl@`J{M8jb`^)HH02V|iJcSTBMb9|egCVxc0ocIpo5r+P+>y za%jn<6?N*JfsD*uxOW8m*}EN$N_k|SrOaCuh3sl-YZ|_7zI6{Z64-CDRJ2XlntNts zO)W+U#j3$FAyFmHAqtc;e1WT*k*@hH2y3qJZA}|n9a?sWqOcQcS3Jk=4NDU1l%{#O z6^V5Rv&WKHSL=B@y$k4ed&G`lA)1*ll_mpMcIa!mAV)%pWkwpMGLBm~YSoN<5^sah z^R{2w81F{oM%+dm!-$Lv$OwtJ<>|~@7m&pGh1j`yn%T?mlk6At&HIwq_9O zMQ+MJhYPQupK|4h((P2JLxt$Bi%nkpH0e_ze#GcU`csnE8VQ@ae%6sJd9yXb=F9Eg zCpyrqf@(b5*a?as-k$_Z!)i{tLcP(T+i(t{{=5%icAd}%8tOX?1Au}?2kRIrWTD22 zradJk?PG`C#7@8DrwNSKQAY5FXnTz{A8zRL0%>;YIBssDA6G1N<(bdB`d&Vdc(y>yh@5AwostxZHDft{Ns|HvspLX-7zJ_@<&>PdPPI8jn z%7}KiUW^AQ+ujYgoh7Pn?|>GD8phVvPgnNI3U%LY{M0D_GFyMkll^WPW}7(~JxF+0qiN{&WlWZZ z+UDJ1kJ3*5kY4!5?SK)i!q<2R{}2Eyp(S z0yB)I=IBxzeBTuvjVe8xkXoh}_CSm(YxrajjrkSRnd_99El1HWap zlabw`Y*z8n|7bgb8j>}v0=GKkBiTRMxSK8m4D)5%`Q*k4nrdcw3`LgmOwp^!f$AUL z9|AmmPH3hVaP%~pPGzmB2aBB>DkoCvo}s|tu|80{;>Rv`CE9(Xq8F4(#f5I)pQtLO z7p7B@-y>P3*!J)RKWcCAUBI)^ic91)m)`dgL8uF-D++6)!XA71J_{@CAF{qotQX8zF9Ic~_WxnGz8q*!&q$Ko&nTf7iQoefTMjc1PLXrv2v6Xj zdamYih-7CgW_s+yOQ%0irH__~I7!tonZJ;t^E{H^exknlCf4A&Qukt?@-?851{Ps1_zY_)$@wu_e6&{7RYZW$+`o2$- z1AaW8Xliqpu3ZICeA9rt%X!tq!u#WE;6?*S_zbJO9LPvEZ3e${xs|b#@+nQu&jG>_ znsZrRyuYGJJ9R!hnqRXsuUpBWX>qwQY=^fSgOBQjphUy(#aPsBrqbq!24~(GX0EQ1 zBK+*0P1AC0K=ZPdBV6>tv`8w@k0RWO*8Hww{QO!#o#kK+!G{3L952e{J*7v8JKS2* zOv5<&QC-~}5=4h=gRB9>Ui4Wk3G$T+9Ir+?g}!eSKYgG#>{q=<`HgRiYMU$f^V8em zfv9@7HnbXSgZgV~6CL!aqA`puB z*Ss=Xbo7OGGvMyT>^9$nSjjvBAC9v-StTwHe6$d3T8sA5PI z$!@wk>j-HnZ`8hDu8Iz1z85vF@0RZi__=r#yg1r*+FsT9c0#A zy&u*!wI-*nqLq4Rvhyqkn9}bS-%Iaw=Hp=!-K%Gnc77*$1DEGk%;T95vU$G_Q7h%^d0xBvW&W*{ zH&opNH||#3J&bXZ8#Z&V)WzMl$%{~lQ&Q_6S!@C5Zf{0qhU~#)##fA-#96Q}?q8Uz zd>_&k)U3=EJ`A6Fn$-;maKLm6Z;jI}ER&NKUr{uOC9lpJ9SSKjDzg)|7V)sDh)h`s z`#>S0RRKtC%kp(GRn!yrD}nUy9+B`)DdpF&(K&(7NTWmE6lVCpjBZRfO{um4`viQm zneLAy@2W4dF8Z7nh(4-*6yZYC$1a=pLh{L@;k!O=R!enUDkc<8pz_zT;|5z4_?CJx zQSvd?K|(n!d09F5P0l^LT+9091{ zaDOSh73!rgDvGaSp1!kToyo9_d_<+4@Qei~0cJU{dz#5Hv^G1cm(wBInetNRP2tGL zft=a*+I3txF?Ct*Bf?X3l6^b|;2R$`>X)TIt+o}u$uTnBEbSj@@mXyr6_{#2toIIN zvg+jS6EQYSomVnUdj)rJ2!Ae&#Vb>c>iHT?e6MvRc9@`;#3qxXY-D_fmN6$g9+5-+ zt+F#_rsQ^Wu4)4-ER0+av;rOAfG79ykJLY=T)IfHDHO&OmPyKfoUUI) zp}xzlaNxqtV|J_Ul?Bz?g!>R-z^tP?AOhoUvO=wu9fnJaB!XpNRl9eLlJ_I3NTrJw z?yPL$Xm4ciI85ro!z@7S=JxW5OQIxewjyarwT5&Ek)=3Fcb&_xXuYrakbXns5%;T> z61#)%u?<>BCbsN7{zoc4zEf+$n5eVcl#3=)CY8Qh4KograTU>p&R;6udlarSIruDh zw+vOeq6bB9m1AK@^ZwPb*GhC7g+|3!JEw8RXhG;e474i+5`{NuD8B{E-_s8c*Qf76 z4L!h$-M5?`pS*QjtYpXXluWErgr#dv#`oiWon$VO>=v#rIx@X#k0)9_-&t38K9p)W z4Rsm?I7X|CoN&iSl#^_ld2R;$a1g@&1o!rP_~sb=$-}2zDoC7blJq@j7d2ITzg(*w z%w3vp{ARYZk}rGE`B8O#$=z@TC?NQ;NZal+hAHQh%)JMcwr+WEoZpW(DR2$LgjA}7 zXiITa@?+ZNm0EqxyboEt>D{NfKh}6#V+to{W0k(U|5V&c_vzuQw!*erR2SBXTk0WX zCPZlpi`i(;(R#!+y_$0>PY%VJ())axQ9ZfW{&xRIW#oymkm0+pM557mwUd%>C1*Z# z>5Snx`%t(gPPoy2ush*8$57*z9#l3tO!8CkhwtH39$cY7vdLGV)nJMCjUOZzW0!j{q5 zqCLa3mS19DC7*pTj&b@)V@S(+!bIkn+ke5K{K*9&&85e2{1QcD$ z$5+MTT7Ugwd_jc#^OV><|0V+Vi&XiK>Or8}-N``+_%B%CZ(;-lK>W?w{BsWmATHRR za~ksR=MVs*3d^GhsrO6m7ZC+TKw!TKo?ps;(^E*$zu<4a2n2ya{w0hM7aY%pC=3ex zEeQwy!}Bm;t4K-cXse+U_-HT$f#+$JU3^_+^v{DR{wI2ZzZuZq`oDk+n-|pAKTMC{ zFYf2}EeIg^H|h0neuBT4(%;V^06`cU+k>;J^!6sB#4p_odk7>D@~@K%1HW>F3L^gn zFRWaEa6$OL>71MTs3MQ8DX*%jBmIl668yW^zv!yMauW1IRdEbK_^-VFks_|B;S~IP z3jUj^U%=(O1kp8Wf+(#w>1QiqY*QVwiA;(119}Svi4J{g6_!CEVSKdomTx9S*n&f> z40}ACcY+tY_S%G|MzJNbIBulGXF;v1lH~BHrwYN)7oB4&RWn6wGi)juSU>X zECoKIry(R=)-!^dLo58*5YOzT+-W9Xvm%r?iS=%+KRg^D{rW$E6`mi3`4a+9NGX1)2 zFWC{}$`|1HsM0|jaAhVfw_}j4&XP+dUQ|PNSxhOMISTc{xs=w?qagvpR$7m+kOuwa zJB*zVaqEh#IurxRY5{EZ!9KD6ObriN&+v6CZ>=%sGSKl(4r0A^C&UKEnH4Q3##_Ff zcHIP6&_XMC~=Twd*rmhnwlQHg$H2wUHjABb^|O_3FHm+>8p zJ;Baf5C_!C!E#S;KG$I=w`|4mqKj)TUTMz!cLHK(W9!O*pLn)Ra6sGfAyB1rhhYEp6R#lcP*4k zFR$k2@3*&ZP%IvMrm3^5-N%!xNXsf7{oeVp+tQ5*03T4rtQ0h z>3I{np%gz7dxuI3gW=&3@roC_P_yhwS^ySw{B+@LOvzc3vp`wpgLWsI2)qj# zV`+DuQ4qI0QOv&<(I(g=PTRBykMGQwWly_! z9Ob5B{BcD1#7KP9u|5Z-wuP0&b|iT#Gf3I-z6e@$##leg+MclGQ1RC|A=R$H|Kv}@ zUmnHVt(Aw#>79r5nxxamqVO}NU)wd560qUk+z)3OlknE~h~BzMR^msgU573ubO4-> zz`p>CO99_0c5m&_?u;xzSrSOXChbTM+FQ+j6a!Tj-mkG9CQ4MsZ4^&WNKFVDV(?ekxdma+8)& zRN%K|7Vbq`i62wy$d~1xOq@<&PP}o4GzT#jp}OrYpKO>MRR4s(UsyxX8@yq*HF%vPhwrQVSla{NLN7{BwC~vaN6r_qM4O<8a zy!pl*cK)9o4Fg5BWpxK_oOfz5>Q0)h?r>xI^1Kh@#lX|(z^I?WKZDKFp(u_J{b6XE zNl`8`bQRYv=@Gcq%6LPwCf#@-wxV&W*`4!;(2o?0Vhe3D9V6Wn62~asWWyvs7f+LJ z*bnf_;1hiN3vS2Q+Gf$iFU~1E zaDVikO+oQ$bw-lU+7er`W;+-v)3&;}9&FQ2ML|PvYHG^X=Z{O7PfsD?pFAWvW5m?X z_l_XnHnx~vw9)CC`y0_2JhdkvJt>cb@r}iy4uPg7r0o0hZ>(p}Qb|y0Vch9XiN{-g z{`lXh2y}rz2t`e*?gZQ9sv{=Icd(jeRKfGIf{9UCV?FcOuO}+5z0SW?*DhJMG*4dX zU9JZF*84Q3=DVb^5V#_^=^BiTvB%bYHsIJf8U@ksL5Fu;zw$vK&YsBUqCU&!Nxx2Bjq-M z)dyu#&FBD{5(>wYOf#Z`^f0#B&O_<%!ML}pzdzOAlmg_|ZFMzi2k?IS|pirA*=2c7EZjD2lBSzc6h$W;PaeNt7 zZ3=^UUeAp6iZ4R8WofJ{@=|(TM)x+`ySwgMKMr?hQxC?iIVR)08zb6)IfVyjz~$@l zR4nkUz;BSln3VjiOdxNq)92yNO-fo zM*6ZdE#PLyz`5-D7r^xPK5n^uSBwPQqMFw#RBx6eG}94le#KDo=;ej5V|&_GBB{y# z5c9MU&U{U|oVN#yBcUsiY@>m!_g@Z@-ZN!@jaK$h6y_uOFMuXSOJaH4&)Ih-v-#U% zer)%ue7Ze-5aZKH6u&6Wu8YHHL$9rIySH8HHI7b|7jkzyR3p-rdUkK_t$~;Y>v3X4 zibwLc$VqZjxCr~}PNNP8V~m%~>zyC;Itqj|gFGsPb2n`iWOD*ZdfZS{%(8{Hna~DeimdXMN1E9$ap*n_6q{^xNfB(HhE7 zE6sd~I%1wsemAGKKGx8$XcsY~AD&fU1?bAFkVzmE+&C5@Fa=RBrN< zf9j~X*7Wqa)%3gCTC7ZcOw#Jw*lBj4ru+Vg)h(8skdW~zr@2R^eSfKEQ1o$R461oq z7je0x`ed8McwsVzc^|kvcD3rYdG-w&-kLSpOjSd~vey548O8qYLn&;irQ*=?SxNgV zoe#>VhuZojo3Z_2%jw^vEeO>TUI9ZsSUkUbcZapb#wfFR1oYf+=@@IWe}aUDO#w&-T@R^OZ3&ASZy#~X%x;X7h;1B}x* zwo$72*WdTc2G`P$HO8e@*Ad*Y3vgSfD}O51f$k`@93L4rU*5F7-AAb=1wPAj|GFYSxdMCYeT+?`wjNZ{Yw`d|09 zPL9$Sr-zV#Z>R-SoUH!${=bc=x2v@cJ`jKeqy1XxX<#7md7u{;z!8A|YXF3RfpGN8 zRyQmV9EK1?bF{Iekic`Ze@cO27hCm9*g1F^10nwp3=TQpMgOS_0)wvT0+FC!a_Igx z7SzQ~{*np^dR~G*F$e^76@yCm*oWiOBnUf@(cwEUMbf(cBL`Tv5PZve>gtJuB;1C(0OxRmIFZ$moXD46nUjV z&an$(^G_!*;FV<=3IqP{YUb{0ZfkGt`itY$vh_Xx)dHhQ-Y}b)TR|+~7M9j9hy} -(* -side_by_s ide_figure*["text-elements"::side_by_side_figure, - side_by_side_figure.anchor="''fig-Dogfood-II-bgnd1''" + +side_by_side_figure*["text-elements"::side_by_side_figure, + anchor="''fig-Dogfood-II-bgnd1''" ,caption="''Exploring a Reference of a Text-Element.''" ,relative_width="''48''" ,src="''figures/Dogfood-II-bgnd1''" @@ -625,8 +625,8 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV- ,caption2="''Exploring an attribute.''" ,relative_width2="''47''" ,src2="''figures/Dogfood-III-bgnd-text_section''" -]\ Hyperlinks. \ -*) +]\ Hyperlinks.\ + declare_reference*["figDogfoodVIlinkappl"::figure] @@ -675,7 +675,7 @@ This example shows that ontological modeling is indeed adequate for large techni collaboratively developed documentations, where modifications can lead easily to incoherence. The current checks help to systematically avoid this type of incoherence between formal and informal parts. \ -(* + section*[onto_future::technical]\ Monitor Classes \ text\ Besides sub-typing, there is another relation between document classes: a class can be a \emph{monitor} to other ones, @@ -699,7 +699,7 @@ classes and imposing different sets of structural constraints in a Classes which are neither directly nor indirectly (via inheritance) mentioned in the monitor are \emph{independent} from a monitor; instances of independent test elements may occur freely. \ -*) + section*[conclusion::conclusion]\ Conclusion and Related Work\ text\ We have demonstrated the use of \isadof, a novel ontology modeling and enforcement diff --git a/test/conceptual/Attributes.thy b/test/conceptual/Attributes.thy index db8e71de..193a9450 100644 --- a/test/conceptual/Attributes.thy +++ b/test/conceptual/Attributes.thy @@ -85,7 +85,7 @@ ML\ HOLogic.dest_number @{docitem_attr a2::omega} \ update_instance*[omega::E, x+="''inition''"] ML\ val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \ - + update_instance*[omega::E, y+="[''defini'',''tion'']"] update_instance*[omega::E, y+="[''en'']"] @@ -93,4 +93,28 @@ update_instance*[omega::E, y+="[''en'']"] ML\val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::omega}); \ + +section\Simulation of a Monitor\ + +open_monitor*[fig1::figure_group, + anchor="''fig-demo''", + caption="''Sample ''"] + + +figure*[fig_A::figure, spawn_columns=False,relative_width="''90''", + src="''figures/A.png''"] + \ The A train \ldots \ +update_instance*[fig1::figure_group, trace+="[figure]"] + + +figure*[fig_B::figure, spawn_columns=False,relative_width="''90''", + src="''figures/B.png''"] + \ The B train \ldots \ +update_instance*[fig1::figure_group, trace+="[figure]"] + +close_monitor*[fig1] + +ML\ (HOLogic.dest_list @{docitem_attr trace::fig1}) \ + + end \ No newline at end of file