From cef4086029e510f7005b800c35130a11d1259d0c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 16 Jun 2023 11:54:33 +0200 Subject: [PATCH] Add basic support for beamer frame options and add a figure_content antiquotation --- .../beamerx/presentation/ROOT | 1 + .../presentation/document/figures/A.png | Bin 0 -> 12194 bytes .../beamerx/presentation/presentation.thy | 35 +++++- Isabelle_DOF/thys/Isa_COL.thy | 114 +++++++++++++----- Isabelle_DOF/thys/Isa_DOF.thy | 4 +- 5 files changed, 118 insertions(+), 36 deletions(-) create mode 100644 Isabelle_DOF-Examples-Extra/beamerx/presentation/document/figures/A.png diff --git a/Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT b/Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT index ebe69c1..4478623 100644 --- a/Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT +++ b/Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT @@ -6,3 +6,4 @@ session "presentation-example" (AFP) = "Isabelle_DOF-Ontologies" + "presentation" document_files "preamble.tex" + "figures/A.png" diff --git a/Isabelle_DOF-Examples-Extra/beamerx/presentation/document/figures/A.png b/Isabelle_DOF-Examples-Extra/beamerx/presentation/document/figures/A.png new file mode 100644 index 0000000000000000000000000000000000000000..0221da4fa35501ce17f1ed3cea84f2175304ee0d GIT binary patch literal 12194 zcmZX)1yoc~+dV#j14^qy2@EALN(?C>rGmr|LrF+?cQ+`Kf`kl6jf8~KN)IXB-6<*E z4Zn-;_y68+tv_qQ+`0FjbMHCldG^_RKZGF_rHSw#;e$XRB3T(p72vZA_^rQ-3;adO zz?MKD{GXPuULj>)y`o1t*_&C~n1VnuVV_ZWYN`|DANnxsA7kI&mAQvuN(BvCgR(WK z8SatFMc#WMWfLlh%@iJfS5qP+e_j(rMPStU3kzWuA^>T%-VYlzWCroPPg->Fhnv~xh&()@lmOw}ZGa+$bi&$s`S>X5 zzj$8j?p(xJNLH}3IA2{{+&ndf>NkNw_)>x~tP5uJJ~Sl=ofyG~AT{E}vA1bYzARnc z9cqyYyi1q9v}9Q)(h)XvY4DVVXPSCJ8MJFcES*9KS|?aEH*<`O5iucpU+`WekaVHr zsM1kYP~?3C>9f9eP2mpPyVR`L%u4%nPAr|yPJ$gyX?k7pyJFa3u+*~so9U>Vf=HM3 zZW^!97}eic3+-{jRrZ#McT4Q@DRex|*t2SvkQ^DD46{VGy{L3UXdA1H*fU?hT|(A- zm*e{)Nt^9dMFvA$t;oSS`5X<(Wxp1Pv_`MN_{}Z+pHC|cE-yt8*%p>`iJ8r zB70%~OWbe2eSR~U>rzgvx6t&Y2UPU>Osn3uKC(Y*aiMc<8ru}FJB%fh^!6_^4w0TB z;xqc&C=;pnHZ#VMt&4Hw*>#o^_A7Hr4;(B~Y_WC_O~W0m2D||I>+tT5MGPwZO*pvY zNs_$M((!JR4a3-Ailwn>54OQRr{c|s{f_($cWB_vc9$Yf1CG!|@s7Jbq0=|&zgPwq zJ}2u;=5cz25*Pf1YAO6%uavG0K=)zT!blwLb}b%U@&;T%5XC%}&kOpySTXd(?6^9g zf`&P8yIv4$lI*`=7{_-Daw;aF0lCg|3F2!vK5-z{!5(W+=*Qc}p`yfvH^4kdS{d#( zy?}(`=DnEwgk^#|A;I2Gv>zPw)d5B<7ZA(9@Hp5BO@w4n!~XnA9VvRq>+(PtPdCsD zUDHp`hm8poYlbBf4jC$plcwR687K+fje1Yf*s;qaNZtFcqQTUG-{-DfU|-|dyqG3# zeLx!$B=wRTDGVck5G;Shf6U3q=uCbQU7T5@>gaxvI5C7j2LF+BUgCEJ3wwh z;Q|uI?~#JPDtbZjwQIn2jrN4TwS4tHT*j~JRC%K&HvdHrNGQuck-E9FOx14E;BCUF0*y^ zq@DSmIKgneLm*CS&N;f>-sr%E@s?A=dkN&n^fX6VPP7M+^;cdy)ibpo|y^$Rue z@7yCkBZI@`dB5^S)ug{C=ZECMHRitiDPJwyoZFx#rYFE<(YWNb7&Cp~j6*S{~opn*q*d)&0& zbhoj;ovYO$&hYyJFOxb`xpKL3<^YaycuCD3&mXHlQ!JVf6J)=1K;x3X73X0r!!3i? ziFn7m8|4kk+kUjs7;l?!@)bR!E2e+zp>3kYr%kBM!~TxLnd2>oe$PPqLviz|ltQ7o zADab(1;pAj72mY+v{$t&-qx3J|5}(-8=o%E9zUNb{AF9_Yin-SRxxGm-j-%2-sczR zn{%asCyiI~Dy}&+v(7lkIQtJMq8Hzktc3HqVM=YvsBo&&`O@Zm%DT_+nGyv7iVua0 zGI##CvcC#VdA^jt(dk&=^tp=+MxTYtQBu+-;tA+J*D%aQ zYYlEVUff?CUd*~Mx*)Wmd;e!B^L?WGJ4_hH2&NrrDrwnF;Y_kjiq~V({-JwePr_na zdc$;Sy*U&`6-md)qa&iDio)pL&es^M1}y|16C6++!+ErS8V!7I`5Q4rk*=3f`MzvP z6PtyBl>CRCrnjMCENpAOIv%tj;;Rv4POU;-s5$xQtSQWr5MOb z{9rr^+x|t>ysMSO-@0KEO9sndmJipt*L$c=Bi~2Hz0BuQ@G#699VA0|OPXc)#MmSq zl%{sQZh5iz=-y+k$Ch1LObUIjc_l8HE?iw4-x)Xl?5{1iy@3^x7FN~`x-74JRw}zH z_16y8YtbD^%8V-$Gk5s4`Zu4y|I2UwRO_SBl>%D5)%rp^QAgj&bA9ImCxp|SZRkXQ zT24|0r@ckyO>3)9u#e+)0}D#w!cXFc{`9MN+1AQTay{8Dej&LwSpvD=lSOjftAX>j zQaaZ1$F}R7Zm`)JvKsZuU;fD#<<$?CV>e^JZXJ|YY#MCC#`o-2V^cNcw&YH>7`J1$ zV?TpYzqUr_Fs>)4{rLSl{G#v`xsRPapXrWwj}Nzx#;1NNIqNUf^<983cGS)^eyLHv zK|vd!?ZUfD28WG>>6+prW4U9HQJ(^`(ayh38=S+>N5=##_#gsJ9|v1wUJ;PYh-^An z7Ib9fleYWkBuTYZ##Y}A=& z*TlRAaS^7^?w==`?VP{(vvYls_cyPnIZLluI_(CjYpn>%$1c}dcJ=C@WYu2(ZcV>0 z_uAqz!VlH!?&+3_+4MRaCR=4=Eh;T6*K@8Mb(*<857XcB7aiE@pK)s5dp)I)le{JB z?A?1VL_?uiG)62i7=}>gO6ii<~k&P|r zap6>98~hTlC|@h(C7E&$q>snK()yN_rEZkIWflkh=gK8o>0#>t@LLc_#6uW3v^8}xr1!A3 zv2zyo5M}&#hcIw_dm7G2|L+zTYf(l`1tk3|dnZ$Reoj74E=DnYdU|>hClfPa70K8C z(;WCF%4p%@;vfu%ySuw{y7O|{JDJ0|g@lCQTs&|d9uD9R4rfn07efyYJ7=c}2WSVrg$jf7`F2k-e*nC?n(TgZ}sDKksSkVfo)D**X8uuz&%=Z?C|)Il18f z+c(fuPucD8@Sw%mpto7yR$j(X2U$K-iR(VG%=`RSu5w9cjy_{FD`6#e5t~!> z!{UQ*`k>P9XMU?fsCTH1EB#(Dr_RnzOS*WK)6PPD%IZzpNp0Ujt=Qu__RAKHfFg-( z4YXeN&b+`b**qJ45$IhoE4DsX4_kx5KrQm}SsnIKPAL4MD}WC-iSYW`>#USnTzt++ z>vH4IAEuk4;^KA{ZEdSO{rWl&h5d`BCL;vKOUwvH*VTfc-~fZci*M=n{EygCoL5iv z_3JLJCn!yxu(SV+*Qrwgn5q#}TI(N+$hC$Mr?#W^OsSPBCPXrmdya`Tnc+zW8W{LjG->sLW!S zX;w$hqu;)zq55yMwHc#+$<)!E4EhmnU^pQsI*|;1oNW!hPcigGU#}=DTTy-(la4kF z=W}BI*3aIyC9@m*XDV(qQiZ*!MSSN%vsJ`IO0#d%QKL_u2Hj9a)0iunUKj-m9+%x0 z|0`h-fhrJxU{J|k7)x^9u7o2~+0%f{5>KXiI(F{N*1ij+a~#^0_CY7K<$CA{ZtVXl z7Ugv8M(sWF@9ev!zj=Zmj#d*TMi1cP0wKng9=;-`k=pf2qZ2T{g4)96v7e*Se>ySb z?i#(pZ|$oaOI=j(J5`@i2=sY1>ldecM^4_V~V+cPz)+S*?(F(oA>!x>Tp zlRquvd@!b6HBlEg+@oC zjG=-K0m80-B?kru_5~g6KM+#A{QC84d`t{OTOzmd2O1`3W+^|GCr`q@@LRtQ3k%zK zwX%A8c6O#LFCXc1(-FtIyoyHxmCsR3Wu%!pTpwEYKHiywi^qNXMBk=aVVCNIao^Fi z8u~`mlOj~+Q%6Y274U(Gnx&86z!aF4eNAqCE^!CqM7SVpt)il0!hz}W=7bYrH)?*~ z;1RzS#MIQZ;~-hYlLvg~PJAC~xeL{GQEJ$X>*?!vx)8E|7POJGg7EODtnCww3Jnbf zPIyvNP)PSA3!n~|>x)CHr3woJ2x>tYY(7tlxsa4Fvpe{p8Ubc?5_ZODbVH~*jk2WL zVyIDJC^p(=ruy@xu-hO`*Tl5QU!H6I+QY?cR9=D}K1{RPzuck(s=42rii!z#j>lf4 zX`vAc=RlHkXiGK(yy;a@@ls|vP3d;#iGDvf73b-Vrl05&{G5lEKtKTxYmaTO(K8Z= za>vwqk9FNg79%E$Za|{N^miD{7q$#%p{*wSqg#edXdnXLu}I1f;~;t`bnp{DHMm0V zM^!~Frn*ARC8z}KXiU>P25=C{vU%NFmGkXjX$S|VU|y37iA49pVZ%5CPULF4RXly4 zJ$bR2Sy@A7(?q05*n?zPP=@k`hWG?&O|vfz2f|>WPGE6!l^jB$nxD$(8_f$f3YQAG z$2KNcy{fPw4mkdb&wt=0G-Vi75gMyJj$_0GLe`%mqiBR)YU)~&F{}4BZ5o=9=x=N; z8tfByWC~V7thh|WFlBU{6z>|g-M>CiSi=+845=K47Kay z9QGv~h7bE>Y7tSd*4xC%zS)G`Mycdx=!l0zMvCttKIoa0gx9|*(TyoyHLPLm`^Dx& zfu!%cOT7LakDU41NFRQD)b##PQXlS)4Hk2Vn@#(HNB;Pf)V~BvPpkwhZIx=iiWY!9g=`eu!N-#5d78deiZzbr_|u5MrmeD>39%{Fz@U((l0U46 z4H>`nr_EuLHBxx-H&b? z85m@gbiKd#FxUHJJ3b+S<>QHwv9WCR@x3le5r%S`2}XUmUTxwo!9W}w29xn4PHz(g zL8m*0hK5Wze>yC@Jfqs?weJ->NE9!YRX+e1toJ(-97z50ZSV<{6>u`I)u5U;?49_6 zFd)1jwhb30RLQb6g@UDrmAP=;FrT`aq)Wh^@lRCmrat}|*@%#X%fyM|c47q?zH)K- zdDz?8-JQko>I2fk0%mGrLTbUqYu1e}x1CavlMAoKl9iQxZ>JR&_C~sIcv$Ua+gxHI z<=J%{t5Rnl2~;FeG1Uk?-}u*3qNA%Tb6TWlbQXyB`@w;?0C+asGNd^&v-=5|EWWU? z;ItgTv2qK5WOvhs9UUD9-w}LsO-sql&87g-D)#edsXwfeYf`sCkWC>Ck@w=o0>7-k z&-A)KAh2jHP%6Csy-KWeyv{^P5=xKb9@xr08b}=9i{tD=c2&`qIkCfs}slQ{ra8Y`H*`8At$W~OiuzK-D3 zUpKZlssFNo7aQzTatk|%-Or~4BX3!xc*YRiLWQRI5q6ST$bO?{)Bp7O8a@9NZ9A9$ zTVKA+{Fn=-WEKt+)VO=)b?l{OPnD4D9#tKAL$RTpXl5^mmPp{{I2RQyhV4-hRN#jm z!Nyp6W=CkGq#)V)0Bvl+Z=1YtClyJQW1jAtu+oz(O&X24*seMJ{ZL6}VB+t{_w|U= zk>P4rYo7120<|HoWKsQ@Y7_t*{QfJ4c#`*9pB-FC6#Qo{cOg|Ew#A71()*9?Nq`<@ZW>1 zp>T;?Qv{5M7YB5inuHkUL(Z3=x2V7U)^`{& zph!SEC0G5vrprCM60i%gL@YrMxhZrl^zDB4^bFy!PI^p$~FW3B5ReGBw9GQ^B z(5(0oIx8$Gsl?)w`gl%W!g$WCZe}aSq&7-9VPZ7B47=uO5>!)d6;AqOVyw&8P3na$ zwEhwM(Z`2Z7tp<&_6pWGEe`c9UCn85Jc;<_C*d>qQ5=HfMCEuBbR`LlZP9Gt2sg|Z zxtgHyE_V~7kX!-ZVYDTWvm2JMdI;MMM9ltrOTu2h2p7Bw)G0UVc%aqu%l*2mxA)sX zrgU7v!Q6C}^K#uOK#a2VhtH2TI>yFOZ+>Vpv^9iXTwDwd=dEn<-i+^13*Y(enjnr} z(c%#z-t4s5VrRJjhzI$aR7Z1@EUKK(TPpk~T##|q`RCzFAcz1a@(NtI!cG{!KB(Yy zbA9#T@ZP<9gSJjH)vo(Tvl#Dt4~CO?%{yH=?WO~;a4g1)4foCFzsV;*Q>fO4LWJ-m zR~jsij(lU%>^+iSNr;@jBq`ZA;^DWOuRK?oEI<_Tpc}pm z8>(kOHEmk-Q!ZAUZ$A7;; zXv zqLfXL^J|SguU`0(*RtqKwpV47WR1bu+EdNM016I%eTDZ0dO!knz{p%KCX_KODJh%a z6|c9I{OI-P4@MN-%BFr^nsm*5r_&y+L?j1w*DzNq<;TcxN~{JF5!By=flb$n7*-}8 z&MCeh>J1(V!Z!W$q+hsjWYi_?4n&4Wk6Kus zgxz5vL`B8b)3gvp9Na<)3nB557I>~D$Gk1b@O*_)%T+U}??P%#FB0W|RV4q}z!VBG^Bv8ByV0 zP<@+7PpDCdnrLoCz)d;#tkQ`;NbHqNEB4jSZva70uH3l+6Uxc6@4_Q&vpTep?j%DH z;f53S%(i5su;t|C30=1zp#L#Cv>FMF3l+M#YA)DlUw`2zicS$?!g@}R{=A?${yME3 z7RD4ln5l*X^YinIkA0ed8uPv5y36Q>4nQArJ0ai_R2dZC{qV`*T*Y%11tX{En}(;k zLtDIbknx!9`VNoU=R3CYwTBOy3aqff>OQCzAWiadnAzAO>XL5+nq_vAag~Pl$_j@z zS&40I1(hB8V^%5F~miH*z1eRKj zJhd7s#N6g=1ph&~ih)KzEaG7sVfIF6c?fsd)=lr}W3VB;+Ax948(i9B{awzW7hL%tVJIn?auec0w45eGl{wv88_dP40uf< zu4Re_6>r@9YOoyMC-RDOhV*ZKzYEd%lTLi~gF*{%OJZY!ndHa<9*|1hM5UTgs{7nQ zZD68TK zDoxg;T68|UFV>^^9Tz3fZaz{AB#g>2Y+c)&J}1SzY`cN)cuhE9bg<-V+_o%MLg?1t zfrTP69uv}urJSGa=-XL5vmRx)d|hrm#+fu`AR65PR$`}rD0-%b$9%V)hnKgj;(~{V zXGztyHIm9HG9I#HmF|1I1g-9R@v`W_?&SGN6rT0~D}kr?_~`JApEqTV-tm1YY^l=* zO95V$Mfj#AFH&ctlHb!qBS-0S5}UwJDJ~~%SvZ_tYVqq1KC%JcB^HOe5_18~ted=A zIKQ!a*>(r7XO?TgMhC8ohN+%hVk=0?eJ!qkP6=90z$HPNB$dH%vYpTpYdN~{?+w8Zd~m~wk^7bhlbSh)aSZoM z>~Qccj^92j$gZC@uD$afM_y%L*$BOc1<37T--{zBV0y4)VhN&p8N=11_j6xRz&E0X zxA+`>QeR~Gc`3cV;e2?V#^TrBfH9X)yIEz?d+F(02srO+D!4i+Oa=mL^!U4WwT81BR+2g z-?biY<`$kFkD!cM&NH8?riHx;HfBHa8qg#UFs8bBQM(kujV!D@)*(~AgOr#WB=^rt z39iy>O~`i$e-B+Qm~B;zGq|yvJy9*7n&6bbpp_MJP~ z7kHCI-?LmkO#I?b*Kxl^EU5wqANu&_Y>ySw4k%5t?1>G~^4b8OmCsnuhldBPHEEej z*;btzWkk{UJiA;I=9H)Z+Iy^LyJ0p1g1qa!Pwaf-M47L{qoNYj&3V_A4+EUy ztKFQg@7#PhxMbWbbVZB|6b<=SJaQ+%F?e)+?O0_P=p5{l;tbgsBpAc_CG`_Oo&UlZ z(~ey%acTN&A%PP~54Jm&G|o}lWli@iISy1=**JUvWXp%VzyaJ`q>bN;xj0z?sc69 zlXQHk$t)B$A7N^mJ`lkkE|ZsXQ>%-=`2g9}Y}uRw%Td~%SKb+=LONuw_N7ao%$RO+ z;1*9$tTBAyF_o)w@%bHkUuC1ngvxoPJEkjUX=%x6y>jYH>YL_Z@XCYFF^p_#E3`{6 ztM%;70tccGwa?T@02hbs(IYuRh_!z_8z=k3p_RGuB4f&)z*VB|s@*X{oN^h`pNnN-O=NoH)TKz2kURKv{$20vyOkzSRIaQ;-KR z0R~|V+}z4`A>Y1z>-+}i;!xfCRAOzmaf$cJ?679M-oO5m(94w1dNdMXO04?EH6-eT zNv76{?_W&m5-#CtItSUQ9$mw#vJ`0&@@bR>GYonGN(6#HtO@WV04|UZz!~Fop@RvI z$QaSC4c(8|UXT{(Xpi#nJ2Htz^VrcJBRB}4f{|52|Hwg7Hjbi?R>c4}+#Gv30$%5! zd)Xpkh)!gdR=y9Gz*1e9oBJ^qaVy4pm95gv`T)WBwRqf~WD3}}k@GmKrMKpeMB@sP z#bemDXEkK}vv4>sn%;b(;s&i}5~%V3;=5_FSEw;l5>k*QGuq9DPERB>JlKk?dkY#eaiF=UbQB7ZV?%R^FnJ4YkfVRE?m*^dE}q13z&+EJ}p<5pl| z81NCxtgX)K7|^lX5A3Q+H?o}|>=;sj-`!RO*1o^{XJE)1YCR^14I!cX1{L*c=WI6b zOUq74q1oou?-4slBZNFT^tO(?8j%m*f{hV zwj5A|*Z|PJlXAi=InXHziH7o7Ai+}XYe>y}rt|qmZH<)&g=#D6v@L*x?5*{=QX5_> zaY;rW8h;x_u+F%ofKr!r6|0$VslZSS!PYCD>!#&^RW5P)Yj0}jumSrWcfT%#Ik1OW zTjnKmAs!+SF zd(tO=s{N{9%g-~JC5IWeYMN4o_$dzI5O~Qw-P7>#5y@-i^5}fb%Bs3CTF~_z_CoR@ z4UK%}>yNRzdNHdoUo7|O&Oc%YHEyz#@pf$-n=(TC&_V@t!#VzUwt|eTzd&Lygl52$ z90rR%{_}phG#2YG#YKx{_E20u=0lqhaCw?CEaqp=5+;A04Bf8L*Euj8)BA80hSNzf zJo_cnU_BVGd9fvenZjXcW#_0NNYw0enL|`lM{Nb`!Lh_dscFP*1pb?wMk}kaZBeh7 z?5rOL6gytO7`LNU1g?}_bTwUMV&=VsCZTQ+Aol=br+h(7`_J69s)?=$5s-WM4k-K} z6bOW;+|~z!zsV;tQf~#k5-|FG_wQ6i(eTau>%JsjX}cswVdLkJGrCC9;^xpXJYpJp zh;L?QCi6}258c3lO~_btc??n)2VCb+lHRr+*z)EdvYlRBARPYWS-(|mcs%F&aa7qR z&T|R&6iCE$|Ldy%zWuBD-*76gn3kv4+AW_wOKcXi$FR*xuiBW$iZt!7dc+&Dhx3p|>@b6QEvnal6A% z+tLq){cm9R-1`O7?+Y86~{o7=Nu}WOSJInHa23-%7 znj*A|4Y0lrdL6DQPrP^{BBJvFjt1mKwfm0Z8u~r=;^N{DdBqn@4cp;P*RLozE@^(^ zZ1c{^yJq!e%w+@d{s@z^1bb>w55&Zr(<1YX!@rdZ?A&^ z$R~T?L>>j}K5F{SO^rnB?+-DnJl&&!V-(x7S>hO9JyssB+s1wQB!MrD5&Wi!Ls|!( znoR*E1mO=x7EF}`8#VKF6MUW~c%s=rE%_cS@!$;1`RL966!V^Gxoye=0B<1_*sEW= zG4fhloS~@{YFhfE#`9p1pb<-AqS7(5&M^3a|K2edK?M>YDNkGm`fr`WffktNCxN9l zRH=RN{{@gjOr8Kv@wZ#er|DMn_!@hIlK6dYcQaR2Zf@v&eze^4rv=Q+%o&U9 z`(NG^WHr=RRwk;bs^$Sj>Gx?qnir;KW-6im+0nEDdQr-nny^>GB31)@xW+$ps#GQ$ zjcQ1YH)k<#t;Pl%33kLi_a7fUIDFUME*lH}==kC*G4Z{aO{~Zgn+c~g?+W`l&bIL? z=Nua6Dj561Rqn&X%?VYDmARNNo;LTRs0E_Vk9OexAGm+CT5a7+Z*c_b#~%%-@CP17 z;i&7b(V&w;+{s%(Auv8ZwWz>8cAd&klNVk~%c%u*C92}p|$a}$_6un@d`ly#TMfg#a#{K9Q`Vu`rY-D6|<`Whf8Lv0uar#FG zX(P>Q$FCnBF~EZbiHwPfd2ywG&y`ZkN5)6XrjApe1+hEqny@&Ccy`k@w@=13Mpn6% zK+TTG5LOdh|K6aokaHPS1kw-OXG0cUKEM6|9Ao8Z1T-!l?(dSE;p \end{frame} \ + frame*[test_frame - , frametitle = \\\Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\ @{thm "HOL.refl"}\\ + , frametitle = \\\Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\ with items @{thm "HOL.refl"}\\ , framesubtitle = "''Subtitle''"] \This is an example! \<^item> The term \<^term>\refl\ is... @@ -31,6 +32,38 @@ frame*[test_frame2 , framesubtitle = \\\Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\ the value of \<^term>\(3::int) + 3\ is @{value "(3::int) + 3"}\\] \Test frame env \<^term>\refl\\ +frame*[test_frame3, frametitle = "''A slide with a Figure''"] +\A figure +@{figure_content (width=45, caption=\\Figure\<^sub>t\<^sub>e\<^sub>s\<^sub>t\ is not the \<^term>\refl\ theorem (@{thm "refl"}).\) + "figures/A.png"}\ + +frame*[test_frame4 + , options = "''allowframebreaks''" + , frametitle = "''Example Slide with frame break''" + , framesubtitle = \\\Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\ the value of \<^term>\(3::int) + 3\ is @{value "(3::int) + 3"}\\] +\ + \<^item> The term \<^term>\refl\ is... + \<^item> and the term encoding the title of this frame is \<^term_>\frametitle @{frame \test_frame4\}\ + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... +\ + (*<*) end (*>*) diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 2db41dc..6d4aed8 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -331,25 +331,34 @@ fun generate_caption ctxt caption = in drop_latex_macros cap_txt end + +fun process_args cfg_trans = + let val {relative_width,relative_height,caption} = cfg_trans mt_fig_content + val _ = if relative_width < 0 orelse relative_height <0 + then error("negative parameter.") + else () + val wdth_val_s = Real.toString((Real.fromInt relative_width) + / (Real.fromInt 100))^"\\textwidth" + val ht_s= if relative_height = 100 + then "" + else "height=" + ^ Real.toString((Real.fromInt relative_height) + / (Real.fromInt 100)) + ^ "\\textheight" + in (wdth_val_s, ht_s, caption) end + fun fig_content ctxt (cfg_trans,file:Input.source) = - let val {relative_width,relative_height,caption} = cfg_trans mt_fig_content - val _ = if relative_width < 0 orelse relative_height <0 then error("negative parameter.") - else () - val wdth_val_s = Real.toString((Real.fromInt relative_width) - / (Real.fromInt 100))^"\\textwidth" - val ht_s= if relative_height = 100 then "" - else "height="^Real.toString((Real.fromInt relative_height) - / (Real.fromInt 100)) ^"\\textheight" - val arg_single = enclose "[" "]" (commas ["keepaspectratio","width="^wdth_val_s,ht_s]) - val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_s]) - val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file - (* ToDo: must be declared source of type png or jpeg or pdf, ... *) + let val (wdth_val_s, ht_s, caption) = process_args cfg_trans + val arg_single = enclose "[" "]" (commas ["keepaspectratio","width="^wdth_val_s,ht_s]) + val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_s]) + val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file + (* ToDo: must be declared source of type png or jpeg or pdf, ... *) - in if Input.string_of(caption) = "" then + in if Input.string_of(caption) = "" then file |> (Latex.string o Input.string_of) |> Latex.macro ("includegraphics"^arg_single) - else + else file |> (Latex.string o Input.string_of) |> (fn X => (Latex.string ("{"^wdth_val_s^"}")) @@ -358,7 +367,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) = @ (Latex.macro "caption" (generate_caption ctxt caption))) |> (Latex.environment ("subcaptionblock") ) (* BUG: newline at the end of subcaptionlbock, making side-by-side a figure-below-figure setup *) - end + end fun fig_content_antiquotation name scan = (Document_Output.antiquotation_raw_embedded name @@ -366,8 +375,27 @@ fun fig_content_antiquotation name scan = (fig_content : Proof.context -> (fig_content -> fig_content) * Input.source -> Latex.text)); +fun figure_content ctxt (cfg_trans,file:Input.source) = + let val (wdth_val_s, ht_s, caption) = process_args cfg_trans + val args = ["keepaspectratio","width=" ^ wdth_val_s, ht_s] + |> commas + |> enclose "[" "]" + in file + |> (Latex.string o Input.string_of) + |> Latex.macro ("includegraphics" ^ args) + |> (fn X => X @ Latex.macro "caption" (generate_caption ctxt caption)) + |> Latex.environment ("figure") + end + +fun figure_antiquotation name scan = + (Document_Output.antiquotation_raw_embedded name + (scan : ((fig_content -> fig_content) * Input.source) context_parser) + (figure_content : Proof.context -> (fig_content -> fig_content) * Input.source -> Latex.text)); + val _ = Theory.setup ( fig_content_antiquotation \<^binding>\fig_content\ + (fig_content_modes -- Scan.lift(Parse.path_input)) + #> figure_antiquotation \<^binding>\figure_content\ (fig_content_modes -- Scan.lift(Parse.path_input))) \ @@ -728,25 +756,33 @@ text\beamer frame environment\ (* Under development *) doc_class frame = + options :: string frametitle :: string framesubtitle :: string ML\ -type frame = {frametitle: Input.source, framesubtitle: Input.source} +type frame = {options: Input.source + , frametitle: Input.source + , framesubtitle: Input.source} -val empty_frame = {frametitle = Input.empty, framesubtitle = Input.empty}: frame +val empty_frame = {options = Input.empty + , frametitle = Input.empty + , framesubtitle = Input.empty}: frame -fun make_frame (frametitle, framesubtitle) = - {frametitle = frametitle, framesubtitle = framesubtitle} +fun make_frame (options, frametitle, framesubtitle) = + {options = options, frametitle = frametitle, framesubtitle = framesubtitle} fun upd_frame f = - fn {frametitle, framesubtitle} => make_frame (f (frametitle, framesubtitle)) + fn {options, frametitle, framesubtitle} => make_frame (f (options, frametitle, framesubtitle)) + +fun upd_options f = + upd_frame (fn (options, frametitle, framesubtitle) => (f options, frametitle, framesubtitle)) fun upd_frametitle f = - upd_frame (fn (frametitle, framesubtitle) => (f frametitle, framesubtitle)) + upd_frame (fn (options, frametitle, framesubtitle) => (options, f frametitle, framesubtitle)) fun upd_framesubtitle f = - upd_frame (fn (frametitle, framesubtitle) => (frametitle, f framesubtitle)) + upd_frame (fn (options, frametitle, framesubtitle) => (options, frametitle, f framesubtitle)) val unenclose_end = unenclose val unenclose_string = unenclose o unenclose o unenclose_end @@ -759,12 +795,14 @@ fun read_string s = end fun convert_meta_args ctxt (X, (((str,_),value) :: R)) = - (case YXML.content_of str of - "frametitle" => upd_frametitle (K(YXML.content_of value |> read_string)) - o convert_meta_args ctxt (X, R) - | "framesubtitle" => upd_framesubtitle (K(YXML.content_of value |> read_string)) - o convert_meta_args ctxt (X, R ) - | s => error("!undefined attribute:"^s)) + (case YXML.content_of str of + "frametitle" => upd_frametitle (K(YXML.content_of value |> read_string)) + o convert_meta_args ctxt (X, R) + | "framesubtitle" => upd_framesubtitle (K(YXML.content_of value |> read_string)) + o convert_meta_args ctxt (X, R) + | "options" => upd_options (K(YXML.content_of value |> read_string)) + o convert_meta_args ctxt (X, R) + | s => error("!undefined attribute:"^s)) | convert_meta_args _ (_,[]) = I fun frame_command (name, pos) descr cid = @@ -775,21 +813,31 @@ fun frame_command (name, pos) descr cid = {is_monitor = false} {is_inline = true} {define = true} oid pos (set_default_class cid_pos) doc_attrs - fun generate_src_ltx_ctxt ctxt src cfg_trans = - let val {frametitle, framesubtitle} = cfg_trans empty_frame - in Latex.string "{" + fun titles_src ctxt frametitle framesubtitle src = Latex.string "{" @ Document_Output.output_document ctxt {markdown = false} frametitle @ Latex.string "}" @ Latex.string "{" @ (Document_Output.output_document ctxt {markdown = false} framesubtitle) @ Latex.string "}" @ Document_Output.output_document ctxt {markdown = true} src + fun generate_src_ltx_ctxt ctxt src cfg_trans = + let val {options, frametitle, framesubtitle} = cfg_trans empty_frame + in + let val options_str = Input.string_of options + in if options_str = "" + then titles_src ctxt frametitle framesubtitle src + else (options_str + |> enclose "[" "]" + |> Latex.string) + @ titles_src ctxt frametitle framesubtitle src + end end fun parse_and_tex (margs, src) ctxt = convert_meta_args ctxt margs |> generate_src_ltx_ctxt ctxt src - |> (Latex.environment ("frame") ) - in Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex + |> Latex.environment ("frame") + |> Latex.environment ("isamarkuptext") + in Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex end val _ = frame_command \<^command_keyword>\frame*\ "frame environment" "Isa_COL.frame" ; diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 914d0aa..7c4f238 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -2206,10 +2206,10 @@ fun document_command (name, pos) descr mark cmd sem_attrs transform_attr = #> document_output_reports name mark sem_attrs transform_attr meta_args text #> SOME): Toplevel.state -> Latex.text option)) ); -fun onto_macro_cmd_output_reports output_figure (meta_args, text) ctxt = +fun onto_macro_cmd_output_reports output_cmd (meta_args, text) ctxt = let val _ = Context_Position.reports ctxt (Document_Output.document_reports text); - in output_figure (meta_args, text) ctxt end + in output_cmd (meta_args, text) ctxt end fun onto_macro_cmd_command (name, pos) descr cmd output_cmd = Outer_Syntax.command (name, pos) descr