From 44bb8968da104e49b3765b18aa54f62870f88c39 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Sun, 20 Sep 2009 23:33:29 +0000 Subject: new mpost package drv 0.93 (20sep09) git-svn-id: svn://tug.org/texlive/trunk@15388 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/metapost/drv/drv.mp | 2245 +++++++++++++++++++++++++++++++++ 1 file changed, 2245 insertions(+) create mode 100644 Master/texmf-dist/metapost/drv/drv.mp (limited to 'Master/texmf-dist/metapost') diff --git a/Master/texmf-dist/metapost/drv/drv.mp b/Master/texmf-dist/metapost/drv/drv.mp new file mode 100644 index 00000000000..5eb38396144 --- /dev/null +++ b/Master/texmf-dist/metapost/drv/drv.mp @@ -0,0 +1,2245 @@ +%% drv.mp 0.93 +%% Copyright 2009 Laurent M\'ehats +% +% This work may be distributed and/or modified under the +% conditions of the LaTeX Project Public License, either version 1.3 +% of this license or (at your option) any later version. +% The latest version of this license is in +% http://www.latex-project.org/lppl.txt +% and version 1.3 or later is part of all distributions of LaTeX +% version 2005/12/01 or later. +% +% This work has the LPPL maintenance status `maintained'. +% +% The Current Maintainer of this work is Laurent M\'ehats. +% +% +% This work consists of the file drv.mp + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% User's macros summary +% +% +% * Judgment & inference declarations +% =================================== +% +% jgm +% judgment index +% sub-judgments math-mode LaTeX code +% +% nfr () (, ) +% inference index +% list of premise indices +% inference label math-mode LaTeX code +% inference line style identifier +% (0, 1, 2, 3, 4, 5, 6 or _) +% 0 none +% 1 simple +% 2 double +% 3 dotted +% 4 dashed +% 5 waved +% 6 TeX-dotted +% _ default (set by drv_path_style) +% +% mvd (, ) +% index of the origin judgment +% number of phantom steps +% phantom steps path-style identifier +% (0, 1, 2, 3, 4, 5, 6 or _) +% +% Nfr () (, , , ) +% inference index +% list of premise indices +% inference label math-mode LaTeX code +% left delimiter label math-mode LaTeX code +% right delimiter label math-mode LaTeX code +% inference line style identifier +% (0, 1, 2, 3, 4, 5, 6 or _) +% +% Mvd (, , , ) +% index of the origin judgment +% number of phantom steps +% left label math-mode LaTeX code +% right label math-mode LaTeX code +% phantom steps path-style identifier +% (0, 1, 2, 3, 4, 5, 6 or _) +% +% NFR () (, , , ) +% (, , ) +% inference index +% list of premise indices +% left inference label math-mode LaTeX code +% right inference label math-mode LaTeX code +% left delimiter label math-mode LaTeX code +% right delimiter label math-mode LaTeX code +% junction style identifier (0, 1, 2, 3 or _) +% 0 fully-interlacing +% 1 semi-interlacing +% 2 non-interlacing +% 3 user specified (tricky) +% _ default (set by drv_junction_style) +% alignment style identifier (l, c, r, u or _) +% l left +% c centered +% r right +% u user specified (tricky) +% _ default (set by drv_alignment_style) +% inference line style identifier +% (0, 1, 2, 3, 4, 5, 6 or _) +% +% MVD (, , , ) +% index of the origin judgment +% number of phantom steps +% left label math-mode LaTeX code +% right label math-mode LaTeX code +% alignment style identifier (l, c, r, u or _) +% phantom steps path-style identifier +% (0, 1, 2, 3, 4, 5, 6 or _) +% +% NFR_opt () () () +% (, , ) +% inference index +% list of premise indices +% list of inference labels math-mode LaTeX code +% list of delimiter labels math-mode LaTeX code +% junction style identifier (0, 1, 2, 3 or _) +% alignment style identifier (l, c, r, u or _) +% inference line style identifier +% (0, 1, 2, 3, 4, 5, 6 or _) +% +% MVD_opt () () ( ) +% index of the origin judgment +% number of phantom steps +% list of labels math-mode LaTeX code +% alignment style identifier (l, c, r or u) +% phantom steps path-style identifier +% (0, 1, 2, 3, 4, 5, 6 or _) +% +% * Tunings +% ========= +% +% drv_font_size +% LaTeX font-size command +% "\tiny" +% "\scriptsize" +% "\footnotesize" +% "\small" +% "\normalsize" +% "\large" +% "\Large" +% etc. +% +% drv_math_style (, ) +% component identifier (drv, jdg, ilb, dlb or plb) +% drv derivation trees +% jdg judgments +% ilb inference labels +% dlb delimiter labels +% plb phantom steps labels +% LaTeX math-style command +% +% drv_scale (, ) +% scale identifier (clr, prm, jdg or ilb) +% clr nice explanation soon (see examples) +% prm nice explanation soon (see examples) +% jdg nice explanation soon (see examples) +% ilb nice explanation soon (see examples) +% scale value +% +% drv_junction_style +% junction style identifier (0, 1 or 2) +% 0 ``fully-interlacing'' +% 1 ``semi-interlacing'' +% 2 ``non-interlacing'' +% +% drv_alignment_style +% alignment style identifier (l, c or r) +% l left +% c centered +% r right +% +% drv_path_style (, ) +% path-type identifier (iln or phm) +% iln inference lines +% phm phantom steps paths +% path-style identifier (0, 1, 2, 3, 4, 5 or 6) +% +% drv_labels_position (, ) +% label-type identifier (ilb, plb or dlb) +% ilb inference labels +% dlb delimiter labels +% plb phantom steps labels +% position identifier (l or r) +% l left +% r right +% +% drv_roots_position +% position identifier (t or b) +% t top +% b bottom +% +% drv_axis_reference +% reference identifier (iln or jdg) +% iln root inference line axis +% jdg root judgment math-axis +% +% drv_left_delimiter +% left delimiter math-mode LaTeX code +% "(" $($ +% "[" $[$ +% "\lbrace" $\lbrace$ +% "\langle" $\langle$ +% etc. +% +% drv_right_delimiter +% right delimiter math-mode LaTeX code +% ")" +% "]" +% "\rbrace" +% "\rangle" +% etc. +% +% drv_box_mode +% status identifier (on or off) +% on +% off +% +% drv_fraction_mode +% status identifier (on or off) +% on +% off +% +% drv_proof_mode +% status identifier (on or off) +% on +% off +% +% * Derivation tree pictures +% ========================== +% +% drv_bbox +% sub-tree root index +% +% drv_axis (, ) +% reference type identifier (iln, jdg or dlm) +% iln inference line axis +% jdg judgment math-axis +% dlm delimiter axis +% reference index +% +% drv_styled +% MetaPost path expression +% path style identifier (0, 1, 2, 3, 4, 5 or 6) +% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% MetaPost messages formatting +% + +% drv_format prevents messages from being automatically cut into lines every +% 79 characters: if possible, a word which would otherwise be cut is 'pushed' +% to the following line by inserting space characters before it. + +vardef drv_format (expr str, fst_len, nxt_len, dbl_pcs)= + % str: the message to be formatted + % fst_len: first line length + % nxt_len: following lines length + % dbl_pcs (boolean): occurrences of the percent character must be doubled + save str_len, sub_len, aux_len, chr_rnk, occ_num; + numeric str_len, sub_len, aux_len, chr_rnk, occ_num; + save aux_str, chr; + string aux_str, chr; + str_len:=length str; + sub_len:=0; + chr_rnk:=0; + occ_num:=0; + aux_len:=0; + aux_str:=""; + forever: + exitif (chr_rnk=fst_len) or (chr_rnk=str_len); + chr:=substring (chr_rnk, chr_rnk+1) of str; + aux_str:=aux_str&chr; + if chr=" ": + sub_len:=chr_rnk+1; + aux_len:=sub_len+occ_num; + elseif (chr="%") and dbl_pcs: + aux_str:=aux_str&"%"; + occ_num:=occ_num+1; + fi + chr_rnk:=chr_rnk+1; + endfor + if chr_rnk=fst_len: + begingroup + if sub_len=0: + sub_len:=fst_len; + aux_len:=sub_len+occ_num; + fi + substring (0, aux_len) of aux_str& + for idx=sub_len+1 upto fst_len: + " "& + endfor + drv_format (substring (sub_len, str_len) of str, + nxt_len, nxt_len, dbl_pcs) + endgroup + else: + aux_str + fi +enddef; + +boolean drv_inside_fig; +drv_inside_fig:=false; + +vardef drv_context= + "drv"&if drv_inside_fig: " (fig. "&decimal charcode&")"&fi ": " +enddef; + +vardef drv_message expr str= + message drv_format (drv_context&str, 79, 79, false); +enddef; + +vardef drv_errhelp expr str= + % Occurrences of the percent character must be doubled: errhelp makes single + % single occurrences behave as newline characters (this is inherited from + % MetaFont). + errhelp drv_format (str, 79, 79, true); +enddef; + +vardef drv_errmessage expr str= + % errmessage inserts the 2-characters string "! " before its argument. + % Hence 77 as a first line length argument. + errmessage drv_format (drv_context&str, 77, 79, false); +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Delayed LaTeX processing +% + +picture tex_pct[]; +string delayed_tex_file; +delayed_tex_file:=jobname&"-delayed.mp"; + +% +% reading LaTeX picture definitions +% + +boolean drv_nullpicture; +drv_nullpicture:=true; + +string readfrom_str; +readfrom_str:=readfrom delayed_tex_file; +if readfrom_str<>EOF: + closefrom delayed_tex_file; + drv_message ("reading `"&delayed_tex_file&"' LateX picture definitions."); + batchmode; + scantokens ("input "&delayed_tex_file); + errorstopmode; + drv_message "done."; + drv_nullpicture:=false; +fi + +% +% copying LaTeX preamble +% + +vardef drv_read (expr search_str) (suffix accum_str)= + save readfrom_str, readfrom_substr; + string readfrom_str, readfrom_substr; + accum_str:=""; + forever: + readfrom_str:=readfrom jobname; + readfrom_substr:=substring (0, length search_str) of readfrom_str; + exitif (readfrom_substr=search_str) or (readfrom_str=EOF); + accum_str:=accum_str&readfrom_str&char(10); + endfor + if readfrom_str=EOF: + closefrom jobname; + drv_errhelp ("`"&jobname&".mp' should contain a line starting with "& + ditto&search_str&ditto&"."); + drv_errmessage (ditto&search_str&ditto&" is missing"); + fi +enddef; + +string tex_preamble_str[]; +% tex_preamble_str[0] from "verbatimtex %&latex" to "\begin{document}" +% tex_preamble_str[1] from "\begin{document}" to "etex;" + +drv_message ("reading `"&jobname&".mp' LateX preamble."); + drv_read ("verbatimtex %&latex", tex_preamble_str[0]); + drv_read ("\begin{document}", tex_preamble_str[0]); + drv_read ("etex;", tex_preamble_str[1]); + closefrom jobname; + write + "%"&char(10)& + "% AUTOMATICALLY GENERATED BY DRV.MP - DO NOT MODIFY."&char(10)& + "%"&char(10)&char(10)& + "verbatimtex %&latex"&char(10)& + tex_preamble_str[0]& + "\begin{document}"&char(10)& + tex_preamble_str[1]& + "etex;" + to delayed_tex_file; +drv_message "done."; + +% +% writing LaTeX picture definitions +% + +numeric tex_pct_idx; +tex_pct_idx:=0; + +% Math style indices: 0, 1, 2, 3 +string mth_sty_str[]; +mth_sty_str[0]:="\displaystyle"; +mth_sty_str[1]:="\textstyle"; +mth_sty_str[2]:="\scriptstyle"; +mth_sty_str[3]:="\scriptscriptstyle"; + +string drv_fontsize; + +vardef drv_tex[] expr tex_str= + % @: math style index + % tex_str: math mode LaTeX code + save def_str, pct; + string def_str; + picture pct; + def_str:="btex{"&drv_fontsize&"$"&mth_sty_str[@]&"{}"&tex_str&"{}$}etex;"; + write "tex_pct["&(decimal tex_pct_idx)&"]:="&def_str to delayed_tex_file; + pct:= + if known tex_pct[tex_pct_idx]: + tex_pct[tex_pct_idx] + else: + nullpicture + fi; + tex_pct_idx:=tex_pct_idx+1; + pct +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% MetaPost shorthands +% + +vardef depth expr pct= + ypart llcorner pct +enddef; + +vardef height expr pct= + ypart urcorner pct +enddef; + +vardef width expr pct= + xpart urcorner pct-xpart llcorner pct +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Font-specific parameters +% + +% +% em[s] width of an m (s: mathstyle index) +% ex[s] height of an x +% axis_hg[s] height of the mathematical axis +% num_bl_hg[s] height of a numerator baseline w.r.t. the fraction bar axis +% den_bl_dp[s] depth of a denominator baseline w.r.t. the fraction bar axis +% rul_thk[s] default rule thickness +% + +numeric em[], ex[], axis_hg[], num_bl_hg[], den_bl_dp[], rul_thk[]; + +% +% thn_sp[s] thin space, usually 1em/6 +% med_sp[s] medium space, usually 2em/9 +% thk_sp[s] thick space, usually 5em/18 +% + +numeric thn_sp[], med_sp[], thk_sp[]; + +% +% pdt_hg[s] height of a punctuation ldot +% pdt_wd[s] width of a punctuation ldot +% + +numeric pdt_hg[], pdt_wd[]; + +% +% tt_dgt[s][i] typewriter typeface digits (i ranges from 0 to 9) +% + +picture tt_dgt[][]; + +% +% min_clr[s] minimal clearance between a numerator +% or a denominator and the fraction bar +% prm_skp[s] +% jdg_skp[s] +% ilb_skp[s] +% plb_skp[s] +% + +numeric min_clr[], prm_skp[], jdg_skp[], ilb_skp[], plb_skp[]; + +vardef drv_fontdimen[] expr font= + save dim_pct; + picture dim_pct; + dim_pct:=drv_tex[0] ("\rule{\the\fontdimen"&(decimal @)&font&"}{0bp}"); + width dim_pct +enddef; + +vardef drv_font_size expr size_str= + save pdt_pct, sp_pct; + picture pdt_pct, sp_pct; + drv_fontsize:=size_str; + write char(10)&"% font-specific parameters ("&drv_fontsize&")"&char(10) + to delayed_tex_file; + ex[0]:=drv_fontdimen[5] "\textfont2"; + ex[1]:=drv_fontdimen[5] "\textfont2"; + ex[2]:=drv_fontdimen[5] "\scriptfont2"; + ex[3]:=drv_fontdimen[5] "\scriptscriptfont2"; + em[0]:=drv_fontdimen[6] "\textfont2"; + em[1]:=drv_fontdimen[6] "\textfont2"; + em[2]:=drv_fontdimen[6] "\scriptfont2"; + em[3]:=drv_fontdimen[6] "\scriptscriptfont2"; + rul_thk[0]:=drv_fontdimen[8] "\textfont3"; + rul_thk[1]:=drv_fontdimen[8] "\textfont3"; + rul_thk[2]:=drv_fontdimen[8] "\scriptfont3"; + rul_thk[3]:=drv_fontdimen[8] "\scriptscriptfont3"; + axis_hg[0]:=drv_fontdimen[22] "\textfont2"; + axis_hg[1]:=drv_fontdimen[22] "\textfont2"; + axis_hg[2]:=drv_fontdimen[22] "\scriptfont2"; + axis_hg[3]:=drv_fontdimen[22] "\scriptscriptfont2"; + num_bl_hg[0]:=(drv_fontdimen[8] "\textfont2")-axis_hg[0]; + num_bl_hg[1]:=(drv_fontdimen[9] "\textfont2")-axis_hg[1]; + num_bl_hg[2]:=(drv_fontdimen[9] "\scriptfont2")-axis_hg[2]; + num_bl_hg[3]:=(drv_fontdimen[9] "\scriptscriptfont2")-axis_hg[3]; + den_bl_dp[0]:=-(drv_fontdimen[11] "\textfont2")-axis_hg[0]; + den_bl_dp[1]:=-(drv_fontdimen[12] "\textfont2")-axis_hg[1]; + den_bl_dp[2]:=-(drv_fontdimen[12] "\scriptfont2")-axis_hg[2]; + den_bl_dp[3]:=-(drv_fontdimen[12] "\scriptscriptfont2")-axis_hg[3]; + min_clr[0]:=3*rul_thk[0]; % The TEXbook, + min_clr[1]:=1*rul_thk[1]; % Appendix G, + min_clr[2]:=1*rul_thk[2]; % Rule 15d. + min_clr[3]:=1*rul_thk[3]; % + for mth_sty:=0 upto 3: + sp_pct:=drv_tex[mth_sty] "\,"; + thn_sp[mth_sty]:=width sp_pct; + sp_pct:=drv_tex[mth_sty] "\>"; + med_sp[mth_sty]:=width sp_pct; + sp_pct:=drv_tex[mth_sty] "\;"; + thk_sp[mth_sty]:=width sp_pct; + pdt_pct:=drv_tex[mth_sty] "\ldotp"; + pdt_hg[mth_sty]:=height pdt_pct; + pdt_wd[mth_sty]:=width pdt_pct; + for dgt=0 upto 9: + tt_dgt[mth_sty][dgt]:=drv_tex[mth_sty] "\texttt{"&(decimal dgt)&"}"; + endfor + prm_skp[mth_sty]:=3*med_sp[mth_sty]; % arbitrary + jdg_skp[mth_sty]:=thn_sp[mth_sty]; % arbitrary + ilb_skp[mth_sty]:=thn_sp[mth_sty]; % arbitrary + plb_skp[mth_sty]:=thk_sp[mth_sty]; % arbitrary + endfor +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Math-related parameters & macros +% + +% +% Math styles +% drv_sty derivation trees +% jdg_sty[drv_sty] judgments +% ilb_sty[drv_sty] inference labels +% dlb_sty[drv_sty] delimiter labels +% plb_sty[drv_sty] phantom steps labels +% + +numeric drv_sty, jdg_sty[], ilb_sty[], dlb_sty[], plb_sty[]; + +% +% Math-axis centered LaTeX pictures +% + +vardef mth_tex[] expr tex_str= + (drv_tex[@] tex_str) shifted (0, -axis_hg[@]) +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% drv-boxes +% + +vardef drv_box text STR= + for str=STR: + expandafter picture scantokens str; + expandafter pair scantokens str.l; + expandafter pair scantokens str.c; + expandafter pair scantokens str.r; + expandafter numeric scantokens str.hg; + expandafter numeric scantokens str.dp; + endfor +enddef; + +vardef box_init @# (expr pct)= + @#:=pct; + @#.r-@#.l=(width pct, 0); + @#.c=(@#.l+@#.r)/2; + @#.hg:=height pct; + @#.dp:=depth pct; +enddef; + +vardef box_freeze @#= + @#:=@# shifted @#.l; +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% beginfig & endfig +% + +% +% drv_beginfig: figure initialization +% + +pen drv_pen; + +vardef drv_beginfig= + % + % Judgments + % + % jdg[i] judgment drv-box + % sbj_num[i] number of sub-judgments + % sbj[i][j] sub-judgment drv-box (j ranges from 0 to sbj_num[i]-1) + % + drv_box "jdg[]"; + numeric sbj_num[]; + drv_box "sbj[][]"; + % + % Inferences + % + % prm_num[i] number of premises + % prm[i][j] premise index (j ranges from 0 to prm_num[i]-1) + % ccl[i] conclusion index + % jct_sty[i] junction style + % alg_sty[i] alignment style + % iln_sty[i] inference line style + % l_prm[i] leftmost `graphical' premise index + % r_prm[i] rightmost `graphical' premise index + % + numeric prm_num[], prm[][], ccl[]; + numeric jct_sty[]; + string alg_sty[]; + numeric iln_sty[]; + numeric l_prm[], r_prm[]; + % + % imin_x[i] inference minimal x + % l_dlb[i] left delimiter label drv-box + % l_dlm[i] left delimiter drv-box + % l_ilb[i] left label drv-box + % iln[i] inference line drv-box + % r_ilb[i] right label drv-box + % r_dlm[i] right delimiter drv-box + % r_dlb[i] right delimiter label drv-box + % imax_x[i] inference maximal x + % + numeric imin_x[]; + drv_box "l_dlb[]", "l_dlm[]", "l_ilb[]"; + drv_box "iln[]"; + drv_box "r_ilb[]", "r_dlm[]", "r_dlb[]"; + numeric imax_x[]; + % + % Sub-trees + % + % smin_x[i] sub-tree minimal x + % smax_x[i] sub-tree maximal x + % smin_y[i] sub-tree minimal y + % smax_y[i] sub-tree maximal y + % boxed[i] boolean + % + numeric smin_x[], smax_x[], smin_y[], smax_y[]; + boolean boxed[]; + % + % Pen initialization + % + drv_pen:=pencircle scaled rul_thk[drv_sty]; + % + % num_hg height of a numerator axis w.r.t. the fraction bar axis + % den_dp depth of a denominator axis w.r.t. the fraction bar axis + % iln_hg[s] height of a style s inference line + % iln_dp[s] depth of a style s inference line + % + numeric num_hg, den_dp, iln_hg[], iln_dp[]; + num_hg:=num_bl_hg[drv_sty]+axis_hg[jdg_sty[drv_sty]]; + den_dp:=den_bl_dp[drv_sty]+axis_hg[jdg_sty[drv_sty]]; + picture iln_pct; + for sty=0 upto 6: + iln_pct:=((0, 0)--(10, 0)) drv_styled sty; + iln_hg[sty]:=height iln_pct; + iln_dp[sty]:=depth iln_pct; + endfor + % + % Derivation trees + % + % root_num number of roots + % root[i] root index (i ranges from 0 to root_num-1) + % drv_built boolean + % drv_frozen boolean + % + numeric root_num, root[]; + boolean drv_checked, drv_built, drv_frozen; + root_num:=0; + drv_checked:=false; + drv_built:=false; + drv_frozen:=false; + % + % Phantom steps + % + % phm_idx phantom inferences index + % src[i] base phantom judgment index (in case of an origin judgment) + % tgt[i] origin judgment index (in case of a base phantom judgment) + % phm_sty[i] phantom steps style + % l_plb[i] left phantom steps label drv-box (in case of a base + % phantom judgment) + % phm[i] phantom steps drv-box (in case of a base phantom + % judgment) + % r_plb[i] right phantom steps label drv-box (in case of a base + % phantom judgment) + % + numeric phm_idx, src[], tgt[], phm_sty[]; + phm_idx:=0; + drv_box "l_plb[]", "phm[]", "r_plb[]"; + % + % Proof pictures + % + % jdg_prf[i] judgment index drv-box + % sbj_prf[i][j] sub-judgment index drv-box (j ranges from 0 to + % sbj_num[i]-1) + % + drv_box "jdg_prf[]", "sbj_prf[][]"; + % + % Info + % + write char(10)&"% fig. "&(decimal charcode)&char(10) to delayed_tex_file; + drv_inside_fig:=true; % context: inside a figure +enddef; + +extra_beginfig:=extra_beginfig&"drv_beginfig;"; + +% +% drv_endfig: proof-file generation +% + +string proof_file; +proof_file:=jobname&"-proof.tex"; + +% TODO: taking outputtemplate into account. +vardef output_file[]= + jobname&"."&(decimal @) +enddef; + +string buf_str; +buf_str:= + "%"&char(10)& + "% AUTOMATICALLY GENERATED BY DRV.MP."&char(10)& + "%"&char(10)&char(10)& + tex_preamble_str[0]& + "\usepackage{graphicx}"&char(10)& + "\makeatletter"&char(10)& + "\def\Gin@def@bp#1\relax#2#3{\gdef#2{#3}}"&char(10)& + "\newsavebox{\graphicsbox}"&char(10)& + "\newcommand*{\drv}[1]{%"&char(10)& + "\sbox{\graphicsbox}{\includegraphics{#1}}%"&char(10)& + "\raisebox{\Gin@lly bp}%"&char(10)& + "{\usebox{\graphicsbox}}}"&char(10)& + "\makeatother"&char(10)&char(10)& + "\newcount\h"&char(10)& + "\newcount\m"&char(10)& + "\h=\time"&char(10)& + "\divide\h 60"&char(10)& + "\m=-\h"&char(10)& + "\multiply\m 60"&char(10)& + "\advance\m\time"&char(10)& + "\def\hm{\number\h:\ifnum\m<10{}0\fi\number\m}"&char(10)&char(10)& + "\newcommand{\mathaxis}{\frac{\quad}{}}"&char(10)&char(10)& + "\begin{document}"&char(10)& + tex_preamble_str[1]& + "\noindent\today\ at \hm\medskip"&char(10)&char(10)&"\noindent"; + +vardef drv_endfig= + drv_inside_fig:=false; % context: outside a figure + buf_str:=buf_str&char(10)& + "\texttt{"&output_file[charcode]&"}"&char(10)& + " (\verb+"&drv_fontsize&"+, \verb+"&(mth_sty_str[drv_sty])&"+)"&char(10)& + " {"&drv_fontsize&char(10)& + " \["&(mth_sty_str[drv_sty])&char(10)& + " \mathaxis\drv{"&output_file[charcode]&"}\mathaxis"&char(10)& + " \]}\\"; + write EOF to proof_file; % erases the previous content + write buf_str&char(10)&"\end{document}" to proof_file; + write EOF to proof_file; + if drv_nullpicture: + draw btex{\tt drv}: run {\tt mpost} again.etex withcolor (1, 0, 0); + fi +enddef; + +extra_endfig:="drv_endfig;"&extra_endfig; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Judgment declarations +% + +vardef jgm[] text SUB= + % @: judgment index + % SUB: list of `sub-judgments' (pictures or strings) + if @<0: + drv_errhelp "An judgment index can not be negative."; + drv_errmessage (decimal @)&" is negative"; + elseif known jdg[@]: + drv_errhelp "An index can be used only once to declare a judgment."; + drv_errmessage (decimal @)&" has been used already as a judgment index"; + else: + save jdg_pct, sbj_pct, jdg_wd, sbj_rnk; + picture jdg_pct, sbj_pct; + numeric jdg_wd, sbj_rnk; + jdg_pct:=nullpicture; + jdg_wd:=0; + sbj_rnk:=0; + for sub=SUB: + sbj_pct:= + if picture sub: + sub + elseif sub<>"": + mth_tex[jdg_sty[drv_sty]] sub + else: + nullpicture + fi; + box_init sbj[@][sbj_rnk] (sbj_pct); + if sbj_rnk>0: + sbj[@][sbj_rnk-1].r=sbj[@][sbj_rnk].l; + fi + addto jdg_pct also sbj_pct shifted (jdg_wd, 0); + jdg_wd:=width jdg_pct; + sbj_rnk:=sbj_rnk+1; + endfor + sbj_num[@]:=sbj_rnk; + box_init jdg[@] (jdg_pct); + if sbj_num[@]>0: + jdg[@].l=sbj[@][0].l; + jdg[@].r=sbj[@][sbj_num[@]-1].r; + fi + fi +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Inference declarations +% + +vardef check_junction_style (suffix sty_sfx) (expr default)= + save sty_str; + string sty_str; + sty_str:=str sty_sfx; + if (sty_str="0") + or (sty_str="1") + or (sty_str="2") + or (sty_str="3"): + sty_sfx + elseif (sty_str="_"): + default + else: + begingroup + drv_errhelp "Valid identifiers are"& + " 0 (fully-interlacing),"& + " 1 (semi-interlacing),"& + " 2 (non-interlacing),"& + " 3 (user specified) and"& + " _ (default)."; + drv_errmessage sty_str&" is not a valid junction style identifier"; + default + endgroup + fi +enddef; + +vardef check_alignment_style (suffix sty_sfx) (expr default)= + save sty_str; + string sty_str; + sty_str:=str sty_sfx; + if (sty_str="l") + or (sty_str="c") + or (sty_str="r") + or (sty_str="u"): + sty_str + elseif (sty_str="_"): + default + else: + begingroup + drv_errhelp "Valid identifiers are"& + " l (none),"& + " c (simple),"& + " r (double),"& + " u (dotted) and"& + " _ (default)."; + drv_errmessage sty_str&" is not a valid alignment style identifier"; + default + endgroup + fi +enddef; + +vardef check_path_style (suffix sty_sfx) (expr default)= + save sty_str; + string sty_str; + sty_str:=str sty_sfx; + if (sty_str="0") + or (sty_str="1") + or (sty_str="2") + or (sty_str="3") + or (sty_str="4") + or (sty_str="5") + or (sty_str="6"): + sty_sfx + elseif (sty_str="_"): + default + else: + begingroup + drv_errhelp "Valid identifiers are"& + " 0 (none),"& + " 1 (simple),"& + " 2 (double),"& + " 3 (dotted),"& + " 4 (dashed),"& + " 5 (waved),"& + " 6 (TeX-dotted) and"& + " _ (default)."; + drv_errmessage sty_str&" is not a valid path style identifier"; + default + endgroup + fi +enddef; + +vardef opt_init[] @# expr arg= + if picture arg: + if arg<>nullpicture: + box_init @# (arg); + fi + elseif arg<>"": + box_init @# (mth_tex[@] arg); + fi +enddef; + +vardef NFR[] (text PRM) (expr lilb, rilb, ldlb, rdlb) + (suffix j_sty, a_sty, i_sty)= + % + % @: inference index + % + if known prm_num[@]: + drv_errhelp "An index can be used only once to declare an inference."; + drv_errmessage (decimal @)&" has been used already as an inference index"; + else: + % + % PRM: list of premise indices + % + save prm_rnk; + numeric prm_rnk; + prm_rnk:=0; + for prm_idx=PRM: + if prm_idx=@: + drv_errhelp "An inference index can not be used"& + " as one of its own premise indices."; + drv_errmessage "the inference index "&(decimal prm_idx)& + " is used as one of its own premise indices"; + elseif known ccl[prm_idx]: + drv_errhelp "An index can be used only once as a premise index."; + drv_errmessage (decimal prm_idx)&" has been used already as a"& + " premise index for inference declaration "&(decimal ccl[prm_idx]); + else: + if known prm_num[prm_idx]: + % + % roots list update + % + save root_idx; + numeric root_idx; + root_idx:=0; + forever: + exitif root[root_idx]=prm_idx; + root_idx:=root_idx+1; + endfor + forever: + exitif root_idx=root_num-1; + root[root_idx]:=root[root_idx+1]; + root_idx:=root_idx+1; + endfor + root_num:=root_num-1; + fi + ccl[prm_idx]:=@; + prm[@][prm_rnk]:=prm_idx; + prm_rnk:=prm_rnk+1; + fi + endfor + prm_num[@]:=prm_rnk; + if known ccl[@]: + % + % cycle detection + % + save ccl_idx, ccl_str; + numeric ccl_idx; + string ccl_str; + ccl_idx:=@; + ccl_str:=decimal ccl_idx; + forever: + ccl_idx:=ccl[ccl_idx]; + if ccl_idx>=0: + ccl_str:=(decimal ccl_idx)&", "&ccl_str; + fi + exitif (unknown ccl[ccl_idx]) or (ccl_idx=@); + endfor + if ccl_idx=@: + drv_errhelp "Inferences declarations can not be cyclic."; + drv_errmessage "inference declaration "&(decimal @)&" creates a"& + " cycle of inferences (indices "&ccl_str&" from conclusions to"& + " premises)"; + fi + else: + root[root_num]:=@; + root_num:=root_num+1; + fi + % + % lilb, rilb: inference labels + % + opt_init[ilb_sty[drv_sty]] l_ilb[@] lilb; + opt_init[ilb_sty[drv_sty]] r_ilb[@] rilb; + % + % ldlb, rdlb: delimiter labels + % + opt_init[dlb_sty[drv_sty]] l_dlb[@] ldlb; + opt_init[dlb_sty[drv_sty]] r_dlb[@] rdlb; + % + % j_sty, a_sty and i_sty: junction, alignment and inference styles + % + jct_sty[@]:=check_junction_style (j_sty, drv_jct_sty); + alg_sty[@]:=check_alignment_style (a_sty, drv_alg_sty); + iln_sty[@]:=check_path_style (i_sty, drv_iln_sty); + if drv_boxmode_on: + boxed[@]:=true; + fi + fi +enddef; + +vardef DCL[] (text PRM) (expr lilb, rilb, ldlb, rdlb) + (suffix j_sty, a_sty, i_sty) text SUB= + NFR[@] (PRM) (lilb, rilb, ldlb, rdlb, j_sty, a_sty, i_sty); + jgm[@] SUB; +enddef; + +vardef MVD[] (expr inf_num, lplb, rplb) (suffix a_sty, p_sty)= + if inf_num<1: + drv_errhelp "The minimal value is 1."; + drv_errmessage (decimal inf_num)&" is not a valid number of inference"& + " steps"; + else: + save aux_idx, aux_sty, phm_jdg; + numeric aux_idx, aux_sty; + picture phm_jdg; + aux_sty:=check_path_style (p_sty, drv_phm_sty); + phm_jdg:=nullpicture; + setbounds phm_jdg to (0, 0)--(iln_hg[aux_sty]-iln_dp[aux_sty], 0)--cycle; + aux_idx:=@; + for i=1 upto inf_num: + phm_idx:=phm_idx-1; + box_init jdg[phm_idx] (phm_jdg); + sbj_num[phm_idx]:=0; + NFR[phm_idx] (aux_idx) ("", "", "", "", 0, a_sty, 0); + aux_idx:=phm_idx; + endfor + src[@]:=phm_idx; + tgt[phm_idx]:=@; + phm_sty[phm_idx]:=aux_sty; + % + % lplb, rplb: phantom steps labels + % + opt_init[plb_sty[drv_sty]] l_plb[phm_idx] lplb; + opt_init[plb_sty[drv_sty]] r_plb[phm_idx] rplb; + phm_idx + fi +enddef; + +vardef bxd[]= + boxed[@]:=true; + @ +enddef; + +% +% Optional labels & shorthands +% + +numeric drv_jct_sty; % default junction style +string drv_alg_sty; % default junction style +numeric drv_iln_sty; % default inference line path-style +numeric drv_phm_sty; % default phantom steps path-style + +boolean drv_left_ilb; % inference labels on the left +boolean drv_left_dlb; % delimiter labels (hence delimiters) on the left +boolean drv_left_plb; % phantom steps labels on the left + +vardef arg_type expr arg= + if picture arg: + "picture" + else: + "string" + fi +enddef; + +vardef opt_lbls @# (text LBL) expr left_lbls= + save lbl_num, fst_lbl, snd_lbl; + numeric lbl_num; + lbl_num:=0; + for lbl=LBL: + if lbl_num=0: + scantokens (arg_type lbl) fst_lbl; + fst_lbl:=lbl; + elseif lbl_num=1: + scantokens (arg_type lbl) snd_lbl; + snd_lbl:=lbl; + else: + drv_errhelp "At most two labels can be specified:"& + " a left one and a right one."; + drv_errmessage "more than two labels have been specified"; + fi + lbl_num:=lbl_num+1; + endfor + if lbl_num=0: + string @#.l; + string @#.r; + @#.l:=""; + @#.r:=""; + elseif lbl_num=1: + if left_lbls: + scantokens (arg_type fst_lbl) @#.l; + string @#.r; + @#.l:=fst_lbl; + @#.r:=""; + else: + string @#.l; + scantokens (arg_type fst_lbl) @#.r; + @#.l:=""; + @#.r:=fst_lbl; + fi + else: + scantokens (arg_type fst_lbl) @#.l; + scantokens (arg_type snd_lbl) @#.r; + @#.l:=fst_lbl; + @#.r:=snd_lbl; + fi +enddef; + +vardef NFR_opt[] (text PRM) (text ILB) (text DLB) + (suffix j_sty, a_sty, i_sty)= + opt_lbls ilb (ILB) drv_left_ilb; + opt_lbls dlb (DLB) drv_left_dlb; + NFR[@] (PRM) (ilb.l, ilb.r, dlb.l, dlb.r, j_sty, a_sty, i_sty); +enddef; + +vardef DCL_opt[] (text PRM) (text ILB) (text DLB) + (suffix j_sty, a_sty, i_sty) text SUB= + NFR_opt[@] (PRM) (ILB) (DLB) (j_sty, a_sty, i_sty); + jgm[@] SUB; +enddef; + +vardef MVD_opt[] (expr inf_num) (text PLB) (suffix a_sty, p_sty)= + opt_lbls plb (PLB) drv_left_plb; + MVD[@] (inf_num, plb.l, plb.r, a_sty, p_sty) +enddef; + +% Nfr, Dcl & Mvd + +vardef Nfr[] (text PRM) (expr ilb, ldlb, rdlb) (suffix i_sty)= + NFR_opt[@] (PRM) (ilb) (ldlb, rdlb) (_, _, i_sty); +enddef; + +vardef Dcl[] (text PRM) (expr ilb, ldlb, rdlb) (suffix i_sty) text SUB= + Nfr[@] (PRM) (ilb, ldlb, rdlb, i_sty); + jgm[@] SUB; +enddef; + +vardef Mvd[] (expr inf_num, lplb, rplb) (suffix p_sty)= + MVD[@] (inf_num, lplb, rplb, _, p_sty) +enddef; + +% nfr, dcl & mvd + +vardef nfr[] (text PRM) (expr ilb) (suffix i_sty)= + NFR_opt[@] (PRM) (ilb) () (_, _, i_sty); +enddef; + +vardef dcl[] (text PRM) (expr ilb) (suffix i_sty) text SUB= + nfr[@] (PRM) (ilb, i_sty); + jgm[@] SUB; +enddef; + +vardef mvd[] (expr inf_num) (suffix p_sty)= + MVD_opt[@] (inf_num) () (_, p_sty) +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Pictured paths +% + +vardef dotted_aux (expr pth, dot_wd, dots_dist)= + save pth_len, pct; + numeric pth_len; + picture pct; + pth_len:=arclength pth; + pct:=nullpicture; + if dots_dist>0: + stp_num:=round ((pth_len-dot_wd)/dots_dist); + if stp_num>0: + stp_len:=(pth_len-dot_wd)/stp_num; + addto pct doublepath pth dashed dashpattern (on 0 off stp_len) + shifted (dot_wd/2, 0) withpen pencircle scaled dot_wd; + fi + fi + pct +enddef; + +primarydef pth dotted wd_dist= + dotted_aux(pth, xpart wd_dist, ypart wd_dist) +enddef; + +vardef expanded_aux (expr pth, scl, dir, stp_len)= + save pth_len, aux_len; + numeric pth_len, aux_len; + pth_len:=arclength pth; + if (stp_len>0) and (pth_len>stp_len): + aux_len:=pth_len/(pth_len div stp_len); + point arctime 0 of pth of pth shifted + (unitvector direction arctime 0 of pth of pth + rotated dir scaled scl).. + {direction arctime 0 of pth of pth} + for i=aux_len step aux_len until pth_len-aux_len: + point arctime i of pth of pth shifted + (unitvector direction arctime i of pth of pth + rotated dir scaled scl) + {direction arctime i of pth of pth}.. + endfor + point arctime pth_len of pth of pth shifted + (unitvector direction arctime pth_len of pth of pth + rotated dir scaled scl) + {direction arctime pth_len of pth of pth} + else: + pth + fi +enddef; + +primarydef pth expanded scl_dir_len= + expanded_aux (pth, + redpart scl_dir_len, greenpart scl_dir_len, bluepart scl_dir_len) +enddef; + +vardef waved_aux (expr pth, amp)= + save pth_len, mid; + numeric pth_len, mid; + pth_len:=arclength pth; + if (amp>0) and (pth_len>2(1+sqrt 5)*amp): + mid:=pth_len/(2(pth_len div (2(1+sqrt 5)*amp))); + point arctime 0 of pth of pth shifted + (unitvector direction arctime 0 of pth of pth + rotated -90 scaled amp) + {direction arctime 0 of pth of pth} + for i=mid step 2mid until pth_len: + ..point arctime i of pth of pth shifted + (unitvector direction arctime i of pth of pth + rotated 90 scaled amp) + {direction arctime i of pth of pth} + ..point arctime i+mid of pth of pth shifted + (unitvector direction arctime i+mid of pth of pth + rotated -90 scaled amp) + {direction arctime i+mid of pth of pth} + endfor + else: + pth + fi +enddef; + +primarydef pth waved amp= + waved_aux(pth, amp) +enddef; + +vardef drv_styled_aux[] expr pth= + save sty_idx, pth_len, pct; + numeric sty_idx, pth_len; + picture pct; + sty_idx:=check_path_style (@, 1); + pth_len:=arclength pth; + pct:=nullpicture; + if sty_idx=1: + interim linecap:=butt; + addto pct doublepath pth withpen drv_pen; + elseif sty_idx=2: + interim linecap:=butt; + addto pct doublepath pth + expanded (1.25rul_thk[drv_sty], 90, rul_thk[drv_sty]) + withpen drv_pen; + addto pct doublepath pth + expanded (1.25rul_thk[drv_sty], -90, rul_thk[drv_sty]) + withpen drv_pen; + elseif sty_idx=3: + addto pct also pth dotted (rul_thk[drv_sty], 2rul_thk[drv_sty]); + elseif sty_idx=4: + if rul_thk[drv_sty]>0: + interim linecap:=butt; + save dsh_num, dsh_len; + numeric dsh_num, dsh_len; + dsh_num:=round(pth_len/(3rul_thk[drv_sty])); + dsh_len:= + if odd dsh_num: + pth_len/dsh_num + else: + pth_len/(dsh_num+1) + fi; + addto pct doublepath pth dashed dashpattern(on dsh_len off dsh_len) + withpen drv_pen; + fi + elseif sty_idx=5: + interim linecap:=butt; + addto pct doublepath pth + waved 1.25rul_thk[drv_sty] withpen drv_pen; + elseif (sty_idx=6) and (pth_len>0): + addto pct also pth dotted (pdt_hg[drv_sty], pdt_wd[drv_sty]); + fi + pct +enddef; + +primarydef pth drv_styled sty= + drv_styled_aux[sty] pth +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Delimiters +% + +% +% 1. Global parameters +% + +string drv_l_dlm; % left delimiter LaTeX code +string drv_r_dlm; % right delimiter LaTeX code + +% +% 2. Macros +% + +vardef minmax_y[]=( + if drv_bot_roots: + if known ccl[@]: + ypart jdg[@].c-num_hg+iln_hg[(iln_sty[ccl[@]])] + +min_clr_scl*min_clr[drv_sty]/2 + else: + smin_y[@]-min_clr_scl*min_clr[drv_sty] + fi, + smax_y[@]+min_clr_scl*min_clr[drv_sty] + else: + smin_y[@]-min_clr_scl*min_clr[drv_sty], + if known ccl[@]: + ypart jdg[@].c-den_dp-iln_hg[(iln_sty[ccl[@]])] + -min_clr_scl*min_clr[drv_sty]/2 + else: + smax_y[@]+min_clr_scl*min_clr[drv_sty] + fi + fi) +enddef; + +vardef delim @# expr dlm_len= + save rule_str, dlm_str, dlm_pct, dlm_dp; + string rule_str, dlm_str; + picture dlm_pct; + numeric dlm_dp; + rule_str:="\rule{0bp}{"&(decimal(dlm_len/2+axis_hg[drv_sty]))&"bp}"; + dlm_str:= + if str @#="l": + "\left"&drv_l_dlm&rule_str&"\right." + else: + "\left."&rule_str&"\right"&drv_r_dlm + fi; + dlm_pct:=mth_tex[drv_sty] dlm_str; + dlm_dp:=depth dlm_pct; + if dlm_dp=0: + nullpicture + else: + begingroup + setbounds dlm_pct to + (xpart llcorner dlm_pct, dlm_dp) + --(xpart ulcorner dlm_pct, -dlm_dp) + --(xpart urcorner dlm_pct, -dlm_dp) + --(xpart lrcorner dlm_pct, dlm_dp) + --cycle; + dlm_pct yscaled (dlm_len/(2*height dlm_pct)) + endgroup + fi +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Checking, building, freezing (very inefficient, to be improved) +% + +% +% 1. Global parameters +% + +numeric min_clr_scl; % +numeric prm_skp_scl; % +numeric jdg_skp_scl; % +numeric ilb_skp_scl; % +numeric plb_skp_scl; % + +boolean drv_bot_roots; % +boolean drv_boxmode_on; % +boolean drv_fractionmode_on; % +string drv_axis_ref; % + +% +% 2. Macros +% + +% +% Checking +% + +vardef fraction_inference[]= + (prm_num[@]=0) + and (iln_sty[@]=0) + and (unknown l_ilb[@]) + and (unknown r_ilb[@]) + and drv_fractionmode_on +enddef; + +vardef drv_check_root[]= + if unknown jdg[@]: + drv_errhelp "An index must be used to declare a both a judgment and an"& + " inference."; + drv_errmessage (decimal @)&" has been used as an inference index but not"& + " as a judgment index"; + elseif unknown prm_num[@]: + drv_errhelp "An index must be used to declare a both a judgment and an"& + " inference."; + drv_errmessage (decimal @)&" has been used as a judgment index but not"& + " as an inference index"; + else: + save i_sty, prm_idx; + numeric i_sty, prm_idx; + i_sty:=iln_sty[@]; + for prm_rnk=0 upto prm_num[@]-1: + prm_idx:=prm[@][prm_rnk]; + drv_check_root[prm_idx]; + % + % numerators and denominators clearances + % The TEXbook, Appendix G, Rule 15d. + % + if drv_bot_roots: + num_hg:=max(num_hg, + iln_hg[i_sty]+min_clr_scl*min_clr[drv_sty]-jdg[prm_idx].dp); + else: + den_dp:=min(den_dp, + iln_dp[i_sty]-min_clr_scl*min_clr[drv_sty]-jdg[prm_idx].hg); + fi + endfor + if not fraction_inference[@]: + if drv_bot_roots: + den_dp:=min(den_dp, + iln_dp[i_sty]-min_clr_scl*min_clr[drv_sty]-jdg[@].hg); + else: + num_hg:=max(num_hg, + iln_hg[i_sty]+min_clr_scl*min_clr[drv_sty]-jdg[@].dp); + fi + fi + if unknown boxed[@]: + boxed[@]:=false; + fi + fi +enddef; + +vardef drv_check= + if root_num=0: + drv_errhelp "Well ..."; + drv_errmessage "no inference has been declared"; + else: + save root_idx; + numeric root_idx; + root_idx:=root[0]; + drv_check_root[root_idx]; + if root_num>1: + save root_str; + string root_str; + root_str:=decimal root_idx; + for idx=1 upto root_num-1: + root_idx:=root[idx]; + drv_check_root[root_idx]; + root_str:=root_str&", "&(decimal root_idx); + endfor + drv_message "warning, multiple root indices ("&root_str&")."; + fi + fi + drv_checked:=true; +enddef; + +% +% Building +% + +vardef drv_build_root[]= + % + % premises junction (from left to right) + % + for prm_rnk=0 upto prm_num[@]-1: + drv_build_root[prm[@][prm_rnk]]; + if prm_rnk>0: + save ll_idx, lr_idx, rl_idx, rr_idx; + save lmax_x, rmin_x, min_skp; + numeric ll_idx, lr_idx, rl_idx, rr_idx; + numeric lmax_x, rmin_x, min_skp; + ypart jdg[prm[@][prm_rnk-1]].c=ypart jdg[prm[@][prm_rnk]].c; + ll_idx:=prm[@][0]; + lr_idx:=prm[@][prm_rnk-1]; + rl_idx:=prm[@][prm_rnk]; + rr_idx:=prm[@][prm_rnk]; + lmax_x:=imax_x[lr_idx]; + rmin_x:=imin_x[rl_idx]; + min_skp[0]:=rmin_x-lmax_x; + forever: + exitif (unknown r_prm[lr_idx]) or (unknown l_prm[rl_idx]); + ll_idx:=l_prm[ll_idx]; + lr_idx:=r_prm[lr_idx]; + rl_idx:=l_prm[rl_idx]; + rr_idx:=r_prm[rr_idx]; + lmax_x:=max(lmax_x, imax_x[lr_idx]); + rmin_x:=min(rmin_x, imin_x[rl_idx]); + min_skp[0]:=min(min_skp[0], imin_x[rl_idx]-imax_x[lr_idx]); + endfor + min_skp[1]:=rmin_x-lmax_x; + if known r_prm[lr_idx]: + r_prm[rr_idx]:= r_prm[lr_idx]; + lmax_x:=smax_x[lr_idx]; + elseif known l_prm[rl_idx]: + l_prm[ll_idx]:=l_prm[rl_idx]; + rmin_x:=smin_x[rl_idx]; + fi + min_skp[2]:=rmin_x-lmax_x; + if jct_sty[@]<3: + min_skp[jct_sty[@]]=prm_skp_scl*prm_skp[drv_sty]; + fi + fi + endfor + if prm_num[@]>0: + l_prm[@]:=prm[@][0]; + r_prm[@]:=prm[@][prm_num[@]-1]; + fi + % + % judgment alignment + % + if prm_num[@]=0: + imin_x[@]:=xpart jdg[@].l-jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; + imax_x[@]:=xpart jdg[@].r+jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; + else: + save l_xref, r_xref; + l_xref= + if boxed[prm[@][0]]: + smin_x[prm[@][0]] + else: + xpart jdg[prm[@][0]].l + fi; + r_xref= + if boxed[prm[@][prm_num[@]-1]]: + smax_x[prm[@][prm_num[@]-1]] + else: + xpart jdg[prm[@][prm_num[@]-1]].r + fi; + if alg_sty[@]="l": + xpart jdg[@].l=l_xref; + elseif alg_sty[@]="c": + xpart jdg[@].c=(l_xref+r_xref)/2; + elseif alg_sty[@]="r": + xpart jdg[@].r=r_xref; + fi + imin_x[@]:=min(xpart jdg[@].l, l_xref) + -jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; + imax_x[@]:=max(xpart jdg[@].r, r_xref) + +jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; + fi + % + % inference line + % + save iln_wd, iln_pct; + numeric iln_wd; + picture iln_pct; + iln_wd:=imax_x[@]-imin_x[@]; + iln_pct:=((0, 0)--(iln_wd, 0)) drv_styled iln_sty[@]; + setbounds iln_pct to + (0, ypart llcorner iln_pct) + --(0, ypart ulcorner iln_pct) + --(iln_wd, ypart ulcorner iln_pct) + --(iln_wd, ypart llcorner iln_pct) + --cycle; % ! `linecap:=butt' and `linecap:=squared' -> same bounding box ! + box_init iln[@] (iln_pct); + xpart iln[@].c=(imin_x[@]+imax_x[@])/2; + % + % orientation, smin_y & smax_y + % + if drv_bot_roots: + ypart iln[@].c=ypart jdg[@].c-den_dp; + smin_y[@]:=ypart jdg[@].c+jdg[@].dp; + smax_y[@]:= + if iln_sty[@]=0: + ypart jdg[@].c+jdg[@].hg + else: + ypart iln[@].c+iln[@].hg + fi; + if prm_num[@]>0: + ypart iln[@].c=ypart jdg[prm[@][0]].c-num_hg; + for prm_rnk=0 upto prm_num[@]-1: + smax_y[@]:=max(smax_y[@], smax_y[prm[@][prm_rnk]]); + endfor; + fi + else: + ypart iln[@].c=ypart jdg[@].c-num_hg; + smin_y[@]:= + if iln_sty[@]=0: + ypart jdg[@].c+jdg[@].dp + else: + ypart iln[@].c+iln[@].dp + fi; + smax_y[@]:=ypart jdg[@].c+jdg[@].hg; + if prm_num[@]>0: + ypart iln[@].c=ypart jdg[prm[@][0]].c-den_dp; + for prm_rnk=0 upto prm_num[@]-1: + smin_y[@]:=min(smin_y[@], smin_y[prm[@][prm_rnk]]); + endfor; + fi + fi + % + % inference labels + % + if known l_ilb[@]: + l_ilb[@].r=iln[@].l shifted (-ilb_skp_scl*ilb_skp[drv_sty], 0); + imin_x[@]:=xpart l_ilb[@].l; + smin_y[@]:=min(smin_y[@], ypart l_ilb[@].c+l_ilb[@].dp); + smax_y[@]:=max(smax_y[@], ypart l_ilb[@].c+l_ilb[@].hg); + fi + if known r_ilb[@]: + r_ilb[@].l=iln[@].r shifted (ilb_skp_scl*ilb_skp[drv_sty], 0); + imax_x[@]:=xpart r_ilb[@].r; + smin_y[@]:=min(smin_y[@], ypart r_ilb[@].c+r_ilb[@].dp); + smax_y[@]:=max(smax_y[@], ypart r_ilb[@].c+r_ilb[@].hg); + fi + % + % phantom steps + % + if known tgt[@]: + save phm_pth, phm_pct; + path phm_pth; + picture phm_pct; + save top_y, mid_y, bot_y; + numeric top_y, bot_y; + if drv_bot_roots: + bot_y:=xpart minmax_y[@]+min_clr_scl*min_clr[drv_sty]/2; + top_y:=xpart minmax_y[tgt[@]]; + else: + bot_y:=ypart minmax_y[tgt[@]]; + top_y:=ypart minmax_y[@]-min_clr_scl*min_clr[drv_sty]/2; + fi + mid_y:=(top_y+bot_y)/2; + phm_pth:=(0, (bot_y-top_y)/2)--(0, (top_y-bot_y)/2); + phm_pct:=phm_pth drv_styled phm_sty[@]; + box_init phm[@] (phm_pct shifted ((width phm_pct)/2, 0)); + phm[@].c=(xpart jdg[@].c, mid_y); + imin_x[@]:=min(imin_x[@], xpart phm[@].l); + imax_x[@]:=max(imax_x[@], xpart phm[@].r); + % + % phantom steps labels + % + if known l_plb[@]: + l_plb[@].r=phm[@].l shifted (-plb_skp[drv_sty], 0); + imin_x[@]:=min(imin_x[@], xpart l_plb[@].l); + fi + if known r_plb[@]: + r_plb[@].l=phm[@].r shifted ( plb_skp[drv_sty], 0); + imax_x[@]:=max(imax_x[@], xpart r_plb[@].r); + fi + fi + % + % smin_x & smax_x + % + smin_x[@]:=imin_x[@]; + smax_x[@]:=imax_x[@]; + for prm_rnk=0 upto prm_num[@]-1: + smin_x[@]:=min(smin_x[@], smin_x[prm[@][prm_rnk]]); + smax_x[@]:=max(smax_x[@], smax_x[prm[@][prm_rnk]]); + endfor + % + % delimiters + % + if known l_dlb[@] or known r_dlb[@]: + save idx, mmy, min_y, max_y; + numeric idx, min_y, max_y; + pair mmy; + mmy:=minmax_y[@]; + min_y:=xpart mmy; + max_y:=ypart mmy; + if known l_dlb[@]: + box_init l_dlm[@] (delim l (max_y-min_y)); + l_dlm[@].r=(smin_x[@], (max_y+min_y)/2); + l_dlb[@].r=l_dlm[@].l; + smin_x[@]:=xpart l_dlb[@].l; + fi + if known r_dlb[@]: + box_init r_dlm[@] (delim r (max_y-min_y)); + r_dlm[@].l=(smax_x[@], (max_y+min_y)/2); + r_dlb[@].l=r_dlm[@].r; + smax_x[@]:=xpart r_dlb[@].r; + fi + fi + if (known l_dlb[@]) or boxed[@]: + idx:=@; + forever: + imin_x[idx]:=smin_x[@]; + exitif unknown l_prm[idx]; + idx:=l_prm[idx]; + endfor + fi + if (known r_dlb[@]) or boxed[@]: + idx:=@; + forever: + imax_x[idx]:=smax_x[@]; + exitif unknown r_prm[idx]; + idx:=r_prm[idx]; + endfor + fi +enddef; + +vardef drv_build= + if not drv_checked: + drv_check; + fi + for idx=0 upto root_num-1: + drv_build_root[root[idx]]; + endfor + drv_built:=true; +enddef; + +% +% Freezing +% + +vardef drv_freeze_root[]= + for prm_rnk=0 upto prm_num[@]-1: + drv_freeze_root[prm[@][prm_rnk]]; + endfor + for sbj_rnk=0 upto sbj_num[@]-1: + box_freeze sbj[@][sbj_rnk]; + endfor + forsuffixes sfx= + iln, jdg, phm, + l_dlb, l_dlm, l_ilb, l_plb, + r_dlb, r_dlm, r_ilb, r_plb: + if known sfx[@]: + box_freeze sfx[@]; + fi + endfor +enddef; + +vardef drv_freeze= + if not drv_built: + drv_build; + fi + save root_idx; + numeric root_idx; + root_idx:=root[0]; + if unknown iln[root_idx].c: + % + % default math axis + % + if drv_axis_ref="iln": + iln[root_idx].c=(0, axis_hg[drv_sty]); + else: % drv_axis_ref="jdg" + jdg[root_idx].c=(0, axis_hg[drv_sty]); + fi + drv_freeze_root[root_idx]; + fi + for idx=1 upto root_num-1: + root_idx:=root[idx]; + if unknown iln[root_idx].c: + smin_x[root_idx]=smax_x[root[idx-1]]+prm_skp_scl*prm_skp[drv_sty]; + ypart iln[root_idx].c=ypart iln[root[idx-1]].c; + fi + drv_freeze_root[root_idx]; + endfor + drv_frozen:=true; +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Derivation tree pictures +% + +% +% 1. Global parameters +% + +boolean drv_proofmode_on; % +color prf_clr; % +color jdg_clr; % +color sbj_clr; % + +prf_clr:=.75background; % arbitrary +jdg_clr:=red; % arbitrary +sbj_clr:=blue; % arbitrary + +% +% 2. Macros +% + +vardef drv_tree_addto @# (expr idx) text draw_options= + for prm_rnk=0 upto prm_num[idx]-1: + drv_tree_addto @# (prm[idx][prm_rnk]) draw_options; + endfor + forsuffixes sfx= + jdg, phm, + l_dlb, l_dlm, l_ilb, l_plb, + r_dlb, r_dlm, r_ilb, r_plb: + if known sfx[idx]: + addto @# also sfx[idx] draw_options; + fi + endfor + if iln_sty[idx]>0: + addto @# also iln[idx] draw_options; + fi +enddef; + +vardef tt_nat[] expr nat= % typewriter typeface naturals + save nat_aux, nat_pct_wd, dgt_num, nat_pct; + numeric nat_aux, nat_pct_wd, dgt_num; + picture nat_pct; + nat_aux:=abs nat; + nat_pct:=nullpicture; + nat_pct_wd:=0; + dgt_num:=1; + forever: + exitif nat_aux div (10**dgt_num)=0; + dgt_num:=dgt_num+1; + endfor + for rnk:=1 upto dgt_num: + addto nat_pct also tt_dgt[@][nat_aux div (10**(dgt_num-rnk))] + shifted (nat_pct_wd, 0); + nat_pct_wd:=width nat_pct; + nat_aux:=nat_aux mod (10**(dgt_num-rnk)); + endfor + nat_pct shifted (0, -axis_hg[@]) +enddef; + +vardef prf_tree_addto @# expr idx= + for prm_rnk=0 upto prm_num[idx]-1: + prf_tree_addto @# (prm[idx][prm_rnk]); + endfor + if idx>=0: + box_init jdg_prf[idx] (tt_nat[2] idx); + jdg_prf[idx].r=jdg[idx].l; + box_freeze jdg_prf[idx]; + addto @# also jdg_prf[idx] withcolor jdg_clr; + addto @# doublepath jdg[idx].c withcolor jdg_clr + withpen pencircle scaled (2*pdt_hg[drv_sty]); + fi + for sbj_rnk=0 upto sbj_num[idx]-1: + box_init sbj_prf[idx][sbj_rnk] (tt_nat[3] sbj_rnk); + if odd sbj_rnk: + sbj_prf[idx][sbj_rnk].c shifted (0, sbj_prf[idx][sbj_rnk].hg)= + sbj[idx][sbj_rnk].c + shifted (0, -den_dp-min_clr_scl*min_clr[drv_sty]/2); + else: + sbj_prf[idx][sbj_rnk].c shifted (0, sbj_prf[idx][sbj_rnk].dp)= + sbj[idx][sbj_rnk].c + shifted (0, -num_hg+min_clr_scl*min_clr[drv_sty]/2); + fi + box_freeze sbj_prf[idx][sbj_rnk]; + addto @# also sbj_prf[idx][sbj_rnk] withcolor sbj_clr; + addto @# doublepath sbj[idx][sbj_rnk].c withcolor sbj_clr + withpen pencircle scaled pdt_hg[drv_sty]; + endfor +enddef; + +vardef drv_tree= + save pct; + picture pct; + pct:=nullpicture; + if not drv_frozen: + drv_freeze; + fi + for root_idx=0 upto root_num-1: + if drv_proofmode_on: + drv_tree_addto pct (root[root_idx]) withcolor prf_clr; + prf_tree_addto pct (root[root_idx]); + else: + drv_tree_addto pct (root[root_idx]); + fi + endfor + pct +enddef; + +vardef drv_bbox[]= + save min_x, max_x, mmy, min_y, max_y; + pair mmy; + numeric min_x, max_x, max_y, min_y; + if not drv_frozen: + drv_freeze; + fi + min_x:= + if known l_dlm[@].r: + xpart l_dlm[@].r + else: + smin_x[@] + fi-jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; + max_x:= + if known r_dlm[@].l: + xpart l_dlm[@].l + else: + smax_x[@] + fi+jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; + mmy:=minmax_y[@]; + min_y:=xpart mmy; + max_y:=ypart mmy; + (min_x, min_y)-- + (min_x, max_y)-- + (max_x, max_y)-- + (max_x, min_y)-- + cycle +enddef; + +vardef mth_axis @# (suffix ref_sfx) (expr idx)= + if not drv_frozen: + drv_freeze; + fi + if unknown prm_num[idx]: + drv_errhelp "An index must be used to declare an inference before it is"& + " used to set the math axis of a picture."; + drv_errmessage "no inference has been declared using index "&(decimal idx); + else: + save ref_str, yref; + string ref_str; + numeric yref; + ref_str:=str ref_sfx; + if ref_str="iln": + yref:=ypart iln[idx].c; + elseif ref_str="jdg": + yref:=ypart jdg[idx].c; + elseif ref_str="dlm": + if known l_dlm[idx]: + yref:=ypart l_dlm[idx].c; + elseif known r_dlm[idx]: + yref:=ypart r_dlm[idx].c; + else: + drv_errhelp "Well ..."; + drv_errmessage "no delimiter is attached to inference "&(decimal idx); + fi + else: + drv_errhelp "Valid identifiers are"& + " iln (inference line axis),"& + " jdg (judgment math-axis) and"& + " dlm (delimiter axis)."; + drv_errmessage (ref_str&" is not a valid reference type identifier"); + fi + if known yref: + @#:=@# shifted (0, axis_hg[drv_sty]-yref); + fi + fi +enddef; + +vardef drv_axis (suffix ref) (expr idx)= + mth_axis currentpicture (ref, idx); +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Tunings +% + +vardef check_math_style (expr sty_str, default)= + if sty_str="\displaystyle": + 0 + elseif sty_str="\textstyle": + 1 + elseif sty_str="\scriptstyle": + 2 + elseif sty_str="\scriptscriptstyle": + 3 + else: + begingroup + drv_errhelp "Valid commands are"& + " \displaystyle,"& + " \textstyle,"& + " \scriptstyle and"& + " \scriptscriptstyle."; + drv_errmessage (sty_str&" is not a valid math-style command"); + default + endgroup + fi +enddef; + +vardef check_position_left (suffix pos_sfx) (expr default)= + save pos_str; + string pos_str; + pos_str:=str pos_sfx; + if (pos_str="l"): + true + elseif (pos_str="r"): + false + else: + begingroup + drv_errhelp "Valid identifiers are l (left) and r (right)."; + drv_errmessage (pos_str&" is not a valid label position identifier"); + default + endgroup + fi +enddef; + +vardef check_mode_on (suffix status_sfx) (expr default)= + save status_str; + string status_str; + status_str:=str status_sfx; + if status_str="on": + true + elseif status_str="off": + false + else: + begingroup + drv_errhelp "Possible identifiers are on and off"; + drv_errmessage (status_str&" is not a valid status identifier"); + default + endgroup + fi +enddef; + +vardef drv_math_style (suffix typ_sfx) (expr sty_str)= + save typ_str, sty_idx; + string typ_str; + numeric sty_idx; + typ_str:=str typ_sfx; + if (typ_str<>"drv") + and (typ_str<>"jdg") + and (typ_str<>"ilb") + and (typ_str<>"dlb") + and (typ_str<>"plb"): + drv_errhelp "Valid identifiers are"& + " drv (derivation tree),"& + " jdg (judgment),"& + " ilb (inference label),"& + " dlb (delimiter label) and"& + " plb (phantom steps label)."; + drv_errmessage (sty_str&" is not a valid component identifier"); + else: + sty_idx:=check_math_style (sty_str, 0); + if typ_str="drv": + drv_sty:=sty_idx; + else: + forsuffixes sfx=scantokens (typ_str&"_sty"): + for idx=0 upto 3: + sfx[idx]:=min(idx+sty_idx, 3); + endfor + endfor + fi + fi +enddef; + +vardef drv_scale (suffix scl_sfx) (expr scl)= + save scl_str; + string scl_str; + scl_str:=str scl_sfx; + if scl_str="clr": + min_clr_scl:=scl; + elseif scl_str="prm": + prm_skp_scl:=scl; + elseif (scl_str="jdg") or (scl_str="jgm"): % "jgm" is deprecated + jdg_skp_scl:=scl; + elseif (scl_str="ilb") or (scl_str="lbl"): % "lbl" is deprecated + ilb_skp_scl:=scl; + else: + drv_errhelp "Valid identifiers are"& + " clr,"& + " prm,"& + " jdg and"& + " ilb."; + drv_errmessage (scl_str&" is not a valid scale identifier"); + fi +enddef; + +vardef drv_junction_style suffix sty_sfx= + drv_jct_sty:=check_junction_style (sty_sfx, drv_jct_sty); +enddef; + +vardef drv_alignment_style suffix sty_sfx= + drv_alg_sty:=check_alignment_style (sty_sfx, drv_alg_sty); +enddef; + +vardef drv_path_style (suffix typ_sfx, sty_sfx)= + save typ_str; + string typ_str; + typ_str:=str typ_sfx; + if typ_str="iln": + drv_iln_sty:=check_path_style (sty_sfx, drv_iln_sty); + elseif typ_str="phm": + drv_phm_sty:=check_path_style (sty_sfx, drv_phm_sty); + else: + drv_errhelp "Valid identifiers are"& + " iln (inference line) and"& + " phm (phantom steps path)."; + drv_errmessage (typ_str&" is not a valid path-type identifier"); + fi +enddef; + +vardef drv_labels_position_aux (suffix typ_sfx, pos_sfx)= + save typ_str, idt_str, pos_str; + string typ_str, idt_str, pos_str; + typ_str:=str typ_sfx; + if typ_str="ilb": + drv_left_ilb:=check_position_left (pos_sfx, drv_left_ilb); + elseif typ_str="dlb": + drv_left_dlb:=check_position_left (pos_sfx, drv_left_dlb); + elseif typ_str="plb": + drv_left_plb:=check_position_left (pos_sfx, drv_left_plb); + else: + drv_errhelp "Valid identifiers are"& + " ilb (inference label),"& + " dlb (delimiter label) and"& + " plb (phantom steps label)."; + drv_errmessage (typ_str&" is not a valid label-type identifier"); + fi +enddef; + +vardef drv_labels_position text ARG= + drv_labels_position_aux if pair ARG: ARG else: (ilb, ARG) fi; +enddef; + +vardef drv_roots_position suffix pos_sfx= + save pos_str; + string pos_str; + pos_str:=str pos_sfx; + if pos_str="t": + drv_bot_roots:=false; + elseif pos_str="b": + drv_bot_roots:=true; + else: + drv_errhelp "Valid identifiers are"& + " t (top) and"& + " b (bottom)."; + drv_errmessage (pos_str&" is not a valid root position identifier"); + fi +enddef; + +vardef drv_axis_reference suffix ref_sfx= + save ref_str; + string ref_str; + ref_str:=str ref_sfx; + if (ref_str<>"iln") and (ref_str<>"jdg"): + drv_errhelp "Valid identifiers are iln (inference line axis) and"& + " jdg (judgment math-axis)."; + drv_errmessage (ref_str&" is not a valid reference identifier"); + else: + drv_axis_ref:=ref_str; + fi +enddef; + +vardef drv_delimiter (suffix pos_sfx) (expr dlm_str)= + if check_position_left (pos_sfx, true): + drv_l_dlm:=dlm_str; + else: + drv_r_dlm:=dlm_str; + fi +enddef; + +vardef drv_left_delimiter expr dlm_str= + drv_delimiter (l, dlm_str); +enddef; + +vardef drv_right_delimiter expr dlm_str= + drv_delimiter (r, dlm_str); +enddef; + +vardef drv_box_mode suffix status_sfx= + drv_boxmode_on:=check_mode_on (status_sfx, drv_boxmode_on); +enddef; + +vardef drv_fraction_mode suffix status_sfx= + drv_fractionmode_on:=check_mode_on (status_sfx, drv_fractionmode_on); +enddef; + +vardef drv_proof_mode suffix status_sfx= + drv_proofmode_on:=check_mode_on (status_sfx, drv_proofmode_on); +enddef; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Default settings +% + +drv_font_size "\normalsize"; +drv_math_style (drv, "\displaystyle"); +drv_math_style (jdg, "\textstyle"); +drv_math_style (ilb, "\scriptstyle"); +drv_math_style (dlb, "\textstyle"); +drv_math_style (plb, "\textstyle"); +drv_scale (clr, 1); +drv_scale (prm, 1); +drv_scale (jdg, 1); +drv_scale (ilb, 1); +drv_junction_style 1; +drv_alignment_style c; +drv_path_style (iln, 1); +drv_path_style (phm, 3); +drv_labels_position (ilb, r); +drv_labels_position (dlb, l); +drv_labels_position (plb, l); +drv_roots_position b; +drv_axis_reference iln; +drv_left_delimiter "\lbrace"; +drv_right_delimiter "\rbrace"; +drv_box_mode off; +drv_fraction_mode on; +drv_proof_mode off; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% LaTeX inclusion macro +% +% \drv includes a picture file in such a way that the baseline of the included +% picture coincides with the baseline of the inclusion point. The code for \drv +% was suggested by Josselin Noirel on the fr.comp.text.tex usenet group. +% +% \usepackage{graphicx} +% \makeatletter +% \def\Gin@def@bp#1\relax#2#3{\gdef#2{#3}} +% \newsavebox{\graphicsbox} +% \newcommand*{\drv}[1]{% +% \sbox{\graphicsbox}{\includegraphics{#1}}% +% \raisebox{\Gin@lly bp}% +% {\usebox{\graphicsbox}}} +% \makeatother -- cgit v1.2.3