From 1358540a62eeaec73aa21b49dbd281a8f2ed05a8 Mon Sep 17 00:00:00 2001 From: bu Date: Thu, 16 Aug 2018 16:52:08 +0200 Subject: [PATCH] Simplified thy_output (cleanup) and set first LaTeX meta-args generator. Restructuring --- Isa_DOF.thy | 43 +++++++--- examples/cenelec/Example.thy | 54 ++----------- examples/math_exam/FormSheet.pdf | Bin 46926 -> 47217 bytes patches/thy_output.ML | 3 +- test/cenelec/Example.thy | 112 ++++++++++++++++++++++++++ {examples => test}/simple/Example.thy | 0 6 files changed, 151 insertions(+), 61 deletions(-) create mode 100644 test/cenelec/Example.thy rename {examples => test}/simple/Example.thy (100%) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index a8064a97..5762949f 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -382,11 +382,27 @@ end (* struct *) section{* Syntax for Annotated Documentation Commands (the '' View'' Part I) *} - + ML{* structure AnnoTextelemParser = struct +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) = + (* for the moment naive, i.e. without textual normalization of attribute names and + adapted term printing *) + let val l = "label = "^lab + val cid = "cid =" ^ (case cid_opt of + NONE => DOF_core.default_cid + | SOME(cid,_) => DOF_core.name2doc_class_name thy cid) + fun str ((lhs,_),rhs) = lhs^"="^rhs (* no normalization on lhs (could be long-name) + no paraphrasing on rhs (could be fully paranthesized + pretty-printed formula in LaTeX notation ... *) + in enclose "[" "]" (commas ([l,cid] @ (map str attr_list))) end + val semi = Scan.option (Parse.$$$ ";"); val attribute = @@ -408,7 +424,7 @@ val attributes = (Parse.$$$ "[" |-- (reference -- (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) [])) - --| Parse.$$$ "]" + --| Parse.$$$ "]" : meta_args_t parser val attributes_upd = (Parse.$$$ "[" @@ -444,8 +460,7 @@ fun check_classref (SOME(cid,pos')) thy = fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),sort)); fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init_global thy) [term]) -fun enriched_document_command markdown (((((oid,pos),cid_pos), - doc_attrs: ((string * Position.T) * string) list), +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 = @@ -454,11 +469,12 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos), 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 count = Unsynchronized.ref (0 - 1); fun incr () = Unsynchronized.inc count + val _ = writeln ("XXX" ^ (meta_args_2_string thy (((oid,pos),cid_pos), doc_attrs)) ) + val generalize_term = let val n = incr () in Term.map_types (generalize_typ n) end fun read_assn ((lhs, pos), rhs) = ((Syntax.read_term_global thy lhs |> generalize_term,pos), @@ -475,8 +491,8 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos), id=id, cid=cid_long}) end - fun check_text thy = ( let val _ = (SPY3 := Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks) - in thy end) + fun check_text thy = let val _ = Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks + in thy end (* as side-effect, generates markup *) in Toplevel.theory(enrich_trans #> check_text) (* Thanks Frederic Tuong! ! ! *) @@ -609,6 +625,10 @@ val _ = >> (fn ((((((oid,pos),cid),doc_attrs),some_name:string option),modes : string list),t:string) => (Toplevel.keep (assert_cmd some_name modes t)))); (* dummy/fake so far *) +(* this sets parser and converter for LaTeX generation of meta-attributes. + Currently of *all* commands, no distinction between text* and text command. +*) +val _ = Thy_Output.set_meta_args_parser (fn thy => attributes >> meta_args_2_string thy) end (* struct *) @@ -671,7 +691,6 @@ ML{* structure OntoLinkParser = struct - fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name = let val thy = Proof_Context.theory_of ctxt; @@ -738,8 +757,6 @@ fun check_and_mark_term ctxt oid = else error("undefined document reference:"^oid) end - - val X = (Scan.lift Args.cartouche_input : Input.source context_parser) >> (fn inp => "") fun docitem_value_ML_antiquotation binding = @@ -909,7 +926,7 @@ end (* struct *) text*[xxxy] {* dd @{docitem_ref \sdfg\} @{thm refl}*} - ML{* AnnoTextelemParser.SPY3; *} +ML{* AnnoTextelemParser.SPY3; *} text{* dd @{docitem_ref \sdfg\} @{thm refl} *} @@ -937,7 +954,7 @@ doc_class side_by_side_figure = figure + (* dito the future monitor: table - block *) section{* Testing and Validation *} - +(* ML{* local @@ -993,5 +1010,5 @@ fun set_meta_args_parser f = (meta_args_parser_hook:= f) end *} - + *) end diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index d5ab6cf6..df33e721 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -9,7 +9,7 @@ section{* Some show-off's of general antiquotations. *} print_attributes print_antiquotations -text{* @{thm refl} of name @{thm [source] refl} +text\ @{thm refl} of name @{thm [source] refl} @{thm[mode=Rule] conjI} @{file "../../Isa_DOF.thy"} @{value "3+4::int"} @@ -17,7 +17,7 @@ text{* @{thm refl} of name @{thm [source] refl} @{theory List}} @{term "3"} @{type bool} - @{term [show_types] "f x = a + x"} *} + @{term [show_types] "f x = a + x"} \ section{* Example *} @@ -40,48 +40,20 @@ to a test-environment or test-engine *} text \ As established by @{docref (unchecked) \t10\}, @{docref (define) \t10\} \ text \ the @{docref \t10\} - the @{docref \ass122\} - \ -text \ safety related applicability condition @{srac \ass122\}. \ -text \ exported constraint @{ec \ass122\}. - \ - -text{* And some ontologically inconsistent reference: @{hypothesis \ass1\} as well as *} --- wrong - -text{* ... some more ontologically inconsistent reference: @{assumption \hyp1\} as well as *} --- wrong - - - -text{* And a further ontologically totally inconsistent reference: - @{test_result \ass122\} as well as ... *} --- wrong - -text{* the ontologically inconsistent reference: @{ec \t10\} *} --- wrong - - + as well as the @{docref \ass122\}\ +text \ represent a justification of the safety related applicability + condition @{srac \ass122\} aka exported constraint @{ec \ass122\}. + \ section{* Some Tests for Ontology Framework and its CENELEC Instance *} declare_reference* [lalala::requirement, alpha="main", beta=42] -declare_reference* [lalala::quod] (* shouldn't work: multiple declaration *) declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] -paragraph*[sdf]{* just a paragraph *} paragraph* [sdfk] \ just a paragraph - lexical variant \ -subsection*[sdf]{* shouldn't work, multiple ref. *} - -section*[sedf::requirement, alpja= refl]{* works again. One can hover over the class constraint and - jump to its definition. *} -text\\label{sedf}\ (* Hack to make the LaTeX-ing running. Should disappear. *) - -section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting, -but wrong doc_class constraint. *} section{* Text Antiquotation Infrastructure ... *} @@ -93,19 +65,7 @@ text{* @{docref \ass122\} -- global reference to a text-item in ano text{* @{ec \ass122\} -- global reference to a exported constraint in another file. Note that the link is actually a srac, which, according to the ontology, happens to be an "ec". *} - -text{* @{test_specification \ass122\} -- wrong: "reference ontologically inconsistent". *} - - - -text{* Here is a reference to @{docref \sedf\} *} -(* works currently only in connection with the above label-hack. - Try to hover over the sedf - link and activate it !!! *) - - -section{* Miscellaneous ...*} - -section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *) + end diff --git a/examples/math_exam/FormSheet.pdf b/examples/math_exam/FormSheet.pdf index 174cc075613fc37eda72b4a2d170aed4f237735a..7cdcfca01cb32cedaaa798bce23f805a9a6ab8d9 100644 GIT binary patch delta 11076 zcmaia1yohp`?i3HG)VWQ8*g7ODcxPtjUp|bmqw+zbfbib2m;dG4FW14ARyonBOtBB zADnS!gx|Nm!&&R@^PIQ$yANwWYY%_L+}^@07rTxx<>csQ?dawT;Nq?nxo(c}UjQv~ zoeq8HCP8I8wj2iDzmn(}JWez}&W}q_rSi>Nm&GcBaf$znRmR{kVvt$cxSrqKfZM;> z zB7Wx(21J4g^R)zvy3LJ*HM86wSQwq*Jo;!AQaUUU7=(U6D$MhjTQM=fZ5b~&IW0GH zH*0{12;jDy>v>GjiwA6Z|qH!lO7z8Kx+XE;Bqzk2VPiTB!mO-tR1af-5y$-J6w#M zEFR#&1kcmG7=RG4e=sDPl!6saLPC0Vj?BrZZo+@gnwVJSBZ7+mJ&pK~zeNCIVrXG+ zI?{jZeB06-02BbDG3cqOwY{CK|2qd4??C4&m6*(Rc<2=X1$va1gaY|@gcmcUZ0&f@ z?LGhjtYo2ob)63Z{1rV21pgI29Q-$E2)L~vB_(O@YHbC8BhhbprLlFi8na)z>)CMB6a4Cip+|r0f}V|I)yBU#GG)(K zi1A5v6>QEpn?=F@NCuStR1`RBKKJ~>IN**zg_yvKs?Cn-ajCC@3 zTkqHlr!Vju`=)~*@mb?ZR&9HOV=e0Nk^O+;Cf+CYqw8Jb&DQT6N;|5@Ok4(NKRKfv zvKdi>6QNt!@m*9Bx5GEE-<^ppwZJx7T6T<82^;i|v+37(my?W=DCMz6S-NoAzcM@y zU3<$vL+q|9uFT2J+{fx7R79JH#T1dn7MoCBe!WIYxDTH23GK`}O=h*Xuy3N87-K2i z`I&$_3NjJ{Pm4|m?idDWGx$#)H*Z&x-G7QA&6d$}5`13tU`xaAI%N>e*>w*iVv6}z zf4Q;b3_9-J>s4`Xapif!i)2lG$Q5)dkq1$+Dju7w*Wj^?NBGf>y?98|3YF#wz4Ztu znq4OS2bvLnW;a&4f@X^dm&6%=-U-?vQy3U(NI0o2``~Aqz*IckBsDe7_QGedk);&% zv5`xdylibB65%r>L*Al*2l+x}FyyW9WiYKcfV6K|{smaAH(*F4n@1Cb4||ZZyV99& zyh6v7n7O3d6tr}mu@lD(Q*6{O$6QR6hwz|xx2oMye9k4mJ>KEqvk!Mm``awt_y=kw z;E&_|npz4is}$yy&XGW!Uee59DS1-VOUYmoep=})YUT$r(Ogf0nQ}JxK_#m5%v{U{ zL=2=lESo*zXtZ#UT3DuP!8zM>{E`=%ugysCu6x zvjn+ejYPAAFN!XoDVFc;ynjRfElDUVsd75D>J6Xq#{SeyG`uD@Ut@0Wy?vr^I$v^j z0l#7^OC@)-3Vue?%sSf8UM!_?Vx?lYDr_wp_qJ}k16+@o&tv4(ras@1QImsa#>W+R z?-*#(D_iP!AFAV<-zT0*n-(Zq+MyDg(BYP_ zklK%ovV*DEkGJvKffVum;$gf;dH1QNL)QC}<(-0u+QeJExI#a*xvEQ-dbHiydOT11 zWH=bf?~uVhqZh$p8O(FJ$FIg%s(wxU#K@U0d+QsE-YSca#OqF!!c!Hq3(_ zoB<00rVVCm2@GAR=0@ZPjR!Rx@tLTo*%-%iGc~ba1~)to5);HmMQm={b@#4K>h2eq znQWn$33zN1`{n&cWo>y21Zc-`waqD2I}Bz58@2=dGSXTH&DYXUAJg0iy{p5sda5g( zTx(pKj)?-wc=((_UMzNH5jsTbwDXwb3=Nl5+2jGbeK!x8IPv?KZY%5b8;0 z%0GV-UQRdlkRwvJL!mZAcU^4q+Q&)na`8h(Uy@TvUTY+53gfIjN%B@pgv}R$-lsay z%={``+n5RRA1JSnf+bp7nIbG^>-Gqzvg% zZq}dU0Lr#^!)@mXtJ>P31)+v9HFYx;eX>GbcN;!7$iK?c-}GR=Tgvz?-cDC^FFw9m znj^E^xS_ZDeuHUnp{&f#a7l`OnVb!6QuVGXa(E@-^Lv!zafG*w>t-zv7i1q?R#vH; zOj|=%_XIWd{O%lsmCk$p=lV90MJC<+9RTtuCEQ|6&p)!voQxjCzpK_Xbp0|W%R*)I z?x0&~J8wuYeEPcy+6s?`X4Stt8eIzg-W*j-qm|@W@vhc|>uj+`>a^y2(oF64geiAf zCQR}g55Z(1nd(#paN==vDNyeU}iMimntadW8 zn-ond-ulzF6GO6wmEabKJS6)^8#mKsfMK3&8=u@beq;3yP%0{L{r*%{DXk!l zlI$MwGWnLf5BPCgz0V@9jaF;|r@8c=w+KRAI89MlJM4+4&-1W?4t{mUht@=zc`x03 z(ki&$>_OI-iS&Z`>O`RURenG0)|Uee>KKVpN&SoxijNR{AR^0Q=D{g4u5956yc3Vr zTn>?}EX54>J$T8?r>V5jVi6~)Y9{lSQnVh265LPKzxKo!yiiITN+(IjDj8BN7r`q+ z-&Ziz*VxTCNue2LYEyyX-*gCgw9vlZ>HPK$(60jq67jyi$`u}oyJHo$fcm~ioeh41 zT1YUpxl7xo0w}s=z}@M*>TcmR{RX&E&k;V$DlZ2zl1-h(>sW4K?4Wo?oqak$FhYGU z%ZvMG6iJ89hsO(RcILG!>D0|G7nbdCccSq+ASluBd(jrPUsGtZMT0Z$3^P|%N)dc= z%c5>RGN69d!VxZdVOb;v=t~}sa-uQ6s~ESi=3i?$SdIU|-!j{iVtH5TG2#xlmNe5a zPF`eZ7l#Dl0ox#}KanS0CQH10g#yRxkq)8nTSU(u=neZ;?NWT>o1)y}%K7w6AUvSX zwH2)f+o1X*rI8l;OwpK0s%`hIsj7qG8*@&x&G*+NDVCi5%Ag(gjFGvn{kvm0lHAuk z)0=hlg?7^6Zba-h--B35-2(#0*`BBf{UBXU#80eDED;a>tc^d<@x|rA<027WVLhjJ zMG1)yjZX*8`os@9pyGNbtXXy>zQ#dEQ7PhBZ-Fvs_2-PJ%BTS5dy(V%u6aIy)6a)N zo;M!Mh<)(p;_e%klvQ7KcX_Q*{Wvu}Aw8jpw>Q>eMLbbo402EJhrhLL*lTk_wA$7^ zOs9=wpfh}{57B^y60UJM`ih14^eE=GN1kYCkBryiO*Qf*B?Ap&4Nz!A$&)Bez*|yA z3C+mDKT@4ajo3X$F&+gkWd+5SwUb(N^?q2_)S8^Jic;#P&dRkIU`o4Nm^+DpvGY2d zE`1I#=;hz6aew-j+i?_KUCf9wq&oH3S#)4R&VA1LQT0IQ zsB-ysvwV#X?4H!;EV*?D3M#3QyFrP)ufEVkQdgTi!{v;6v6ngB{@{Ixf+5)M=5p9# z+ai7kutZAMLsvUnN3Ddf`$f&_mxZ@dUQl)So3RY7_b|tauiMPORu^~OA}dUol3Jf; zu?3*Jycm_~QCWjYjIS9vi85hd+`ceZ`UKMESFg+$1cpyN%j^R9J7Bqnx5Vlel*&nq zuP7SCkX2=l4uupNmD&kgi@4jAKT2K<`#>(DRSrmL&Gd0GRn!yrEr#^(91`<8NTNb|3ex>vMKz?ECRc&I{lD4F^gkl&tShuGM14vPKp$2;j&PywW0y^RDf#sA z@Lg|LtEE~l6%%qNP}!T9af3~AJWIXkNcrd)D*<{$^GxBq*S-1nz^{v~NG|3=#T&cf zPnFZ}r1!B%X~btcj>cudN{tnllnolh*at}#uDMsu-yx%VH7=+gl}DEaUw3;>@8}R5 z?k9!2LWNrTqN4aZ`q?`h*4cE+M~^ABT9@zL--3}Y+jk7?mwc4?zN1dVutaHh;1^+OGn0MX&AG!;t<(X z-zqwyXNv`za#ZVCVPRx?pcUu<2Rx~df28gS#o`Uc^S?)l_#t21v4p~y!ZJwMkJ9uD z$<=qb74}`YdCVAEUt3VVjlT~O2Fy9S0U|KpCMncd*7X5thz*8K3Fw1z*;n^W&<#;=ADrP(bh#k=C8(^i$5q8M_ZCY+ZAEoZpW(DsTniJv4oSduuIo@SxuT+WBM~Yq2yq*HB9XEPbnVV+C&^OEGt3VVtx=v@p>>azLl&~4xLA45e%6hkZ zG6n=cxoxL?gllR4g<9A$DoeC`n8xx;%r__ctoX1S0jye4o9K^q@4Z2Ji zo8W?9xnLup5J3dGRaoeTlA5HFtZsq`H3qbjMq~v81NslG@z*OfNbIRD>@ury0bFJ^ z{-SsOrdmJ%1mdUC-_KwG;({?cC++^CVjutn67A&6S*b3bgT#QNx4bC$E)@Qvl#rl* z_>+HlCI}1y{s%>(LEdB-!1Gv{(QCpaH&mn~bhOpbe%{oWfNcas+u~|XgWSROhGsrn8Am( z;#0jC{^Fee76{CAL+kTPati)c?0F;c)M5fIE>r;m9GG`2Lv^0QKB@9#=ltR|1#(KJX0|*IA;yq-gw~ ze|%f1*hq}tDJcu2?C8E{Ic^E|cSV0M%Lyx+dKX(FCMPrYvPGH#dmQ`P&duqfiC9j) zhoXF`)Ky4}(ZISJuGlsamT4HWy`+bXD_?-)qe}a&z?Iq5oc2MsT1zgKI8hDRWih32 z=19~_=Mox6_xgAUTS*;@bJB@<0qEs|B#t2Ybi(G1UjMp5f_MFsw1> z(9`lx4r0G`Be(&KH7i_Bh_ie<^YE*POK=kN-JTnD1jvq)*DoLac+Mvq&*j<1Xc^a- z8JXZKhOqTX{(%_h_$snO<}$vGxhvSg0C7OA>@Ros=5ZZ_a?6$ve|CA8gIkil@ExDX z+1R?me>sTSou$8SwE2DM3Qq~2QP`@~t4>BO(!@w*-n#Y*Q)lnHq_cyQ&)=0UKUDrv z+jYMmcC--*%3sKC(o$ z9x1y>J(Zis#)!`s#KME88+eB?n%hio1*IOHCtIVv{$eLUhcuDDvfy(G6BY;;hxX%f zyNlKxt`zFGLUF7dQo)L z>s$5?IpZI`N}C#rnvSK&J+LpC(2FqIENq@;ca50PYxsFbG)R3_qHQdz8LD(3(JPwz z@bNz7w~wLWI_oFFNb;@jUQ%tJO)QUF&<&-yk(fJ_TA1{KheRu$>_Sbl$Ep6<(D9SS zvoR%SP0oB}l@Hn-Y$AAS9o*`uR*j{d1xCS}WeH+_HHcQhMwy3s)UsPmv2BWnw^^Q) zNg)~oPeYtB_B(7-Biz3;W0gMZ%Gnl+qej8q=QWrA#kn$NMtq zvoq%US?1P+Er*Jq#xaR@Io?M^H<6-WCO)D12M5p_G92_vU{% zQ=5dh#6|ShPO=g`PU$>wDW(PBOauP}d|vYZPQJsiO|w0+2xW;U4x6+i*>7tx`%wf` zS$x07dXOMd5xY?|Ga)r0SQ+_F%~Xya&kR}UGl>}sz$9}fJ-v~G9!Ly&KN_;D)`hoy zc84%pP|=pnoVtD2SoxV?A<9)+LQ#R=mRYzLZ6$t0p(9_KcRX=2fi=nOF!yL@l{SlVo}%PT%~8n}MaAu|>_W^HNPcOdqmBrzV>DBHvrxl}EL!YVyT1MtfFSFsYXw6*8V31^WShwcH|3(AV+Dz=GkZLSsG_(Y!r92lJ!(wKbMl zfC*OI?doyi)n#q&SK&Kb4o0OBW;h##h*tCM54$d2bb9?Z_773l16sXWJ5M3Q!&2%` zO73&i;p5?d`x9=**wSjz%`eU=JaB*Xo=twyYE^oo_u3L$l4ctiD$~09c|F*sjgp+2 z&eYVDt8{a$pJlmKeI?)EFZ*D!Jv$$$cL3&c|@#7nxhuUv9 zHX>!;mwjVBd!9m!N)6*qb4obc?DNC>Mv1Qr{6QdUQh6uXCPy7HLAH(EB%=ymkQGdb z%pB`pxbbG9{Mws5hT1mC(xnBm3a>IX;J4mq(beB2jU@+oT1GM)USC&_c%du4ud%d2 z0aTrYltpe%letRCsV_>>9b+=!-PBfpptMf1+o(6{bk@7&iE>Ha`Ln5wOZ|Plx}YX! zZHO<4kph9D=Kb4>(GE8D$PyMYEnE_Mo7>%5yy~?!_e)w0=p@_aKiX4^&Urbv zi8(?0QrS_VA{e{Gvd~DE!co(X3|74@JBFpAQ?MRc`dhA->AV1%g2$>aDS|?6j+j?1 zZM!rMs1F%!10t4?GHHlINA+Aj3Dz#Y{LeUzT~4Hf7}}`$7KMA31PKPmMYuGCosVjH zZomIewXLi3uJw~} zXEycVo7G38oOh!|>#?SA;q*88x;+&0J<9RwyYaX$_9RxnIn+A} zBXz2t-@oCEqI5n|tv(D>Fsci>=99$E()Gx5m)6EYpeJb;viYOuS>E&cdNZwI^UJ#RY$7-t@eR)+4V1gnXSE>W%8ZT5^#$uUaL^O zIgZc_N9=_aL&?Ke7s8HhshbHTCVNB7GeS5E)n#&C?ktW34+&)(3}n6jbddC#Ed^|} zu!o|s9?O3LG%{Ke$>02xb!Re*zcu>DR*+-b-_q})N6UA0m=vb2EsPP5ZZ=)oc)55H=x2* z{6^wCu{_(xK2MqgIT^@iHU(N(-M!c9Czyae75XJSS?Nw=f&EsRh3r}!P3ioqyzj~H zyX$98XIl?0H``6EwRQOJaH?nxrK^=>yh0r^Pbj~eS6d&e?^m>onAH!@%(nt`=2lB+ zqKGKX^6ld?ODjktuu#Nehk&YeFjcaiE?>nqJ~>V9$b=o$gQF+f?Y9G;$kd1Bh`D(6 zEUe3ea@h8?j&yXNsJdJW0?Da+kHo?PMc@Xp#H5{qs>$m zL@aat&sUM`?>>~khMLO{ET0#*z1I1ld~%?zU;H(uKWsVedz1x%TKsEZ$OnrTckgbq zHrp6w6pesh7!JMN{^RuI<-NBzp7;c@*qP8by_XS(_&~*K7C-LN6q2faWY3>GxvMjV zlGqRYTD%)VgM&|TcB26|# zD1_hQ$vA+Q)iB4hmrL>Xa8B7*ovD{ey8ZP4_B5A#np4)E#6m0Ot_b?ITh^K{!Zjry z7qCS_tY|mB7aYM0M8!+^k}Bhi{OS7K5FbP89@ zHZ?kY?Zu<_c)XVi`s6>{dwAU+JVtShnUQ6rtKTHoKs0CjX@Byobx2Fv;m4*o6E5$o zcZD2c9`AqSRs3c-R?+M>Ti@XComSY09Y#pZc-;5L_iW*T6hy;1UbJoD zt)k7o9)YGE`n{tKL%#5BvH1bUnd@69)jW*%{j$L|bYl&%DOI)jckKLK*J;b1i8Xq2 ziA;W^k@TP8@umiTF;D*btZ8vDM1;*N*tgH9?gxi=2HTl9Q#vy6V(0kp&i-PXC-`fh z41odv*(MAAIs(C^Vr~gg(*oQDfPmNnAcz1QJ^hLf6A45gyyBxpUhIM|jBrT{fq@`F zpdbhi0zwc#2wJp^L-oSQ#bKNC;~#EL4*|%FvlG9bZJivYFHXVyG;t29I9dJo`QQDh z*F$R?JRkrGM!znjqlSUN=kZ=#07n4c&jAnu2Ex%xWp3BuFoYo5sGJ>z1fB=>yAT+5 zu|vOvor9M#5b}RuaL74D@w@K%$(}2^KqTm=T*7M>)WzQak_HHRUVz^*2n2K$gI^FH zm*n8cs~7@)1%v+bf%;ELSkD{VE3j9lNMMSP*vAiQv^>V9*O<>USqFLCBR-!vwD`4G0MKyW?{+5D*xOx@-^* zx%klh?gWkipVNVtG3aFs0)~JtR{;bB!7n=ofuPV|(~0`^bvOsFE_?*!YIX>S;AO|q z^96mSG6?9E20jnwa?mIs2nYsVRz42~d=(RfU3LsQ@4?Fr41&Y1^a2QRp7Ny%f)Ee{ z1n_hH{o6DUF!;(kKF45}mCrH6CzfT3{T|$D*`aSINRsyX8zFa T=YKRP3=Bfzv9rsl$>RMVrVCc7 delta 10904 zcmaia1yoes_qK$9h;(ojFwg*8CJYn+ zmmM91NBY-I=QSb>6fpq@3j6vYj{9Bf^B?L4!6LekwitsL#0=DG|L1*P19%rF2d zh@J|yNKKA*peXx4Tggxkr1ch8r2zb@I9ilN#K~cRWV>5z1npr#3KgG>u40L40bXBC zziz&KEA7^GWeT^pM0IPN#C5YLewY{r^h`$hR!(=_J>0C!9WU;jE$s0j;Bzl7ZiEp3 zLJ-s`2`#FHnhNDkOorO0PQ=hbh10MhC3QdS9esLn6^qigf;y=V=dR8crU^W2Te^NA z6!<`Ksj6mGk0T(NtY()&V$iL7AfgBVD96lPeA^^UCxHL3An!eZu35$-FaNzxE1oQ? zZRL*+40irpb`DF1Zkicv(hREIS`0hcRMP19qV*VIQ@R=hnlY_T)!DPO>!TRoIbYd@ z!SyADjW0(5Mf@EF5DrFZ(2D;Tz2w)=IlqWjlUZCG{gI#p0|SD-MU{wg#u@Ovx<9*6*jd4O zKY;XuAkSYoFSIn2(Mgp~*ECwbt3drgeGmDn@|9@o$sqFP6jjuB8x!e_$yT3@wwe=q zO}Vp_H#HJF=4Y*#AqGes#s};TbV;{@akS`yc8B{o$53eu#wMnT+12Jw2Uc$^roK7Y z`m)QK&X=6daOFOO9psm)X(T{C3Tnx;Yh$$0ha4&#-vc$pMr;}}6b?_4iU;`r=6 zjXY|<48MWx_xcvEru|Z>*?8h>*waO&TClR)61IXLIy~_0<-(P_4s*qTFgy$#>`Ys` zqtH7d?<92p5u&YwxXkjQQCQaUskZK`0Cmbj`A`w(Xpp?gpiCb$H4`8<^y5`cf=Kw0 z_pC?R6){zJIhD)?nBOCp}7Jp=tFymsDt?5Ti z_hcRGijIA8J&Wj4yndOYB_s1`!A8-t2q#gPy{la#{aX_!mJBx)lNrfDn?B$!J9#1( zTZ+{z&0W`q{2NzwzUP11$Uiu;O5vVfE-f3LH&u5=lk>0eBd>bG=yvY~R`{#?6uU)M z8`9SQ~#ykh_2>~Ij-qa0XeWX+C3cFzGi{aF|q za8+39=iWEC*?LsA)(_B;He2F+L+m=bcc8^G>A6ik2Yqhh#6? zAwJ{jm|5BT8_NRIqTJr9w^Q#YZ)vCUeTpP#!g(qA<|C5H@xHTN=J;fVw5j3jCoqh%o9l}csP+uI!YDTUS(*0z@;(80 z#lBtXXL_{(P5;=Q*v z@T%lz)V)~d35gVkB^kBb;fq&YES|9eco>ppN18}=JAsHt2guvl>*Od-F~OHaymx{f z#UoPm3YSI|-UMUKz6p7UyGUR4##w33EJy}PJ*TzJfWQ{)Fzv&-tGu3qQy4w^qCxvc zJXU#H9SXQB5RiCOw4bz3Wrv^88!ovCz2dj{V(L^unXIAKw{Pxl&?d)sZmNST(C*E< z2U?TF;h1-#o-)EZr6Sr8MnTB7;!mVjPoVo(et@4!9&?rClF0GIv130-Yk6pg-Q$sh zogTWb;i)A6LZrqrgm<9Mf{$+uGb&(q75L+3gf)k}&6lxzx93np(9 zaW;_EwGq#2K+Z*5HSR z_dnSjyHcAfteRbHlIyn`uurzXwKgzlflRR=s$$~i@1Iw#Rr{RbD`UX^k}n{{und0? z0d}$tyFvVFUT*HpT$iDpaEbtDgG`$`Zx%PbBgsEbnl}_94wu zKsPGG*DMJwga_%(SqGor;d+tgXgyikxhdd9G}qqJ-;z6(ORXVIo=SceH}k=5$$E(~ zD?8P7s3qdw(L9mVF5uYh8?6U1kzM!?1YNj1aYsXwaGz9!p2R05$9+Oy9-XLXi}d~s zdKD!KYvCVd!k3+x1_I(vxTyOQ*QH$$}|q$9*Xb3Bo25WLs0 zv~t&m=Em`0%swPr7X^~b&MMI4y%Sc1hiH~G4x%c@NT|X;IFPC4$JQWeRwZfEOQ+hf z{vOe6Bp6YopChop+0_1);;RRTXk^&)uyt14Eeh|QRL0=AL{C2dUWrYTlV${x=3}PC zNxh{%{;oAxcj0B26Omxzl`V=5oEM$%gNl1^cN^o$xg|)wM;JXxp`*-&H88;Mlq8Ea zTcj-PM9E_K)QnI%S86%vFYftP4_QmBtJjW(2apT-O2?3S4X=?4-GU|SFoQ59vATJ78LCvVkpy*$0+Kq! zUrHpiws*+rt%_TVi&OHWV&NE>{vaAVi{)_=;x}`|fGKvIjn{T&|EbZDg?$d=j`2^xxx<^%;ZJQL| z(hrk;q_5mVZF^3+XE*D9128$Q66|^U!v#3IN%L*-9{%8nFndPi8lp3mKkzu)Oe*k9 z(xF(|3HR9(zp1#J`>ORpkRsm3Fx5iBleEzZ%6a_9h|NAqV@8SBm;%W8NXo~EV7|#M zx#!i=1=Kr-jGZ2XOVsZAEbmr&4BO8HI;TP<=u>7K4z5|dveLgM9N026dPLfwv6!JN zecLO6B`$H1vMgE}VAHeQ#-9e{Z;e^QG#Ul-;h&+ALLJGG4OPpI)Q(mJi=~F4m3!92 zCf-_jf{N0@*B9+$d=ii`+n-GtI-+e@jP{oBUXZ$4#w!5~^a#wq-jr-Ov?e~BCGU7I zU4SO8=uCSF>QHJG4&AU}ncZH(6I6N?dmCm^Ghl%y*eZhupCjlPfIjmUw>As)+%heMULw(e%Zo$t!_7FNsczDl9$tg6{?jMp3Pn?+Tt&Sxt zwX)Hjo-7Zvep~B0%XKo0pOH_m;D0~4$R?wADmlUWK?s2m`%atFkYVIisF2{0*Ej27 zV;v=#>VO>EKx=B%T=mV?gu|1S3N@b>(cS2Nwj3++p|f#fxmjH^pxof?<_#b5&rT(IOmm(Nb9Zl()9itqd^eM7--0^@PVZRXQ0PgGzfT z?x{|c zns&MTdzy(fei@6c?#gzG-P-N z^{2C3dtQb2xebfUFd|DKylKyj(vMdK;?{5{<>~B{2F7}*qJ|74k!7%ZU6@(;0Y#d(Ombp80yyQ~aIqP) z45HulawK=T7woltt}Bn*GyrYS>>y{2l^86`qaUxX?<~XT{oc>*O>7CgEMS*ly}6+{ zS@H61W~yC(rrwmxSuj&v*+$Dte>?QEiZ^N2ysq9%$WI>(ht(gyZtl{=+rkpxYFD|k zMQ%=OrZOnM?IjiXbtjSXK8EdqfZ@o8`pIzEjW8Tv;gFIzLn|VzWzoUifEu}s!1!=% zH5bA3oA>9Kos*Z47_4hTk(aAl_=Q4nQSO1E03fRAmN1j5zNEU6KA)6|CJ?|ZDC_Lx zA#LSu>1OBR;q1l?2chBv`Oy-$n=mjy7v&_*U)@oBQhB=n6u$qKlK<5Gzm}4apY`V7 zl_iiF{#W_>_cMqY4*Rto%nXO4?1H$^iqemTs4j+HxC(^8!O(w=KobMW`7TENYyv~U zpnsd-f1^+c;2#VIIro|Zwarg}G7BVTmX(*(l+`^CR!i%@qD7oXTaF1w{EYOkz9<)D zo*rE2rKlV<2aTxg zhK?6b1;}p^4g-o?`13AD*j*A;p5x_?Y;~h1t{b%T@+fBjBXWN~bo*gK7u7Anu+4|# zXQG>}9Gk7Jd&Y`4Ug(|V(60|HB^xDE%45A@?ZWN+!Vnv}K5}!G$Wv8fke!F6kIhxM zm@XHKDcnzVTYL(**XWwq z#78o-EX5<&%vR#p3vPkJdj?JK+N4PgAA+au1+t6}YaIH6^fe0_CDzRMS~=$|#1-6Z z5gve8MS8GALd|S5-*nt}-=VJ@M+xh*B3b1sd8Ivre51&wp=h+!PN|cGdc^bTDi zz&$W`JS){>A}f8JDq%CGfOoH8b8?XEDJun9J>N^gSylO+Rm&sEK7}u18}h0PxBahh zE@Hhr)L;HsFzOOFsLZ!{`0=wGFa5Nagj4)3AN`yi#nZzYUbI*_KQwut&XlAM4}Sga zL;7|eL?}73otGVNB=7cEBuSp`SVSK8x1GNCr08{Q#t_oHr8guR9J_%hV4+5`Z`!>_ zV_;S;5NpK9>4K?U6|403oi`fUc?oXH6rAmO#<~6~0s;%bukYar%6sm$}C2BR~Z=(G7$- z8!EAwK7Fe%Wb-58aH4R?>G9BFHZDxb82p`fa7H{r)Y{)N9s33*Xt9xP8o=w&~A6tC)NtXPv5r3ZJz?uO*R7 zNzC3LYBN`F#~5X(ymHv_tRX4q^N|br`>wlbNM%1k+`y8Mvo^DB727Zg%_EpM#+Pu$ zH=5ZL#8M*yHMsEjn+fl+4MUJYk?MG@4_2N;7<>+CUm$B|BhSWiUu34wJ3e~^D+-Us zKNa$(lulD|bjt0`Y%g6f2iy`)lDz3t-=d9{++A$Nw5L{SCHXbJNLSK*Qa2Ig=Qw(NEQNKyQF@3|2L|3 zbcF)6Z?9>aQ@(C9n2mU`6X>6r{%X)_Jsmld<~b--7nVI-VKcw%wB&n~ePW_>XF+mX zdV6WXF5+DNqnT*qq@BC&g8#acs8`c4(zfU6ov7>Fo(ovYOkaA$izvVEkh>F0bPaFc zJ4slixk=WENQYTdxkvZ}`(zt;ydOTz`H}RpP30p^pu|~YzkolrExrR$Gh-I5DA@_} zQQaMqG6=X(9qW3#QoiFu9v9r$4?K$Db`v-Y9Ny3*@lI*#(5;B8x3Ib`33atf+c&Cc zQWrYCvqt-fQ=$n}u=B0=mFZEvV?dQb{Gta!LmrjaHrc%>MdHMi*C-B+59JQ!9EOA=%tVO+`n>VD)CBqt=|Zmb=9JkrnaiTwS$nbk-=hJ5OCy6hT*=Pv7FpjuH8| zY8e4KL)kj+gJyDCEzP{dp^u7+og9TDi6v-qDOcI1E=P3l^F{|siPxFNYR7W|nLVsT zVf*Xxfok$ZTyyq?_>}ckT~-NI$dL~z1Mdul=VB{jJT_4ggetO4)vofyMG*c@f-Tv1 zX69j<9XESsjGU(LvSnM8&3!iJpL|_${{?B8F40jhv^eLuSKgGBOm!;P*uk*5Q}DJ{ zexA?DPRwTlx3+bTEzolBu zyTL!kj~>?&{5U~EjNe@tsvRtHqFMI`uSF3NQ3aP>e55C>iF?J zE!Zj__7CadWk=&jay5y{cOs1>y{&r*%4sG9_72lc8uPz^Vkjp84c&zmCbc}``=q=F z>POwGbDj__Z4(=`hsl$A&wR)2XH|?_5pq_O##cB>l=oK+5=Q*=o%Kvoyl6e6M<((H zo&9W8`|4=s^bozeB^rQ%k$ueP<@NoPL_({RcYO<)#%d45BF<}U9Ay1*d-9lEtH$)h z>)crt{Iwhc>yKk%JlvG46JbJgnzCZ4Jomar?bfmy8{TSK+vRq>nwAo}>YtsXY*AT} z;~hd*BG-oklpc%bY?Ndx7c!Jec8Q3Mb&MuZauYRz!b{Y3gUuIn+xxVzKnzE0=?D zfRVcnfvLpB%(bCMz7H3tTNyjuy8%XD2MFc?QJJ@1bJV~?satkvf&OpLdn0uS{A3dz znR_#uA952Q=SBM~lbAb`zq|A_I8s#{b&HdwNxQaN{lB-`CxW|z>{J!rHIf^UEbLD1^JzDMk59DFq>G0xWh{{*38{yRje)hWox@rL!%)jcb0B@Z|Gm(b5Z|Sr0McmZ^t_#Eevnk!+$G@q%_T zV$xm2j1{~f#b9YUZ)}B|8F`j1wJEczxXk#8_i?l&S}^63a+yt^E2)^fqksZ5mL4Hd zH<5SU(nBof_mj$Mu4={MQkn%$n!bseaQ3p?>@p0X8-7mM{B`L^u$m;b{nYs2l^rGw zxq@ZKQZagWvio!>B@qpJ{{!`%9;wu8P@RpI(H@H2_r!Vyc=e9eBRo!Hs0I;6N`gyY2z$xB7D5VrNugwmg6(~dpoNvqO>K#p*@5P;NWyzO!W4h zlE;nTu4(mc=6X6NK;ru>M2R>bAyt6G<4swxYfC-@!BH3 zr7l=#XkPBw=mc9HlRL-Fo@)lGtIM~wDkf@)sBu+^C`L3z&oV-6XemFDrUg@dE%Z1* zQ;Fn@#+_9rzNEHS%G=@GBWlO?HY)8~>2JvVW~IP~g0nlfJH{XsvTO{jkCCx!@JO{x z@3f!q5Y0Z05t_i=`a z)&&T19+Fy=-c@(z?k~7jkj@Vxr&wFVxiPH|o=}R+Qn)u+97@AV|Kt%Rz3qn%Pg>k4 zphx~&>ukd0&hnu*@y^`sCn3m_W*(lpYc=m23Jl!|fFmKiq&lCNtF0XaT9A85LUVNA z`?VTurbcU58@^2+R~OgADFhzbun80%Peas1NfvZ_g z>c!jnE@XM^65xR(OnY&TK5-VAt7TXS-9c7iQb%jtS2MAMpVXO~Kx-)uD$K7nS7q-C zW#j8NS;)*Zrz1LX9`zvyVq>F+hG;ldIX-b%I=!ZVsA||2XkD|2heg>|ns2TQ+cQ`V zdx#zF2R;zv1#(Ql1BOiIHSXij^Oe6!BWmSQ6EqBvTiBW}w3y`+QPkZsu7AO>Ly}TO z{vKWCXuK9CXK3nEjDU_d9I)0b_XJ$kcSR?IULT=cbzN+%_h1 z2fU56tDA;3lTXdkkxAnn6_#7p`YEc`4bt!4X!Ccn(-Pm7VO;Rhe&m2SRq?Hjsu6l) ziCD3F&rZHVo6Y&IEoNM*=uNj-L7}M_qS}w7Iab&ysP3l8bQ?}J+N_q=aX);}eqWrj zf%@BFTthta%V=PcpDoV|Kxp*)@=Y26)FC_FzU?bg{p1;}QW$Cakc@sNPk5`6%`@7U zx#1+yQPtJ?Ze#$bf{{;WP2YZm2a7eF($~@>qBj}`+h9h+L_ZMwDC}FD$YL$|hfu6Y zx2N1VP_W_#A8!^#%hKnTI*#b(T+&>?T$BQ@{OXzh8_DWNp9B(Lvg69H9^7~y-z>Mw z(RaT+A=-m_oP__QLk}YJG!p5|^IzRc>0@a8R_B>&H0&@3k?i$aS-I6XFF#n zX>$)N=AToXgDTEp2>AJ|7ZU$L{5_WkSAn20sPypbPt5EQTxcK|jP_WP?3asdVh|7Anr7lL4L=q1BIDD+%L z``yU7K6ow_{((VJENC($h=RU7ir~ zUl{mTBR_3`L6_Gb7>b0Q@12Y5msJnF*iXM>AUOPTba2R})PdpWGyO3Z0)SpxO%T9^ z%zSDuayzIb$%Tz<4;7cr=Z{JJKoa?lIVn85J=r?A5@{fRk{_F@Af`R|cI}iv0 zU+M=0TpXsmxc{29PAOP?mEL?gqf`OoajQr0A5DNO8)pP#A zLeNXwH)bFZ z1o)R#?cru_=V0ab^N607ov+o!S7p1N#S8?6K@b)I7{Uq$gPDWP5f)%8E08q+0J;k_ ohk_yE_@e*cF3iT~M;GzkJ fn s => ("",s)): theory -> string parser) diff --git a/test/cenelec/Example.thy b/test/cenelec/Example.thy new file mode 100644 index 00000000..7b663a23 --- /dev/null +++ b/test/cenelec/Example.thy @@ -0,0 +1,112 @@ +theory Example + imports "../../ontologies/CENELEC_50126" +begin + +section{* Some show-off's of general antiquotations. *} + + +(* some show-off of standard anti-quotations: *) +print_attributes +print_antiquotations + +text\ @{thm refl} of name @{thm [source] refl} + @{thm[mode=Rule] conjI} + @{file "../../Isa_DOF.thy"} + @{value "3+4::int"} + @{const hd} + @{theory List}} + @{term "3"} + @{type bool} + @{term [show_types] "f x = a + x"} \ + +section{* Example *} + +text*[tralala] {* Brexit means Brexit *} + +text*[ass1::assumption] {* Brexit means Brexit *} + +text*[hyp1::hypothesis] {* P inequal NP *} + + +text*[ass122::srac] {* The overall sampling frequence of the odometer +subsystem is therefore 14 khz, which includes sampling, computing and +result communication times... *} + +text*[t10::test_result] {* This is a meta-test. This could be an ML-command +that governs the external test-execution via, eg., a makefile or specific calls +to a test-environment or test-engine *} + +text \ @{ec \ass122\}}\ + +text \ As established by @{docref (unchecked) \t10\}, + @{docref (define) \t10\} \ +text \ the @{docref \t10\} + as well as the @{docref \ass122\}\ +text \ represent a justification of the safety related applicability + condition @{srac \ass122\} aka exported constraint @{ec \ass122\}. + \ + +text{* And some ontologically inconsistent reference: @{hypothesis \ass1\} as well as *} +-- wrong + +text{* ... some more ontologically inconsistent reference: @{assumption \hyp1\} as well as *} +-- wrong + + + +text{* And a further ontologically totally inconsistent reference: + @{test_result \ass122\} as well as ... *} +-- wrong + +text{* the ontologically inconsistent reference: @{ec \t10\} *} +-- wrong + + + +section{* Some Tests for Ontology Framework and its CENELEC Instance *} + +declare_reference* [lalala::requirement, alpha="main", beta=42] + +declare_reference* [lalala::quod] (* shouldn't work: multiple declaration *) + +declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] + +paragraph*[sdf]{* just a paragraph *} +paragraph* [sdfk] \ just a paragraph - lexical variant \ + +subsection*[sdf]{* shouldn't work, multiple ref. *} + +section*[sedf::requirement, alpja= refl]{* Shouldn't work - misspelled attribute. *} +text\\label{sedf}\ (* Hack to make the LaTeX-ing running. Should disappear. *) + +section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting, +but wrong doc_class constraint. *} + +section{* Text Antiquotation Infrastructure ... *} + +text{* @{docref \lalala\} -- produces warning. *} +text{* @{docref (unchecked) \lalala\} -- produces no warning. *} + +text{* @{docref \ass122\} -- global reference to a text-item in another file. *} + +text{* @{ec \ass122\} -- global reference to a exported constraint in another file. + Note that the link is actually a srac, which, according to + the ontology, happens to be an "ec". *} + +text{* @{test_specification \ass122\} -- wrong: "reference ontologically inconsistent". *} + + + +text{* Here is a reference to @{docref \sedf\} *} +(* works currently only in connection with the above label-hack. + Try to hover over the sedf - link and activate it !!! *) + + +section \Miscellaneous\ + +section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *) + + +end + + \ No newline at end of file diff --git a/examples/simple/Example.thy b/test/simple/Example.thy similarity index 100% rename from examples/simple/Example.thy rename to test/simple/Example.thy