- matex: we separate axioms (propositions) and assumptions (other)

[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 b01223fefec60774fc182dabebde22033d01edea..7d6ae277e8b678f41181428b31e309b2ab5a6a1e 100644 (file)
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,33 +1,43 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{matex}[2016/06/21 MaTeX Package]
+\ProvidesPackage{matex}[2016/07/03 MaTeX Package]
 \RequirePackage{xcolor}
 \RequirePackage[lcgreekalpha]{stix}
 \ExecuteOptions{}
 \ProcessOptions*
 
-\makeatletter
+\newcommand*\neverindent{\setlength\parindent{0pt}}
 
-\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}
-\newcommand*\ma@caze{\mathrel\mapsto}
-\newcommand*\ma@pair{\mathbin\mapsto}
+\makeatletter
 
 \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*\neverindent{\setlength\parindent{0pt}}
+\newcommand*\ma@constr[1]{{\color{\ma@punct}#1}}
+\newcommand*\ma@thop[1]{\mathpunct{#1}\allowbreak}
+
+\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*\setlabel[1]{\protected@edef\@currentlabel{#1}}
 %\newcommand*\ObjLabel[1]{\label{obj:#1}\hypertarget{obj:#1}{}}
@@ -54,14 +64,18 @@
 \newcommand*\ObjIncNode{}
 \newcommand*\ObjNode{}
 
-\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{proof}[2]{\ma@theneck{Proof}}{\par}
+\newcommand*\ma@thehead[4]{\ObjIncNode
+   \textbf{#1 \ObjNode:} (\ma@settarget{#3}{#4}) \textit{#2:}%
+   \neverindent\par
+}
+\newcommand*\ma@theneck[1]{\textit{#1:}\neverindent\par}
+
+\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*\ma@tmp{}
@@ -70,13 +84,8 @@
    \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@thop[1]{\mathpunct{#1}\allowbreak}
-\newcommand*\ma@cm{\ma@thop{,}}
-\newcommand*\ma@or{\mathbin\vert}
-\newcommand*\ma@cp{)\allowbreak}
-\newcommand*\ma@qm{\mathord{?}}
 \newcommand*\ma@arg[1]{#1}
-\newcommand*\ma@args{(\ma@list\relax\ma@arg\ma@cm\ma@cp}
+\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]{}
@@ -86,19 +95,19 @@
 \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*\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@prod\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
+   \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@fall\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
+   \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@qm\ma@cast #2)\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$}