From 83151cf473413ded441cb144ddb5b24155aa5e50 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 2 Apr 2019 14:19:59 +0200 Subject: [PATCH 1/2] Something in Isabelle_DOF --- Isa_DOF.thy | 4 +- examples/conceptual/Concept_Example.thy | 5 +- .../MyCommentedIsabelle.thy | 61 +++++++++++++++++- .../TR_my_commented_isabelle/ROOT | 1 + .../document/figures/markup-demo.png | Bin 0 -> 13406 bytes ontologies/CENELEC_50128.thy | 2 +- ontologies/small_math.thy | 3 +- 7 files changed, 66 insertions(+), 10 deletions(-) create mode 100644 examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 7270595..c9cb959 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -55,7 +55,7 @@ fun docref_markup_gen refN def name id pos = if id = 0 then Markup.empty else Markup.properties (Position.entity_properties_of def id pos) - (Markup.entity refN name); (* or better store the thy-name as property ? ? ? *) + (Markup.entity refN name); (* or better store the thy-name as property ? ? ? *) val docref_markup = docref_markup_gen docrefN @@ -1434,7 +1434,7 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc else {unchecked = true, define= false})) {unchecked = false, define= false} (* default *); -val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.cartouche_input)) +val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input)) fun docitem_antiquotation_generic cid_decl {context = ctxt, source = src:Token.src, state} diff --git a/examples/conceptual/Concept_Example.thy b/examples/conceptual/Concept_Example.thy index 8085c0c..935f1cb 100644 --- a/examples/conceptual/Concept_Example.thy +++ b/examples/conceptual/Concept_Example.thy @@ -14,7 +14,7 @@ section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ text*[d::D, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, - ... @{docitem \c1\} @{thm "refl"}\ + ... @{docitem c1} @{thm "refl"}\ update_instance*[d::D, a1 := X2] @@ -35,12 +35,13 @@ text\ ..., mauris amet, id elit aliquam aptent id, ... @{docitem \a text\Here we add and maintain a link that is actually modeled as m-to-n relation ...\ update_instance*[f::F,b:="{(@{docitem ''a''}::A,@{docitem ''c1''}::C), (@{docitem ''a''}, @{docitem ''c2''})}"] - + close_monitor*[struct] text\And the trace of the monitor is:\ ML\@{trace_attribute struct}\ + print_doc_classes print_doc_items diff --git a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy index 4b4fa43..e6b3074 100644 --- a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy @@ -9,7 +9,7 @@ open_monitor*[this::report] title*[tit::title]\An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\ subtitle*[stit::subtitle]\Version : Isabelle 2017\ -text*[bu::author, +text*[bu::author, email = "''wolff@lri.fr''", affiliation = "''Universit\\'e Paris-Saclay, Paris, France''"]\Burkhart Wolff\ @@ -845,6 +845,8 @@ end; *) \ + + ML\ Thy_Output.document_command {markdown = true} \ (* Structures related to LaTeX Generation *) @@ -1158,15 +1160,68 @@ ML\ fun dark_matter x = XML.content_of (YXML.parse_body x)\ (* MORE TO COME *) +section\Positions\ +text\A basic data-structure relevant for PIDE are \<^emph>\positions\; beyond the usual line- and column +information they can represent ranges, list of ranges, and the name of the atomic sub-document +in which they are contained. In the command:\ +ML\ +val pos = @{here}; +val markup = Position.here pos; +writeln ("And a link to the declaration of 'here' is "^markup) +\ +(* \<^here> *) +text\ ... uses the antiquotation @{ML "@{here}"} to infer from the system lexer the actual position +of itself in the global document, converts it to markup (a string-representation of it) and sends +it via the usual @{ML "writeln"} to the interface. \ + +figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"] +\Output with hyperlinked position.\ + +text\@{docitem \hyplinkout\} shows the produced output where the little house-like symbol in the +display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above.\ + +section\Markup and Low-level Markup Reporting\ +text\The structures @{ML_structure Markup} and @{ML_structure Properties} represent the basic +annotation data which is part of the protocol sent from Isabelle to the frontend. +They are qualified as "quasi-abstract", which means they are intended to be an abstraction of +the serialized, textual presentation of the protocol. Markups are structurally a pair of a key +and properties; @{ML_structure Markup} provides a number of of such \<^emph>\key\s for annotation classes +such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample +from \<^theory_text>\Isabelle_DOF\. A markup must be tagged with an id; this is done by the @{ML serial}-function +discussed earlier.\ +ML\ +local + +val docclassN = "doc_class"; + +(* derived from: theory_markup; def for "defining occurrence" (true) in contrast to + "referring occurence" (false). *) +fun docclass_markup def name id pos = + if id = 0 then Markup.empty + else Markup.properties (Position.entity_properties_of def id pos) + (Markup.entity docclassN name); + +in + +fun report_defining_occurrence pos cid = + let val id = serial () + val markup_of_cid = docclass_markup true cid id pos + in Position.report pos markup_of_cid end; + +end +\ + +text\The @\ML report_defining_occurrence\-function above takes a position and a "cid" parsed +in the Front-End, converts this into markup together with a unique number identifying this +markup, and sends this as a report to the Front-End. \ -section\Low-level Markup Reporting\ section\Environment Structured Reporting\ text\ @{ML_type "'a Name_Space.table"} \ section\ Parsing issues \ - + text\ Parsing combinators represent the ground building blocks of both generic input engines as well as the specific Isar framework. They are implemented in the structure \verb+Token+ providing core type \verb+Token.T+. diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT index bf9d816..2952a4c 100644 --- a/examples/technical_report/TR_my_commented_isabelle/ROOT +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -7,6 +7,7 @@ session "TR_mycommentedisabelle" = "Isabelle_DOF" + "preamble.tex" "prooftree.sty" "build" + "figures/markup-demo" "figures/text-element.pdf" "figures/isabelle-architecture.pdf" "figures/pure-inferences-I.pdf" diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png b/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png new file mode 100644 index 0000000000000000000000000000000000000000..661566eb4f6cd3120c93dfb18381357a0f97b72e GIT binary patch literal 13406 zcma)i1#p~6&bBFrm^o%jW{R01W@i2-dwX|#yY*N7 zQ#I2sw7R87YPF=EP2E$Z*+l5QchE1POr$>4Tf$8F2tNRlq|JqXEy~leExEF`3w3}!d)4o zWTnseo9Yxg?5-zR3|GiUD0^?hei-m>se46ra4=z_;-)NZV&yG!6uj?x{wPw3TvCxz z30y*vbjlo|7x*D}V4n&vTx;pU>eF+wl)q2-^DQ+IJ14^Sqk%boM}fH%;RElFMT!0~ zl3vh1iNs~(*%N=mIUa#3OUPsiRc5IG$Nhyq`Pb#I=j@aF^|<7+4^jFsFf!!f5vp?t zPtJ6vDhX&a#HaB_{r#WIkuP{_J{cpkNMh2E#?Rgs)98--@dwD^eyfDgF~jIDLfFZV4;I zH-^|4-qE*KwS<)1ahyD?uy{k_xu6u935gKJWj&4oQrXe!NNLon(RFA8!5nf@;j!qk z?+JlJmdD0!mz(Z21*9yTq5);^g+pU;v-mx;Xnn{+(gV?)rvYuv*NU<5<`dOGNiH5opZNYu zCPHa10Nc;38$8GN9fqxuuR1Ya$nsO#;|9}>G}i_=&Uc8<8@W>m9{I&4#7^>Q#M*+j!@8%r-kOFDB z0d`~uqti_U6~N4l+V3wM^WLPJF?_>4$!}4QPz^y6z^(RfE`YZBofTwTx164!8H8B3 zge{g91i=PRGrX!CvMcms4<2&}F)UmT8AAVunom}!ru_sL0Ek#-a@)e2lCNLjBz z4RQ`5`%1YS{-|$lTR6k7&KA4bpX`D>BYJNe{(RRJvlHH?Uv69VBG^^%HT4r!3R(u7 zHx#4(dy;VGba}~Q;$vcb(hNTvCFD)SSaBn?lhCzupfrUE`W{*`Iw$HKnj8vm=xRSW zTBwn|O?0|`Dw@REf3*!p0{49CD(A$PGkQq7pvADcUDwO`x6Y5~?{1VlSOdw(X( z-&eGv@lH?+^JNXLjjPR^{@fyckb|IjQ+zuMWKT_wDE}$weJ6G^q z*Nll-^v_=w@b%ahs+ODMejLQ^$A^^Zm;Y352MxxYE67s(~(S{98=?H({rR?P92 zdnmbliq6?9#4bxNYSOZ4T6@<~^hoZ-`@-zy=Nx(9$CZeFFUw^cb{_7>^i^P=*+d>&(JZNDx0VYFue_YPzQ9{lSRf?GLN?F-lYEM^U_p zTcR-{Z4URhecr<2l6dp>1FacgA+QkAD3f!Ew!StqSMOTa`~&ZSpSU%tMf=3!>}A+vl1-#w20$kg#y!*PF2%^oO zKEM^w0EqUl2zb}S>z`dsu(){4f4oOhNm3glL}J73o$-)?o}*?aY^HAJk>ahUsHVIS zU|V)xe*Sp=3Of`|viGDI>wXN8yMCH{+@g##`P12<4?se87%D++{9hO&Fc_kuVjDs zEB0#o3Q6jkf;(=eZqyWW>@a~xN~%En!TaIp>d9E4mcU+EKzmI~4~+8|_#S4UDJ(e9 zFYssJnF-Z|fPB6xIgLg7Hk;{U2GzjkfZ+JR-sN87cwI)5>ssH#@q;EdF+3|)J!8F& zT5YwdLVvDycuBYe)>~`8(~mTYsxFC#!h-&CBL#`OCe-!0WQ*isNgMCIx7DPAd&P_C zTVuiz4#p=fO6oSXQw<%3S37Q>hk>)z&Z=i`Gm&3mw~0D*oK>WiapkQwJZ3kQ?CzFf z^Nv-S^^JA}mfDN0^GBwYUGglQ1|!gi&;vo0!~4U(B02C>fzN6brL8&yiXBaZ^(N|L z%QF5lsvIyj)(ZxW1)d|pME!y*OSm-+HFK4X26%Rwn~g)u@lDxJQ+q?L1eCnPE}ly? zi;E3(-tz}MXRWQPg>9;Hc{gE?Yy2~}j?Wm6N)7>1eRCb79lKB60t21vKC*8QgRjLe z6)>JiZ20y3Y7QZG#pS5x88Zv(3j;arq|Otc@qVOv+ZT4RYJrjqI9qXb2QV-! zir-&w2}SaAFfi~8^Dk_0A^@&}9R@M$Y zuKc8b^xy$q|9;FwO8iF`M@xQEH5qwgAsc&RVs=J0MrKlh_r%1+eD+2rJc`1if0Bdl z_({zi9c_7-m|R?37+pRx+Sr>iv2b&9GcmI=v9dCNdN4S+Sv%^xGFUs1{cDhak0WgC zU}$e{>u7FcP5gUYeFGaOM}AV$-xK}k^DjP)UCsYHleNR2Vu1u?`u&E9g^`)*KVySP z`F=m;kvDfWwo(%|2O3*DfaVb3Vq@m}qyInN{CCE`P^$lzlH-2}|MKEbLO!P7{QpIs ze}VPKQxIAL@A;VigFNU}ymKH(8TjVHa$i6##Ba@jK7^nz^`9;18XcZE`E>^j3~gRQ z81Tgv{8$?%0)GIlV(}xTR0uf=ASB`)Y_J0{Tr3L!DmD*{1cmq_vu|~gEA~245NY89 z3Ms5G+IlL&AlwMCJqj#|Fm!gb-umk4+UeQ+-kL7w=;`?N^o){9GP5ZTu~HGZbX=koNOmG2IOB2E6sgpOnz?9sqc%7mY=r;gPhj1v^0JmR91 z<}-)m>J`*uUO(DYD5kVRaRNS}pg=)^|Ft>90exCT+)D|fKwrVzDn4IwRSnl zG`9fu;pVez_?2ps3p4+f=8qBfZ(v==458_~V24p=Ny_<$9kXeSX*Ma$q)fw>Ud5-o z_R0@$^x(k$3d|oO%df+_G8n?pP4E;D(oFC?mmnS|u+vB(s>S8wpYSNsbU>TWwL5JY zsICJ6`RIRR*PS0?*nc*K{V2LRfS_D-b^g3@g!Ubc44x*h*{!ESjJua5D%k%@2<68k z)@?~xfkAG}qgWP|;GRD!igQyoDn_eVCAG9NC6PW$iRgfB{mqd_d(Sq+^&bpRrlX!y zM&TE8nD5V=Xcl3Rd!m=X6Ma>lBU6jxiKAJ{=P*y#vqf$Ouw9XsHj5Lpb((wn}8@m z@bM9Md6D8LZvI>&`IvgOj@I#E17?WUKY0FzDsLGBZF&QvmxE7%Mypr>P)s5#my#@t z9&Bu)I*1mWaomeAX0ISVsTm?v-2DeVF)W5~cRI7Z?<*8qxmairbOW?R%W?@lPV)>6 zMTw9XwR3zeu}oU$7mR#=`C*xVSVyrFRQm;4f`2|om6RDgT0))xl#rri%WBV0#>C-$ z8C*&k-NJDtcDgFH7>mZkuXcYM;F}e!EBZI$lF5!oao`Q&i8zgP2{}f7xqTg(g;F{j zo18X1R(`E=I0pIOmL4ob;-~I(E(^V;@JtPtubAQsOL(VFI2}JZwN4&Okp~);M(Ra! ziIsDM@}>Va=O+|uJP3D0v?M%zL+HB5CRSpacO~h;j;(+bgZUhK@m%7>3Kca#+i|Vb zX=z0TgNu$FmDV6}%hvZX^PwE{e$||2$wbW%sur=?<->xd-QDMR4HNdai{CDfXrc@m znp?{jb$wnE30*h9H99@Hz208#W)~Mz$#llJq&&VWD=BA-^D9@nx7)oPW&`DiQJt$t zob~g9gk`z?DQH%A&EXYi5=8P{+RE^&Y9tx!q0RRvbFK%lb#F!02T(^zS}O@?L%ECQ&%ePVr@yBhWdX20)6k|iPwe~O#_CjinyX0HVz9-a_}>4 zd*QA}n7W|Q=&{EOt@9F0FMThlA0XaU^oa+^71XeJit{IS#ky_h5Yz06yUn3uP?U?X zVo@|NQ_QGatU|#ndQ}1*ACIccC%*ysV|2T``3c&?V6+eb8YT)(q!Mu0?F_?ZeDe9M-U`ABrN7g2$qtw9<9@sq8qx ze>WM$d#dKlBE2f=mdfeYZI$3@j9vNp9j+&BWaOsMVaYQhz-HPvy03RY)>71hLh&w_ zym=M1fvV0OyDiCF>d+p$ZL!W&$-%(^d8bG=Q?hB@+atPJQu}&tT;a%GmF(^3_jq7e zEr_LThU~;~)$q$X(usm{)1JJ9{lPr1>nX7rmvyhAP|vF|&ibRuwm~wp)aCkEYNjhn zR!bgFo4}Xx12r{AMXdHtfV-9iF5I96W7bliqD%pK2-)Ir2jKA>%Zp`=awctg-i>!5Mb1TWGL z=eU~EysG1N+Ai^#B@=`1x-d%PKNzk5zcA8fa5B6Pxs1}g1oNYQ*dkHkZ9x?9k8IA=%w}vmW_9^0B`g8F;up7>j#0p4OYt4U8C7OYENB$uEjbu}REi<=IA&?x zj^eFfs3s@*Ffuio`tbl{R`YfM!NRKzLLL;1(x?B6*QkNRPk{5q?#&0Z!gBWaW zO-)TRD=iKOpyiNX)%h5Pi;HX4?F;U>9mzQzh^?cRq}^1Fbks1fGm}(*x9*eujmtm? z=^WzS<$_^!fn`-kQWV!#2r;!J+TIYS6$xLqpxlCA)J%1SrXZpqQ}@#_UDfD`tK))x z@IhnU(`nmNyoRm=VK3T`VARGJACQHZ|A?cg*YATKyK7vwmJ$j=$f+CWk-EctL2Rgg zCnCKki6uMKXpMN(_4dlk|9swe{VUyOI+)12_z8iT`yfAlzxAjxPf3pdCpp97)X)1( zNvsG0GpaI`idExE}29e+z`i zKD-Ny7I+ko9&jz<1&MOQySkgKD=S9el+YCtr`>1oI3vSp{^%;psMDSTjZCOjd#Qyo zXBmU07Ld@5OMXLy$8L5MTT4VELetj)+qks{VvV zsc^?yQ4Nqa`9DRi$Vx2WHA+5%f5d>Vd$9=UQ$-xIWj|UKi zd(M07#8x&mBu=WXd7O24E}Ct0`(5|KGpQw}CR4Y8l<`}6J#$h_9l}kk&Uh~`ck2-& zSw$%%ebVYB{$&?^iS%;(HyDwG{ArC=i)hrWgyVOsF1kITR7N{a7_)?sp--2)QUUkO z+bP*F^xZ={pXAT4zF$EXaN0fG!=|rK_DoGcZoQv^lZ@tj-N-$25ZJor7PL{Q(jGx8 ze6HpS&QYe0?BSAhqeR{xEWuXYhS`I$7d~)^>A@uW7N~b0>Tm8c?%GwjLQJdg)>F6H zel?yqA@D>WBF)H1-=PIPf-c>TOeCOXqh~*_?J~vCwDLIx!Fw;$#SG+L>+>}pt=9Tu zH5tS;6G;o`%tcD1#y%Kww&iPte`OaRQ%e4s=wI)4WwPY+_TrF)re?zo={*U6+1;wX zXI+nCYezi;**p}`bGBHaRY_k4-6Y26^}$p-V5UfJf<~uZazgOU)BUKT$q@thV?quj z5|?lFLS0EoXcB|wU_6Wflm~frdv^q<2|&LEm&5AA35feNG?StWAk6vYcC_Fjmz4#$ zarLa^5mwQ)lt&S#&g%jAYN-lij6V8{dW>v!{nqqPpA0kBF_VvXAx{|;i|6J z*3PdKU?RG_IG~9c&ILAQPzrPO4dr}`i2<8Qm z6elP6@Qw7Jic%NZf4%f~{p^_|U!F;N7D|;R&b&#cSKX(lcBn@N z@4EG1b%@0@m?G}G3yX#N9bT1=aQdMBw9U3n1Xpd1`C^k5qb!+uJD5)Wy!&LmtIK*` zZ6s6z^Q{Oy;uy4*b4KEEj%z^^x)G#yqNgw$7$w+6TveZSK1~N83ltL_zmn>+2b5VQ zpaddM?zZ>$kkMuu01?^)51!h!(glL;x1d#P?;kd52TJe+SM9YN)_{itKkxO8cAr6O zvhsoX`O8S`HdO4+dhg#sJwoC(lM({uE6dxsIom3#WpwL;S&UHDd6vV zosk3yu;)eB2%Hy4Ol9l=oJ5F9gr`HX%RxvJhDuEvsWV`2i7HVbo+ zu+-L^JzXG5#q8CUXpUNqr?3cNyNt2V@4qVo7+-b5H+}qA2vyJ!8m_@a-M1dC^~3)H zeccBDrkhd`f$mE1;1(r>?S^<_u$>|i%omsi*=&Q3@M7TU+b9u!#pNnofZhrg;oEKfKnoOG!xg&M}6n=0L@X*4w7da+~_sRGPLhNPyVzSOjInF zE%2E3b}kx@6Vd7Qbh-SvlHXH)2y!EH+XD0~YRBQ{AiLg6pvi)*bZ*xVKEclrU2yo0 z$eG$;Id5SJrqzugkRcjF|J+&T5J0d$@E3%;q4B*(Q0b9(Z##DR0teWnd3U`EK_Rny zHzafc0!OVcQPxDE^`=-PI05*L`{fU+BZoKS70a3rSl~$;o=2+B54}3UCCLWAt$Unn z8=)70q?fL$9nE8tp(?NXWOn111<3nsfS;|0^duyo?S~;x?zIaK1YBV!%BFB&6`oz$ z10V5|du~?}>0d8ftn3a4<(ly4GhEW$?by9PsB;S{JZ4x5APD}n-)a5|G<5yt31UJ6 z%9W+N3^M*cGBWb9JpqpvXC(gIJ!k}OG?x`*j7!@!g%);TJrZVnrMv?miLb@1IPsPsME50`!#=5}n!K9ZXkaHDs{p9E^(b`n@3;{ zU7+|~} zBJ_w5cs>`p<2%+noGrOtvaE7KJD9J^PM@2d-61@J(P!0nE97x($sfx0y2V)qdA`HT zwGNM&a`n3X)3&ohy2|F<07<2G0!G@+{-h3acj?N|xT&iSwiV}PASk9La*J0IoM(C0 zpw0w4V~O9A#qTjal_%C=QJ&3v`)#3~K8C%8Q5yP1TvHS8i$ax7$L!iuQA0z6kRooz zSN++@;2(>$;gwXf+WTBL+svb_8QxZHL{k3Xu2$Q=14h6jF!hZfZLXv?0>ZM)oplZpgLpn^i z_63sS$tdbET#e6{0U^<2(oG*|URgQ}_}QhnyvIQ-jq05)(|*|L+mq#k+hrTo6Rw%PKxLy)V~ewv@)lHlAlE9(-jHVC+Gc15#ZXcCZRg?Px zAjrdj|A5?T^@-A1#^}1XpTAKVt7^60&f{c}kF$r6a(m^j@v)a#Q-8Pd-{w1jOs8Wu zn$8)$=6NNPNN}y#ced1Q-mU$Bq&OyyfO!Fi<{@%SR>J?WN5W!ByR$-E3{Q3%f)K!i zUbv8B*A5E5ODjRS7^?fl0Jhf=zvOuSRL~E;n^~o6(Bh_Drc){Z21Drj4L#~^%_BO? z^HPFy^*U#+qkH2MQ5KT>6MU3o)^zt~V5y)P)aIqmwhN&OjQ6GZ#}-OS(TSl+mf?VL zxTs&Jt8IzqT$`GWRu=^P2)!zjtvd6CPQ`L!h!#a9oNlw8jV(|w0r1sd;qB=dYY0^ ziBqo*eyAI4yT_Vp4ipuxWiCCbd7N33K4xw=yAh+KHO?AK((MGYA8RV=?Ts^oCk>`o zD^MOO5f!g}G)gH9VuLm|c){6`mC{nfQYa=~vrVO?!>%04F`eHWH!59W4i?q(!dm#| zurL?7w;IGezffNqwGrYthlC~U9o&i?$z`yRiO=hJR6PB{wz(OKz}eR9dK8~APSzIn zxII1~Hk~%>Gjcv&0H9M!%kx}(Yj--DLwcMF0aeP5qF71l5{QP7h8xgd#?scs7dQKY zF~x?WiCn5AA%n}Ful)p+2auCh1@`&Mkt9Lj+Q`59LBf3L;F+PzcKd~+QLP6+!6-X$ zUlx06J1i|Dz45vEsmf+PO-`{lFB|LUe7Hh{$7!9PZrw_wXj1|K@(1aFo7`=<_=l?r z!2^(YQ<^cn`1Lzcn`1h$jVM99+MD1^3s~L!9Dt7Z5?oQc?|vQ-?(GE14m%6FXQy#K zn%w{54h3Pp{Gz6YXKVX-0^IhE%m=Q9Gg+tpX~FHgp$^s{f06zdfAMbzJPgDWOR1>* z{u^r*FOz9d@!_4G49(EYK?o$f-cB*?$jmX9now*2dwu2> zYJT2Wz23oK7!hE)DD38Jy{j(`rAySeL}6Tmg5G4Ns4bOki5iDqx(^njk@u`U{_yZ{ z_6skYUWA^0YglK&W=i|@wAA(U)dbx~SBG$Oy>ZCXR;MEjB%{MCm6`6GWb`3W(Z-%A z|6K322Zo5;U6V)|MyHL76NEe^{adEXT2AUm)7CM+5t8i}^G`yO9}URLB&aQ$iWH}}w)-yWlK50pwPop=l<&^R6xB)4X?zdjz7%7t%{ z{phf1BMP^Gl-0aA1)=}?8+`_eRR1Nl43G8x%Fu`=KD!BE!hmHResc#0Ff&~*I&SLh zN%5(d`nL-SB^#9m?SPx_x&~aQ*z9-2Zy>HR9L5!1n05LmviO%XIRs6|@q6FcI5sLh zVa(_D4U*=Gb`yQR?AVdNCQm47Mv*PoG<}`Q9~@LE^|B@tYZxi&F;sUnNb?uKB&X)d zL=w#&^cQ7!Io0A^&Yu$fp*Mz%%TlQK00gD*q|Yvm#W3(oM6JRe6rKu7=JW}^bV|!gye{; zcOvK_lI^OmKlLIA&qmZ^iM{BrYHrsF~qG!~?uFEChB}(R0{wJ#IIGl#)kgkv-Q@We8WR zPl_J6PQLCesKU5HX&g>x=)Woq?VS14nb0{otD?pY+<=|QcFr32D`DvJuy}iYIoxH{ zX$Pg;O^4i&T_V_8wtkOegEsN#<)gE*S}o1SJq{*!jxk)LE~o{2f+;%5d%lSLTq~S> zt>{!5#TP_KR~`4Gu+u0_aUwb&P@unp>wo%hGfoKY3Uv@fYE#;88^Y}QRe{`T^an!) zupOx=F@P;3!10z1o~DGE7y%Zt*Z1FztuyO4eDZsd0qMl|SK2!R;ufU@yfWOk3HJEE z@QA_!19m(CooFS!7`%)BJKG<3u!h8SF@2ufBh};7XoGQK_)|zxXmga9m&&t~v%Quv zbEVvC`opabSzO|)EzVHs|DN?v9wzxee5cRQ9_wjeE?U5J>lYWP*`8_C@|!2SXo|U1 zFWo~P7}ssD+{#;ULLPn>_%~`|1V>e9)_WwhIs9F>e%Nu;iN?OYn1qr1!lm7hj^$Yd z`FnFC7;UE-;r>$pMd?o|%9&$IDsXZ#wzoQAzU8Pj z>Dm7;R{y#~hD=>bB?}LUj;hH+I12^2sjK$e;uss<@Pv_4)cmCayaB)^iG18Y;My3~ zC$7_*LmWVWF_$MfMj1o8I$2O3-rFR;$mit}Z-*{X$z90gZeXN9{hMaLg6l$ag{_(q z@)=Bo?9G&jJ9~yWiMx%qZ0AA9)s)%rNjPwe3o#~NDJ#N-q777{Sx7Ly|BI4;Gp;@I z$plrb2J)-33#_-|69%s*H5R0lT7cuV+Q%w@hVB&7^hQqr==iIK@qY~DH|=VcpY&>m z1tFIO5r+lx)mRE@1|X97;`NK)VLG#aJpe!7S~n9y{vRMq>JwjCjhP`$%l{M@i7Hyu zZ_IrE;I#y>upGOF(AF`CFB+eO4bo)( zBCBX&Gq2`;dBrmhH+`x2_F?QYM{OYH`5$omeM|%ie2f?VE~+0a7}hej_L(VuOr9~? zcD)xn z!=K@$rKM)yV@SSeYs-L622_XiDU4xCG+KlnK*(un+wyb{RqP>=r7F@ZrsZVgw}(Rcw(T_2^T7S zapoQaq2Q{EI_iscpSOaO<)#@>4q*<8N`}qnj>t<1b00|rY4aQ(waLsgaVA@;$Yp^m zO&pGnCfCOj+^*-uz{T3Y-?8@7?MWUeb0~)GbJaOo?-Go}`4~hgmn98~!C@&1W?#v^ zxM7+VAql(w8JSMa5h%@7|+ zV#ou<`AHpMb*2-AO>6E_iV!4%fhrjCq zCrb?@>GXSWA0}I(ON*cmmD>6Ty)1>qEZ#-rG?yL9H{n6MfHK#5_Zy4Woj57af!yma zifz|e@=WPt_W1?#;a#&11g0^SprYw?7$%+BbiPEUuyo}-)B8st^AvgzBu5gHuB?-j zQ!DrSHs~yIIs)gT=T(Lp^ZSq~kunderlying idea: a monitor class automatically receives a doc_class article = style_id :: string <= "''LNCS''" - accepts "(title ~~ \author\\<^sup>+ ~~ abstract ~~ + accepts "(title ~~ \author\\<^sup>+ ~~ abstract ~~ \introduction\\<^sup>+ ~~ \technical || example\\<^sup>+ ~~ \conclusion\\<^sup>+)" @@ -158,7 +158,6 @@ setup\ let val cidS = ["small_math.introduction","small_math.technical", " - gen_sty_template From 0d96aeb494b0a701c3e27a843f0e4423587a9ff4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?= Date: Thu, 4 Apr 2019 15:43:48 +0200 Subject: [PATCH 2/2] support inner syntax cartouches to prevent an error for accent letters in attributes (see hol-testgen/add-ons/Featherweight-OCL/src/compiler_generic/Init.thy ) --- Isa_DOF.thy | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 7270595..9df3766 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -741,12 +741,91 @@ consts ISA_thy :: "string \ thy" ("@{thy _}") consts ISA_docitem :: "string \ 'a" ("@{docitem _}") consts ISA_docitem_attr :: "string \ string \ 'a" ("@{docitemattr (_) :: (_)}") +\ \Dynamic setup of inner syntax cartouche\ + +ML \ +(* Author: Frédéric Tuong, Université Paris-Saclay *) +(* Title: HOL/ex/Cartouche_Examples.thy + Author: Makarius +*) + local + fun mk_char f_char (s, _) accu = + fold + (fn c => fn (accu, l) => + (f_char c accu, + Syntax.const @{const_syntax Cons} + $ (Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c) + $ l)) + (rev (map Char.ord (String.explode s))) + accu; + + fun mk_string _ accu [] = (accu, Const (@{const_syntax Nil}, @{typ "char list"})) + | mk_string f_char accu (s :: ss) = mk_char f_char s (mk_string f_char accu ss); + + in + fun string_tr f f_char accu content args = + let fun err () = raise TERM ("string_tr", args) in + (case args of + [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] => + (case Term_Position.decode_position p of + SOME (pos, _) => c $ f (mk_string f_char accu (content (s, pos))) $ p + | NONE => err ()) + | _ => err ()) + end; + end; +\ + +syntax "_cartouche_string" :: "cartouche_position \ _" ("_") + +ML\ +val cartouche_grammar = + [ ("char list", snd) + , ("String.literal", (fn (_, x) => Syntax.const @{const_syntax STR} $ x))] +\ + +ML\ +fun parse_translation_cartouche binding l f_char accu = + let val cartouche_type = Attrib.setup_config_string binding (K (fst (hd l))) + (* if there is no type specified, by default we set the first element + to be the default type of cartouches *) in + fn ctxt => + string_tr + let val cart_type = Config.get ctxt cartouche_type in + case (List.find (fn (s, _) => s = cart_type) + l) of + NONE => error ("Unregistered return type for the cartouche: \"" ^ cart_type ^ "\"") + | SOME (_, f) => f + end + f_char + accu + (Symbol_Pos.cartouche_content o Symbol_Pos.explode) + end +\ + +parse_translation \ + [( @{syntax_const "_cartouche_string"} + , parse_translation_cartouche @{binding cartouche_type} cartouche_grammar (K I) ())] +\ + + (* tests *) term "@{typ ''int => int''}" term "@{term ''Bound 0''}" term "@{thm ''refl''}" term "@{docitem ''''}" ML\ @{term "@{docitem ''''}"}\ +(**) +term "@{typ \int => int\}" +term "@{term \Bound 0\}" +term "@{thm \refl\}" +term "@{docitem \\}" +ML\ @{term "@{docitem \\}"}\ +(**) +declare [[cartouche_type = "String.literal"]] +term "\Université\ :: String.literal" +declare [[cartouche_type = "char list"]] +term "\Université\ :: char list" +(**) subsection\ Semantics \