]> matita.cs.unibo.it Git - helm.git/blobdiff - components/tactics/doc/tdiagram.sty
branch for universe
[helm.git] / components / tactics / doc / tdiagram.sty
diff --git a/components/tactics/doc/tdiagram.sty b/components/tactics/doc/tdiagram.sty
new file mode 100644 (file)
index 0000000..02202b3
--- /dev/null
@@ -0,0 +1,166 @@
+%%
+%% This is file `tdiagram.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `allOptions,Tdiagram')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from tdiagram.sty.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file semantic.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
+%%
+%% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
+%%                             Arne John Glenstrup
+%%
+\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
+  \PackageError{semantic}{%
+    This file should not be loaded directly}
+    {%
+      This file is an option of the semantic package.  It should not be
+        loaded directly\MessageBreak
+      but by using \protect\usepackage{semantic} in your document
+        preamble.\MessageBreak
+      No commands are defined.\MessageBreak
+     Type <return> to proceed.
+    }%
+\else
+\TestForConflict{\@getSymbol,\@interpreter,\@parseArg,\@program}
+\TestForConflict{\@putSymbol,\@saveBeforeSymbolMacro,\compiler}
+\TestForConflict{\interpreter,\machine,\program,\@compiler}
+\newif\if@@Left
+\newif\if@@Up
+\newcount\@@xShift
+\newcount\@@yShift
+\newtoks\@@symbol
+\newtoks\@@tempSymbol
+\newcommand{\compiler}[1]{\@compiler#1\end}
+\def\@compiler#1,#2,#3\end{%
+  \if@@Nested %
+    \if@@Up %
+    \@@yShift=40 \if@@Left \@@xShift=-50 \else \@@xShift=-30 \fi
+    \else%
+      \@@yShift=20 \@@xShift =0 %
+    \fi%
+  \else%
+    \@@yShift=40 \@@xShift=-40%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(1,0){80}}%
+    \put(0,-20){\line(1,0){30}}%
+    \put(50,-20){\line(1,0){30}}%
+    \put(30,-40){\line(1,0){20}}%
+    \put(0,0){\line(0,-1){20}}%
+    \put(80,0){\line(0,-1){20}}%
+    \put(30,-20){\line(0,-1){20}}%
+    \put(50,-20){\line(0,-1){20}}%
+    \put(30,-20){\makebox(20,20){$\rightarrow$}} %
+   {\@@Uptrue \@@Lefttrue \@parseArg(0,-20)(5,-20)#1\end}%
+   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+   {\@@Uptrue \@@Leftfalse \@parseArg(80,-20)(55,-20)#3\end}%
+   {\@@Upfalse \@@Lefttrue \@parseArg(50,-40)(30,-40)#2\end}%
+   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
+  }%
+}
+\newcommand{\interpreter}[1]{\@interpreter#1\end}
+\def\@interpreter#1,#2\end{%
+  \if@@Nested %
+    \if@@Up %
+    \@@yShift=40 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
+    \else%
+      \@@yShift=0 \@@xShift =0 %
+    \fi%
+  \else%
+    \@@yShift=40 \@@xShift=10%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(-1,0){20}}%
+    \put(0,-40){\line(-1,0){20}}%
+    \put(0,0){\line(0,-1){40}}%
+    \put(-20,0){\line(0,-1){40}}%
+   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-20)#1\end}%
+   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+   {\@@Upfalse \@@Lefttrue \@parseArg(0,-40)(-20,-40)#2\end}%
+   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
+    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
+  }%
+}
+\newcommand{\program}[1]{\@program#1\end}
+\def\@program#1,#2\end{%
+  \if@@Nested %
+    \if@@Up %
+    \@@yShift=0 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
+    \else%
+      \PackageError{semantic}{%
+        A program cannot be at the bottom}
+        {%
+          You have tried to use a \protect\program\space as the
+          bottom\MessageBreak parameter to \protect\compiler,
+          \protect\interpreter\space or \protect\program.\MessageBreak
+         Type <return> to proceed --- Output can be distorted.}%
+    \fi%
+  \else%
+    \@@yShift=0 \@@xShift=10%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(-1,0){20}}%
+    \put(0,0){\line(0,1){30}}%
+    \put(-20,0){\line(0,1){30}}%
+    \put(-10,30){\oval(20,20)[t]}%
+    \@putSymbol[#1]{-20,20}%
+   {\@@Upfalse \@@Lefttrue \@parseArg(0,0)(-20,0)#2\end}%
+  }%
+}
+\newcommand{\machine}[1]{%
+  \if@@Nested %
+    \if@@Up %
+      \PackageError{semantic}{%
+        A machine cannot be at the top}
+        {%
+          You have tried to use a \protect\machine\space as a
+          top\MessageBreak parameter to \protect\compiler or
+          \protect\interpreter.\MessageBreak
+         Type <return> to proceed --- Output can be distorted.}%
+       \else \@@yShift=0 \@@xShift=0
+    \fi%
+  \else%
+    \@@yShift=20 \@@xShift=10%
+    \fi
+  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
+    \put(0,0){\line(-1,0){20}} \put(-20,0){\line(3,-5){10}}
+    \put(0,0){\line(-3,-5){10}}%
+   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-15)#1\end}%
+  }%
+}
+\def\@parseArg(#1)(#2){%
+  \@ifNextMacro{\@doSymbolMacro(#1)(#2)}{\@getSymbol(#2)}}
+\def\@getSymbol(#1)#2\end{\@putSymbol[#2]{#1}}
+\def\@doSymbolMacro(#1)(#2)#3{%
+  \@ifnextchar[{\@saveBeforeSymbolMacro(#1)(#2)#3}%
+               {\@symbolMacro(#1)(#2)#3}}
+\def\@saveBeforeSymbolMacro(#1)(#2)#3[#4]#5\end{%
+  \@@tempSymbol={#4}%
+  \@@Nestedtrue\put(#1){#3#5}%
+  \@putSymbol[\the\@@tempSymbol]{#2}}
+\def\@symbolMacro(#1)(#2)#3\end{%
+  \@@Nestedtrue\put(#1){#3}%
+  \@putSymbol{#2}}
+\newcommand{\@putSymbol}[2][\the\@@symbol]{%
+  \global\@@symbol=\expandafter{#1}%
+  \put(#2){\makebox(20,20){\texttt{\the\@@symbol}}}}
+\fi
+\endinput
+%%
+%% End of file `tdiagram.sty'.