]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_notation/doc/reserved.sty
tex macros, checked in disambiguation section from whelp paper
[helm.git] / helm / ocaml / cic_notation / doc / reserved.sty
1 %%
2 %% This is file `reserved.sty',
3 %% generated with the docstrip utility.
4 %%
5 %% The original source files were:
6 %%
7 %% semantic.dtx  (with options: `allOptions,reservedWords')
8 %% 
9 %% IMPORTANT NOTICE:
10 %% 
11 %% For the copyright see the source file.
12 %% 
13 %% Any modified versions of this file must be renamed
14 %% with new filenames distinct from reserved.sty.
15 %% 
16 %% For distribution of the original source see the terms
17 %% for copying and modification in the file semantic.dtx.
18 %% 
19 %% This generated file may be distributed as long as the
20 %% original source files, as listed above, are part of the
21 %% same distribution. (The sources need not necessarily be
22 %% in the same archive or directory.)
23 %%
24 %% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
25 %%                             Arne John Glenstrup
26 %%
27 \expandafter\ifx\csname sem@nticsLoader\endcsname\relax
28   \PackageError{semantic}{%
29     This file should not be loaded directly}
30     {%
31       This file is an option of the semantic package.  It should not be
32         loaded directly\MessageBreak
33       but by using \protect\usepackage{semantic} in your document
34         preamble.\MessageBreak
35       No commands are defined.\MessageBreak
36      Type <return> to proceed.
37     }%
38 \else
39 \TestForConflict{\reservestyle,\@reservestyle,\setreserved,\<}
40 \TestForConflict{\@parseDefineReserved,\@xparseDefineReserved}
41 \TestForConflict{\@defineReserved,\@xdefineReserved}
42 \newcommand{\reservestyle}[3][]{
43   \newcommand{#2}{\@parseDefineReserved{#1}{#3}}
44    \expandafter\expandafter\expandafter\def
45      \expandafter\csname set\expandafter\@gobble\string#2\endcsname##1%
46    {#1{#3{##1}}}}
47 \newtoks\@@spacing
48 \newtoks\@@formating
49 \def\@parseDefineReserved#1#2{%
50   \@ifnextchar[{\@xparseDefineReserved{#2}}%
51      {\@xparseDefineReserved{#2}[#1]}}
52 \def\@xparseDefineReserved#1[#2]#3{%
53   \@@formating{#1}%
54   \@@spacing{#2}%
55   \expandafter\@defineReserved#3,\end
56 }
57 \def\@defineReserved#1,{%
58   \@ifnextchar\end
59   {\@xdefineReserved #1[]\END\@gobble}%
60   {\@xdefineReserved#1[]\END\@defineReserved}}
61 \def\@xdefineReserved#1[#2]#3\END{%
62   \def\reserved@a{#2}%
63   \ifx \reserved@a\empty \toks0{#1}\else \toks0{#2} \fi
64     \expandafter\edef\csname\expandafter<#1>\endcsname
65     {\the\@@formating{\the\@@spacing{\the\toks0}}}}
66 \def\setreserved#1>{%
67   \expandafter\let\expandafter\reserved@a\csname<#1>\endcsname
68   \@ifundefined{reserved@a}{\PackageError{Semantic}
69       {``#1'' is not defined as a reserved word}%
70       {Before referring to a name as a reserved word, it %
71       should be defined\MessageBreak using an appropriate style
72       definer.  A style definer is defined \MessageBreak
73       using \protect\reservestyle.\MessageBreak%
74       Type <return> to proceed --- nothing will be set.}}%
75   {\reserved@a}}
76 \let\<=\setreserved
77 \fi
78 \endinput
79 %%
80 %% End of file `reserved.sty'.