X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Ftactics%2Fdoc%2Freserved.sty;fp=components%2Ftactics%2Fdoc%2Freserved.sty;h=c0d56b8aa41eef8e6be25b485ea548e500dac901;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/components/tactics/doc/reserved.sty b/components/tactics/doc/reserved.sty
new file mode 100644
index 000000000..c0d56b8aa
--- /dev/null
+++ b/components/tactics/doc/reserved.sty
@@ -0,0 +1,80 @@
+%%
+%% This is file `reserved.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `allOptions,reservedWords')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from reserved.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{\reservestyle,\@reservestyle,\setreserved,\<}
+\TestForConflict{\@parseDefineReserved,\@xparseDefineReserved}
+\TestForConflict{\@defineReserved,\@xdefineReserved}
+\newcommand{\reservestyle}[3][]{
+  \newcommand{#2}{\@parseDefineReserved{#1}{#3}}
+   \expandafter\expandafter\expandafter\def
+     \expandafter\csname set\expandafter\@gobble\string#2\endcsname##1%
+   {#1{#3{##1}}}}
+\newtoks\@@spacing
+\newtoks\@@formating
+\def\@parseDefineReserved#1#2{%
+  \@ifnextchar[{\@xparseDefineReserved{#2}}%
+     {\@xparseDefineReserved{#2}[#1]}}
+\def\@xparseDefineReserved#1[#2]#3{%
+  \@@formating{#1}%
+  \@@spacing{#2}%
+  \expandafter\@defineReserved#3,\end
+}
+\def\@defineReserved#1,{%
+  \@ifnextchar\end
+  {\@xdefineReserved #1[]\END\@gobble}%
+  {\@xdefineReserved#1[]\END\@defineReserved}}
+\def\@xdefineReserved#1[#2]#3\END{%
+  \def\reserved@a{#2}%
+  \ifx \reserved@a\empty \toks0{#1}\else \toks0{#2} \fi
+    \expandafter\edef\csname\expandafter<#1>\endcsname
+    {\the\@@formating{\the\@@spacing{\the\toks0}}}}
+\def\setreserved#1>{%
+  \expandafter\let\expandafter\reserved@a\csname<#1>\endcsname
+  \@ifundefined{reserved@a}{\PackageError{Semantic}
+      {``#1'' is not defined as a reserved word}%
+      {Before referring to a name as a reserved word, it %
+      should be defined\MessageBreak using an appropriate style
+      definer.  A style definer is defined \MessageBreak
+      using \protect\reservestyle.\MessageBreak%
+      Type <return> to proceed --- nothing will be set.}}%
+  {\reserved@a}}
+\let\<=\setreserved
+\fi
+\endinput
+%%
+%% End of file `reserved.sty'.