path: root/Master/texmf-dist/doc/metapost/drv/sample/drv.mp

%% 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.
% <laurent.mehats@gmail.com>
%
% This work consists of the file drv.mp


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% User's macros summary
%
%
% * Judgment & inference declarations
% ===================================
%
%   jgm <nat> <str list>
%	<nat>		judgment index
%	<str list>	sub-judgments math-mode LaTeX code
%
%   nfr <nat> (<nat list>) (<str>, <id>)
%	<nat>		inference index
%	<nat list>	list of premise indices
%	<str>		inference label math-mode LaTeX code
%	<id>		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 <nat 1> (<nat 2>, <id>)
%	<nat 1>		index of the origin judgment
%	<nat 2>		number of phantom steps
%	<id>		phantom steps path-style identifier
%			(0, 1, 2, 3, 4, 5, 6 or _)
%
%   Nfr <nat> (<nat list>) (<str 1>, <str 2>, <str 3>, <id>)
%	<nat>		inference index
%	<nat list>	list of premise indices
%	<str 1>		inference label math-mode LaTeX code
%	<str 2>		left delimiter label math-mode LaTeX code
%	<str 3>		right delimiter label math-mode LaTeX code
%	<id>		inference line style identifier
%			(0, 1, 2, 3, 4, 5, 6 or _)
%
%   Mvd <nat 1> (<nat 2>, <str 1>, <str 2>, <id>)
%	<nat 1>		index of the origin judgment
%	<nat 2>		number of phantom steps
%	<str 1>		left label math-mode LaTeX code
%	<str 2>		right label math-mode LaTeX code
%	<id>		phantom steps path-style identifier
%			(0, 1, 2, 3, 4, 5, 6 or _)
%
%   NFR <nat> (<nat list>) (<str 1>, <str 2>, <str 3>, <str 4>)
%     (<id 1>, <id 2>, <id 3>)
%	<nat>		inference index
%	<nat list>	list of premise indices
%	<str 1>		left inference label math-mode LaTeX code
%	<str 2>		right inference label math-mode LaTeX code
%	<str 3>		left delimiter label math-mode LaTeX code
%	<str 4>		right delimiter label math-mode LaTeX code
%	<id 1>		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)
%	<id 2>		alignment style identifier (l, c, r, u or _)
%			  l	left
%			  c	centered
%			  r	right
%			  u	user specified (tricky)
%			  _	default (set by drv_alignment_style)
%	<id 3>		inference line style identifier
%			(0, 1, 2, 3, 4, 5, 6 or _)
%
%   MVD <nat 1> (<nat 2>, <str 1>, <str 2>, <id 1> <id 2>)
%	<nat 1>		index of the origin judgment
%	<nat 2>		number of phantom steps
%	<str 1>		left label math-mode LaTeX code
%	<str 2>		right label math-mode LaTeX code
%	<id 1>		alignment style identifier (l, c, r, u or _)
%	<id 2>		phantom steps path-style identifier
%			(0, 1, 2, 3, 4, 5, 6 or _)
%
%   NFR_opt <nat> (<nat list>) (<str list 1>) (<str list 2>)
%     (<id 1>, <id 2>, <id 3>)
%	<nat>		inference index
%	<nat list>	list of premise indices
%	<str list 1>	list of inference labels math-mode LaTeX code
%	<str list 2>	list of delimiter labels math-mode LaTeX code
%	<id 1>		junction style identifier (0, 1, 2, 3 or _)
%	<id 2>		alignment style identifier (l, c, r, u or _)
%	<id 3>		inference line style identifier
%			(0, 1, 2, 3, 4, 5, 6 or _)
%
%   MVD_opt <nat 1> (<nat 2>) (<str list>) (<id 1> <id 2>)
%	<nat 1>		index of the origin judgment
%	<nat 2>		number of phantom steps
%	<str list>	list of labels math-mode LaTeX code
%	<id 1>		alignment style identifier (l, c, r or u)
%	<id 2>		phantom steps path-style identifier
%			(0, 1, 2, 3, 4, 5, 6 or _)
%
% * Tunings
% =========
%
%   drv_font_size <str>
%	<str>		LaTeX font-size command
%			  "\tiny"
%			  "\scriptsize"
%			  "\footnotesize"
%			  "\small"
%			  "\normalsize"
%			  "\large"
%			  "\Large"
%			  etc.
%
%   drv_math_style (<id>, <str>)
%	<id>		component identifier (drv, jdg, ilb, dlb or plb)
%			  drv	derivation trees
%			  jdg	judgments
%			  ilb	inference labels
%			  dlb	delimiter labels
%			  plb	phantom steps labels
%	<str>		LaTeX math-style command
%
%   drv_scale (<id>, <float>)
%	<id>		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)
%	<float>		scale value
%
%   drv_junction_style <id>
%	<id>		junction style identifier (0, 1 or 2)
%			  0	``fully-interlacing''
%			  1	``semi-interlacing''
%			  2	``non-interlacing''
%
%   drv_alignment_style <id>
%	<id>		alignment style identifier (l, c or r)
%			  l	left
%			  c	centered
%			  r	right
%
%   drv_path_style (<id 1>, <id 2>)
%	<id 1>		path-type identifier (iln or phm)
%			  iln	inference lines
%			  phm	phantom steps paths
%	<id 2>		path-style identifier (0, 1, 2, 3, 4, 5 or 6)
%
%   drv_labels_position (<id 1>, <id 2>)
%	<id 1>		label-type identifier (ilb, plb or dlb)
%			  ilb	inference labels
%			  dlb	delimiter labels
%			  plb	phantom steps labels
%	<id 2>		position identifier (l or r)
%			  l	left
%			  r	right
%
%   drv_roots_position <id>
%	<id>		position identifier (t or b)
%			  t	top
%			  b	bottom
%
%   drv_axis_reference <id>
%	<id>		reference identifier (iln or jdg)
%			  iln	root inference line axis
%			  jdg	root judgment math-axis
%
%   drv_left_delimiter <str>
%	<str>		left delimiter math-mode LaTeX code
%			  "("	$($
%			  "["	$[$
%			  "\lbrace"	$\lbrace$
%			  "\langle"	$\langle$
%			  etc.
%
%   drv_right_delimiter <str>
%	<str>		right delimiter math-mode LaTeX code
%			  ")"
%			  "]"
%			  "\rbrace"
%			  "\rangle"
%			  etc.
%
%   drv_box_mode <id>
%	<id>		status identifier (on or off)
%			  on
%			  off
%
%   drv_fraction_mode <id>
%	<id>		status identifier (on or off)
%			  on
%			  off
%
%   drv_proof_mode <id>
%	<id>		status identifier (on or off)
%			  on
%			  off
%
% * Derivation tree pictures
% ==========================
%
%   drv_bbox <nat>
%	<nat>		sub-tree root index
%
%   drv_axis (<id>, <nat>)
%	<id>		reference type identifier (iln, jdg or dlm)
%			  iln	inference line axis
%			  jdg	judgment math-axis
%			  dlm	delimiter axis
%	<nat>		reference index
%
%   <path> drv_styled <id>
%	<path>		MetaPost path expression
%	<id>		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]	<nice explanation>
% jdg_skp[s]	<nice explanation>
% ilb_skp[s]	<nice explanation>
% plb_skp[s]	<nice explanation>
%

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