MaTeX:

[helm.git] / matita / components / binaries / matex / test / matex.sty

diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index a25d051cbca3668539d798844960509d9a4a527c..119dffd26e5f9cbaf67fb9a5b314776dc5beed17 100644 (file)
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,11 +1,20 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{matex}[2016/05/22 MaTeX Package]
+\ProvidesPackage{matex}[2016/06/05 MaTeX Package]
 \RequirePackage{xcolor}
+\RequirePackage{stix}
 \ExecuteOptions{}
 \ProcessOptions*
 
 \makeatletter
 
+\newcommand*\ma@cast{\mathbin:}
+\newcommand*\ma@abbr{\mathrel\eqdef}
+\newcommand*\ma@prod{\mathord\Pi}
+\newcommand*\ma@arrw{\mathrel\Rightarrow}
+\newcommand*\ma@fall{\mathord\forall}
+\newcommand*\ma@impl{\mathrel\supset}
+\newcommand*\ma@case{\mathrel\questeq}
+
 \definecolor{ma@black}{HTML}{000000}
 \definecolor{ma@blue}{HTML}{00005F}
 \definecolor{ma@purple}{HTML}{3F005F}
@@ -25,6 +34,17 @@
 
 \newcommand*\ma@settarget[2]{\hypertarget{obj:#2}{#1}}
 \newcommand*\ma@setlink[2]{\hyperlink{obj:#2}{#1}}
+\newcommand*\ma@setopttarget[2]{\def\ma@tmp{#2}%
+   \mathord{\ifx\ma@tmp\empty #1\else\ma@settarget{#1}{#2}\fi}%
+}
+\newcommand*\ma@setoptlink[2]{\def\ma@tmp{#2}%
+   \mathord{\ifx\ma@tmp\empty #1\else\ma@setlink{#1}{#2}\fi}%
+}
+
+\newcommand*\setordlink[2]{\mathord{\ma@setlink{#1}{#2}}}
+\newcommand*\setoplink[2]{\mathop{\ma@setlink{#1}{#2}}}
+\newcommand*\setbinlink[2]{\mathbin{\ma@setlink{#1}{#2}}}
+\newcommand*\setrellink[2]{\mathrel{\ma@setlink{#1}{#2}}}
 
 \newcommand*\ObjIncNode{}
 \newcommand*\ObjNode{}
@@ -32,10 +52,10 @@
 \newcommand*\ma@thehead[3]{\ObjIncNode\textbf{#1 \ObjNode(\ma@settarget{#2}{#3})}\neverindent\par}
 \newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par}
 
-\newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}}{\par}
-\newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}}{\par}
-\newenvironment{definition}[2]{}{\par}
-\newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}}{\par}
+\newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}$}{$\par}
+\newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}$}{$\par}
+\newenvironment{definition}[2]{$}{$\par}
+\newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}$}{$\par}
 \newenvironment{proof}[2]{\ma@theneck{Proof}}{\par}
 \newenvironment{ma@step}[1]{\color{#1}}{\par}
 
@@ -45,44 +65,52 @@
    \ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi
    \ma@tmp #3#2#3#4%
 }
-
-\newcommand*\ma@space{ }
+\newcommand*\ma@thop[1]{\mathop{#1}\allowbreak}
+\newcommand*\ma@cm{\ma@thop{,}}
+\newcommand*\ma@or{\mathbin\vert}
+\newcommand*\ma@cp{)\allowbreak}
 \newcommand*\ma@arg[1]{#1}
-
-\newcommand*\ma@setopttarget[2]{\def\ma@tmp{#2}%
-   \ifx\ma@tmp\empty #1\else\ma@settarget{#1}{#2}\fi
+\newcommand*\ma@args{(\ma@next\relax\ma@arg\ma@cm\ma@cp}
+\newcommand*\ma@cases{\ma@next\relax\ma@arg\ma@or\relax}
+\newcommand*\ma@bind{\ma@thop{}}
+
+\newcommand*\PROP{\mathord\mathrm{PROP}}
+\newcommand*\CROP[1]{\mathord\mathrm{CROP}}
+\newcommand*\TYPE[1]{\mathord\mathrm{TYPE}}
+\newcommand*\LREF[2]{\ma@setoptlink{#1}{#2}}
+\newcommand*\GREF[2]{\ma@setoptlink{\mathrm{#1}}{#2}}
+\newcommand*\ABBR[4]{(\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3)\ma@bind}
+\newcommand*\ABST[3]{(\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind}
+\newcommand*\PROD[3]{\def\ma@tmp{#2}%
+   \ifx\ma@tmp\empty #3\ma@arrw\else
+   (\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
 }
-
-\newcommand*\PROP{PROP}
-\newcommand*\CROP[1]{CROP}
-\newcommand*\TYPE[1]{TYPE}
-\newcommand*\LREF[2]{\def\ma@tmp{#2}%
-   \ifx\ma@tmp\empty #1\else\ma@setlink{#1}{#2}\fi
+\newcommand*\FALL[3]{\def\ma@tmp{#2}%
+   \ifx\ma@tmp\empty #3\ma@impl\else
+   (\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
 }
-\newcommand*\GREF[2]{\ma@setlink{#1}{#2}}
-\newcommand*\ABBR[4]{(D \ma@setopttarget{#1}{#2} #3 #4) }
-\newcommand*\ABST[3]{(I \ma@setopttarget{#1}{#2} #3) }
-\newcommand*\PROD[3]{(P \ma@setopttarget{#1}{#2} #3) }
-\newcommand*\APPL{(A)\ma@next\ma@space\ma@arg\ma@space\relax}
-\newcommand*\CASE[3]{(C #1 #2 #3)\ma@next\ma@space\ma@arg\ma@space\relax}
+\newcommand*\APPL[1]{#1\ma@args}
+\newcommand*\CASE[3]{(#3\ma@cast #1)\ma@case\ma@cases}
+\newcommand*\NONE{\mathrm{(omitted)}}
 
+\newcommand*\ma@term[1]{$#1$}
 \newcommand*\ma@with{ with }
 \newcommand*\ma@comma{, }
 \newcommand*\ma@stop{.\end{ma@step}}
 \newcommand*\ma@head[6]{\def\ma@tmp{#5}%
-   \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{\ma@setopttarget{#2}{#3}}%
-   \else\begin{ma@step}{#4}\textbf{\ma@setopttarget{#5}{#6}}%
+   \ifx\ma@tmp\empty\begin{ma@step}{#1}$\mathbf{\ma@setopttarget{#2}{#3}}$%
+   \else\begin{ma@step}{#4}$\mathbf{\ma@setopttarget{#5}{#6}}$%
    \fi
 }
-\newcommand*\ma@tail{\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
+\newcommand*\ma@tail{\ma@next\ma@with\ma@term\ma@comma\ma@stop}
 
-\newcommand*\EXIT[1]{\ma@head{}{}{}{\ma@exit}{end}{} of block #1\ma@stop}
+\newcommand*\EXIT[1]{\ma@head{\ma@exit}{end}{}{}{}{} of block #1\ma@stop}
 \newcommand*\OPEN[3]{\ma@head{}{}{}{\ma@open}{#1}{#2} is this block #3\ma@stop}
-\newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type #3\ma@stop}
-\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type #3\par}
-\newcommand*\BODY[1]{being #1\ma@stop}
-\newcommand*\STEP[1]{by #1\ma@tail}
-\newcommand*\DEST[1]{by cases on #1\ma@tail}
+\newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type $#3$\ma@stop}
+\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type $#3$\par}
+\newcommand*\BODY[1]{being $#1$\ma@stop}
+\newcommand*\STEP[1]{by $#1$\ma@tail}
+\newcommand*\DEST[1]{by cases on $#1$\ma@tail}
 
 \makeatother