now every object is output in a LaTeX environment, not just proofs

[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 50338f5df7b89051193f660e605a2b70f8bd4d27..a37b0054574565b626a2af8ed5b6ea8f4e20ae5d 100644 (file)
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,18 +1,43 @@
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesPackage{matex}[2016/02/15 MaTeX Package]
+\RequirePackage{xcolor}
+\ExecuteOptions{}
+\ProcessOptions*
+
 \makeatletter
 
-\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
+\definecolor{ma@black}{HTML}{000000}
+\definecolor{ma@blue}{HTML}{00005F}
+\definecolor{ma@purple}{HTML}{3F005F}
+
+\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}
 
-\newtheorem{prop}{Proposition}
+\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
 
 \newcommand*\ObjLabel[1]{\label{obj:#1}}
 \newcommand*\ObjRef[1]{\ref{obj:#1}}
 
-\newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
+\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}}
+\newcommand*\ma@thehead[2]{\textbf{#1 (#2)}\\}
+\newcommand*\ma@theneck[1]{\textsl{#1}\\}
+
+\newenvironment{axiom}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Axiom}{#1}}{}
+\newenvironment{declaration}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Declaration}{#1}}{}
+\newenvironment{definition}[2]{}{}
+\newenvironment{proposition}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Proposition}{#1}}{}
+\newenvironment{proof}[2]{\ma@theneck{Proof}}{}
+\newenvironment{ma@step}[1]{\color{#1}}{\\}
 
-\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*\ma@tmp{}
+\newcommand*\ma@skip[4]{}
+\newcommand*\ma@next[5]{\def\ma@tmp{#5}\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*\@proc[1]{ #1}
+\newcommand*\ma@space{ }
+\newcommand*\ma@arg[1]{#1}
 
 \newcommand*\PROP{PROP}
 \newcommand*\CROP[1]{CROP}
@@ -22,16 +47,27 @@
 \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*\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}
 
-\def\@arg#1{, #1}
-\def\@stop{.\vskip10pt}
+\newcommand*\ma@with{ with }
+\newcommand*\ma@comma{, }
+\newcommand*\ma@stop{.\end{ma@step}}
+\newcommand*\ma@head[4]{\def\ma@tmp{#4}%
+   \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{#2}%
+   \else\begin{ma@step}{#3}\textbf{#4}%
+   \fi
+}
+\newcommand*\ma@tail{\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
 
-\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*\EXIT[1]{\ma@head{}{}{\ma@exit}{end} of block #1\ma@stop}
+\newcommand*\OPEN[3]{\ma@head{}{}{\ma@open}{#1} is this block #3\ma@stop}
+\newcommand*\PRIM[3]{\ma@head{}{}{\ma@prim}{#1} will have type #3\ma@stop}
+\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{\ma@fwd}{#1} has type #3\\}
+\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