X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Fmatex.sty;h=7d6ae277e8b678f41181428b31e309b2ab5a6a1e;hb=bedea63520c165e9445c15b09455e349c72e48a5;hp=50338f5df7b89051193f660e605a2b70f8bd4d27;hpb=ea6b4322051d3eb1794bfca3928f6e1773f971ba;p=helm.git

diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index 50338f5df..7d6ae277e 100644
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,37 +1,137 @@
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesPackage{matex}[2016/07/03 MaTeX Package]
+\RequirePackage{xcolor}
+\RequirePackage[lcgreekalpha]{stix}
+\ExecuteOptions{}
+\ProcessOptions*
+
+\newcommand*\neverindent{\setlength\parindent{0pt}}
+
 \makeatletter
 
-\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
+\definecolor{ma@black}{HTML}{000000}
+\definecolor{ma@blue}{HTML}{00005F}
+\definecolor{ma@purple}{HTML}{3F005F}
+\definecolor{ma@green}{HTML}{004F00}
+
+\newcommand*\ma@punct{ma@green}
+\newcommand*\ma@fwd{ma@black}
+\newcommand*\ma@open{ma@blue}
+\newcommand*\ma@exit{ma@blue}
+\newcommand*\ma@prim{ma@purple}
+\newcommand*\ma@qed{ma@blue}
+
+\newcommand*\ma@constr[1]{{\color{\ma@punct}#1}}
+\newcommand*\ma@thop[1]{\mathpunct{#1}\allowbreak}
 
-\newtheorem{prop}{Proposition}
+\newcommand*\ma@cast{\mathbin\ma@constr{:}}
+\newcommand*\ma@abbr{\mathrel\ma@constr{\eqdef}}
+\newcommand*\ma@prod{\mathord\ma@constr{\Pi}}
+\newcommand*\ma@arrw{\mathrel\ma@constr{\Rightarrow}}
+\newcommand*\ma@fall{\mathord\ma@constr{\forall}}
+\newcommand*\ma@impl{\mathrel\ma@constr{\supset}}
+\newcommand*\ma@case{\mathrel\ma@constr{\questeq}}
+\newcommand*\ma@caze{\mathrel\ma@constr{\mapsto}}
+\newcommand*\ma@pair{\mathbin\ma@constr{\mapsto}}
+\newcommand*\ma@cm{\ma@thop{\ma@constr{,}}}
+\newcommand*\ma@or{\mathbin\ma@constr{\vert}}
+\newcommand*\ma@op{\mathopen\ma@constr{(}}
+\newcommand*\ma@cp{\mathclose\ma@constr{)}\allowbreak}
+\newcommand*\ma@qm{\mathord\ma@constr{?}}
 
-\newcommand*\ObjLabel[1]{\label{obj:#1}}
-\newcommand*\ObjRef[1]{\ref{obj:#1}}
+%\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
+%\newcommand*\ObjLabel[1]{\label{obj:#1}\hypertarget{obj:#1}{}}
+%\newcommand*\ObjRef[1]{\hyperlink{obj:#1}{\ref*{obj:#1}}}
+%\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}}
 
-\newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
+\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*\@skip[2]{}
-\newcommand*\Next[3]{\def\@tmp{#3}\ifx\@tmp\empty #2\let\next=\@skip\else #1{#3}\let\next=\Next\fi\next #1#2}
+\newcommand*\setordlink[2]{\mathord{\ma@setlink{#1}{#2}}}
+\newcommand*\setopenlink[2]{\mathopen{\ma@setlink{#1}{#2}}}
+\newcommand*\setcloselink[2]{\mathclose{\ma@setlink{#1}{#2}}}
+\newcommand*\setpunctlink[2]{\mathpunct{\ma@setlink{#1}{#2}}}
+\newcommand*\setoplink[3]{\mathop{\ma@setlink{#1}{#2}#3}}
+\newcommand*\setbinlink[3]{\mathbin{\ma@setlink{#1}{#2}#3}}
+\newcommand*\setrellink[3]{\mathrel{\ma@setlink{#1}{#2}#3}}
 
-\newcommand*\@proc[1]{ #1}
+\newcommand*\ObjIncNode{}
+\newcommand*\ObjNode{}
 
-\newcommand*\PROP{PROP}
-\newcommand*\CROP[1]{CROP}
-\newcommand*\TYPE[1]{TYPE}
-\newcommand*\LREF[2]{#1}
-\newcommand*\GREF[2]{#1}
-\newcommand*\ABBR[3]{(D #1 #2 #3) }
-\newcommand*\ABST[2]{(I #1 #2) }
-\newcommand*\PROD[2]{(P #1 #2) }
-\newcommand*\APPL{(A)\Next\@proc\relax}
-\newcommand*\CASE[3]{(C #1 #2 #3)\Next\@proc\relax}
+\newcommand*\ma@thehead[4]{\ObjIncNode
+   \textbf{#1 \ObjNode:} (\ma@settarget{#3}{#4}) \textit{#2:}%
+   \neverindent\par
+}
+\newcommand*\ma@theneck[1]{\textit{#1:}\neverindent\par}
 
-\def\@arg#1{, #1}
-\def\@stop{.\vskip10pt}
+\newenvironment{assumption}[2]{\ma@thehead{Assumption}{has type}{#1}{#2}$}{$\par}
+\newenvironment{axiom}[2]{\ma@thehead{Axiom}{states}{#1}{#2}$}{$\par}
+\newenvironment{declaration}[2]{\ma@thehead{Definition}{of type}{#1}{#2}$}{$\par}
+\newenvironment{definition}[2]{\ma@theneck{is defined as}$}{$\par}
+\newenvironment{proposition}[2]{\ma@thehead{Proposition}{stating}{#1}{#2}$}{$\par}
+\newenvironment{proof}[2]{\ma@theneck{is proved by}}{\par}
+\newenvironment{ma@step}[1]{\color{#1}}{\par}
 
-\newcommand*\DECL[3]{\textbf{#1} : #3\vskip10pt}
-\newcommand*\PRIM{}
-\newcommand*\BODY[1]{is #1\vskip10pt}
-\newcommand*\STEP[1]{by #1\Next\@arg\@stop}
-\newcommand*\DEST[1]{by cases on #1\Next\@arg\@stop}
+\newcommand*\ma@tmp{}
+\newcommand*\ma@last[4]{#4}
+\newcommand*\ma@list[5]{\def\ma@tmp{#5}%
+   \ifx\ma@tmp\empty\let\ma@tmp=\ma@last\else #1#2{#5}\let\ma@tmp=\ma@list\fi
+   \ma@tmp{#3}{#2}{#3}{#4}%
+}
+\newcommand*\ma@arg[1]{#1}
+\newcommand*\ma@args{\ma@op\ma@list\relax\ma@arg\ma@cm\ma@cp}
+\newcommand*\ma@cases{\ma@list\relax\ma@arg\ma@or\relax}
+\newcommand*\ma@bind{\ma@thop{}}
+\newcommand*\ma@skip[1]{}
+
+\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@op\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3\ma@cp\ma@bind}
+\newcommand*\ABST[3]{\ma@op\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind}
+\newcommand*\PROD[3]{\def\ma@tmp{#2}%
+   \ifx\ma@tmp\empty #3\ma@arrw\else
+   \ma@op\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi
+}
+\newcommand*\FALL[3]{\def\ma@tmp{#2}%
+   \ifx\ma@tmp\empty #3\ma@impl\else
+   \ma@op\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi
+}
+\newcommand*\APPL[1]{#1\ma@args}
+\newcommand*\CASE[3]{#3\ma@case\ma@cases}
+\newcommand*\CAZE[3]{#3\ma@caze\ma@op\ma@qm\ma@cast #2\ma@cp\ma@cases}
+\newcommand*\PAIR[2]{#1\ma@pair #2}
+
+\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}$\mathbf{\ma@setopttarget{#2}{#3}}$%
+   \else\begin{ma@step}{#4}$\mathbf{\ma@setopttarget{#5}{#6}}$%
+   \fi
+}
+\newcommand*\ma@tail{\ma@list\ma@with\ma@term\ma@comma\ma@stop}
+\newcommand*\ma@type[1]{\def\ma@tmp{#1}%
+   \ifx\ma@tmp\empty\mathrm{(omitted)}\else #1\fi
+}
+
+\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 $\ma@type{#3}$\ma@stop}
+\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type $\ma@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
+
+\endinput