% \iffalse meta-comment
% An Infrastructure for Semantic Macros and Module Scoping
% Copyright (c) 2019 Michael Kohlhase, all rights reserved
%                this file is released under the
%                LaTeX Project Public License (LPPL)
% 
% The original of this file is in the public repository at 
% http://github.com/sLaTeX/sTeX/
%
% TODO update copyright  
%
%<*driver>
\def\libfolder#1{../../lib/#1}
\input{../../doc/stex-docheader}

\begin{document}
  \DocInput{\jobname.dtx}
\end{document}
%</driver>
% \fi
%
% \title{ \sTeX-Statements
% 	\thanks{Version {\fileversion} (last revised {\filedate})} 
% }
%
% \author{Michael Kohlhase, Dennis Müller\\
% 	FAU Erlangen-Nürnberg\\
% 	\url{http://kwarc.info/}
% }
%
% \maketitle
%
%\ifinfulldoc\else
% This is the documentation for the \pkg{stex-statements} package.
% For a more high-level introduction, 
%  see \href{\basedocurl/manual.pdf}{the \sTeX Manual} or the
% \href{\basedocurl/stex.pdf}{full \sTeX documentation}.
%
% \input{../../doc/packages/stex-statements}
% \fi
%
% \begin{documentation}\label{pkg:statements:doc}
% \changes{3.1.0}{2022/02/28}{Added \detokenize{\definiendum} and related macros to \detokenize{sparagraph},
%   if \detokenize{type=symdoc}}
%
% Code related to statements, e.g. definitions, theorems
%
% \section{Macros and Environments}\label{pkg:statements:doc:macros}
%
% \begin{environment}{symboldoc}
%    \begin{syntax} \cs{begin}\Arg{symboldoc}\Arg{symbols} \meta{text} \cs{end}\Arg{symboldoc} \end{syntax}
%  Declares \meta{text} to be a (natural language, encyclopaedic) description
% of \Arg{symbols} (a comma separated list of symbol identifiers).
% \end{environment}
%
% \end{documentation}
%
% \begin{implementation}\label{pkg:statements:impl}
%
% \section{\sTeX-Statements Implementation}
%
%    \begin{macrocode}
%<*package>

%%%%%%%%%%%%%   features.dtx   %%%%%%%%%%%%%

%<@@=stex_statements>
%    \end{macrocode}
%
% Warnings and error messages
%
%    \begin{macrocode}

%    \end{macrocode}
% \begin{macro}{\titleemph}
%    \begin{macrocode}
\def\titleemph#1{\textbf{#1}}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Definitions}
%
% \begin{macro}{definiendum}
%    \begin{macrocode}
\keys_define:nn {stex / definiendum }{
  pre     .tl_set:N     = \l_@@_definiendum_pre_tl,
  post    .tl_set:N     = \l_@@_definiendum_post_tl,
  root    .str_set_x:N  = \l_@@_definiendum_root_str,
  gfa     .str_set_x:N  = \l_@@_definiendum_gfa_str
}
\cs_new_protected:Nn \_@@_definiendum_args:n {
  \str_clear:N \l_@@_definiendum_root_str
  \tl_clear:N \l_@@_definiendum_post_tl
  \str_clear:N \l_@@_definiendum_gfa_str
  \keys_set:nn { stex / definiendum }{ #1 }
}
\NewDocumentCommand \definiendum { O{} m m} {
  \_@@_definiendum_args:n { #1 }
  \stex_get_symbol:n { #2 }
  \stex_ref_new_sym_target:n \l_stex_get_symbol_uri_str
  \str_if_empty:NTF \l_@@_definiendum_root_str {
    \tl_if_empty:NTF \l_@@_definiendum_post_tl {
      \tl_set:Nn \l_tmpa_tl { #3 }
    } {
      \str_set:Nx \l_@@_definiendum_root_str { #3 }
      \tl_set:Nn \l_tmpa_tl {
        \l_@@_definiendum_pre_tl\l_@@_definiendum_root_str\l_@@_definiendum_post_tl
       }
    }
  } {
    \tl_set:Nn \l_tmpa_tl { #3 }
  }

  % TODO root
  \stex_html_backend:TF {
    \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { \l_tmpa_tl }
  } {
    \exp_args:Nnx \defemph@uri { \l_tmpa_tl } { \l_stex_get_symbol_uri_str }
  }
}
\stex_deactivate_macro:Nn \definiendum {definition~environments}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{definame}
%    \begin{macrocode}

\NewDocumentCommand \definame { O{} m } {
  \_@@_definiendum_args:n { #1 }
  % TODO: root
  \stex_get_symbol:n { #2 }
  \stex_ref_new_sym_target:n \l_stex_get_symbol_uri_str
  \str_set:Nx \l_tmpa_str {
    \prop_item:cn { l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop } { name }
  }
  \str_replace_all:Nnn \l_tmpa_str {-} {~}
  \stex_html_backend:TF {
    \stex_if_do_html:T {
      \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { 
        \l_tmpa_str\l_@@_definiendum_post_tl
      }
    }
  } {
    \exp_args:Nnx \defemph@uri {
      \l_tmpa_str\l_@@_definiendum_post_tl
    } { \l_stex_get_symbol_uri_str }
  }
}
\stex_deactivate_macro:Nn \definame {definition~environments}

\NewDocumentCommand \Definame { O{} m } {
  \_@@_definiendum_args:n { #1 }
  \stex_get_symbol:n { #2 }
  \str_set:Nx \l_tmpa_str {
    \prop_item:cn { l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop } { name }
  }
  \exp_args:NNno \str_replace_all:Nnn \l_tmpa_str {-} {~}
  \stex_ref_new_sym_target:n \l_stex_get_symbol_uri_str
  \stex_html_backend:TF {
    \stex_if_do_html:T {
      \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { 
        \exp_after:wN \stex_capitalize:n \l_tmpa_str\l__stex_statements_definiendum_post_tl
      }
    }
  } {
    \exp_args:Nnx \defemph@uri {
      \exp_after:wN \stex_capitalize:n \l_tmpa_str\l__stex_statements_definiendum_post_tl
    } { \l_stex_get_symbol_uri_str }
  }
}
\stex_deactivate_macro:Nn \Definame {definition~environments}

\NewDocumentCommand \premise { m }{
  \noindent\stex_annotate:nnn{ premise }{}{\ignorespaces #1 }
}
\NewDocumentCommand \conclusion { m }{
  \noindent\stex_annotate:nnn{ conclusion }{}{\ignorespaces #1 }
}
\NewDocumentCommand \definiens { O{} m }{
  \str_clear:N \l_stex_get_symbol_uri_str
  \tl_if_empty:nF {#1} {
    \stex_get_symbol:n { #1 }
  }
  \str_if_empty:NT \l_stex_get_symbol_uri_str {
    \int_compare:nNnTF {\clist_count:N \l_@@_sdefinition_for_clist} = 1 {
      \str_set:Nx \l_stex_get_symbol_uri_str {\clist_item:Nn \l_@@_sdefinition_for_clist 1}
    }{
      % TODO throw error
    }
  }
  \str_if_eq:eeT {\prop_item:cn {l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop}{module}}
    {\l_stex_current_module_str}{
      \str_if_eq:eeF {\prop_item:cn {l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop}{defined}}
      {true}{
        \prop_put:cnn{l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop}{defined}{true}
        \exp_args:Nx \stex_add_to_current_module:n {
          \prop_put:cnn{l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop}{defined}{true}
        }
      }
  }
  \stex_annotate:nnn{ definiens }{\l_stex_get_symbol_uri_str}{ #2 }
}

\NewDocumentCommand \varbindforall {m}{
  \stex_symbol_or_var:n {#1}
  \bool_if:NTF\l_stex_symbol_or_var_bool{
    \stex_if_do_html:T {
      \stex_annotate_invisible:nnn {bindtype}{forall,\l_stex_get_symbol_uri_str}{}
    }
  }{
    % todo throw error
  }
}

\stex_deactivate_macro:Nn \premise {definition,~example~or~assertion~environments}
\stex_deactivate_macro:Nn \conclusion {example~or~assertion~environments}
\stex_deactivate_macro:Nn \definiens {definition~environments}
\stex_deactivate_macro:Nn \varbindforall {definition~or~assertion~environments}

%    \end{macrocode}
% \end{macro}
%
% \begin{environment}{sdefinition}
%    \begin{macrocode}

\keys_define:nn {stex / sdefinition }{
  type    .str_set_x:N  = \sdefinitiontype,
  id      .str_set_x:N  = \sdefinitionid,
  name    .str_set_x:N  = \sdefinitionname,
  for     .clist_set:N  = \l_@@_sdefinition_for_clist ,
  title   .tl_set:N     = \sdefinitiontitle
}
\cs_new_protected:Nn \_@@_sdefinition_args:n {
  \str_clear:N \sdefinitiontype
  \str_clear:N \sdefinitionid
  \str_clear:N \sdefinitionname
  \clist_clear:N \l_@@_sdefinition_for_clist
  \tl_clear:N \sdefinitiontitle
  \keys_set:nn { stex / sdefinition }{ #1 }
}

\NewDocumentEnvironment{sdefinition}{O{}}{
  \_@@_sdefinition_args:n{ #1 }
  \stex_reactivate_macro:N \definiendum
  \stex_reactivate_macro:N \definame
  \stex_reactivate_macro:N \Definame
  \stex_reactivate_macro:N \premise
  \stex_reactivate_macro:N \definiens
  \stex_reactivate_macro:N \varbindforall
  \stex_if_smsmode:F{
    \seq_clear:N \l_tmpb_seq
    \clist_map_inline:Nn \l_@@_sdefinition_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \exp_args:NNo \seq_put_right:Nn \l_tmpb_seq {
          \l_stex_get_symbol_uri_str
        }
      }
    }
    \clist_set_from_seq:NN \l_@@_sdefinition_for_clist \l_tmpb_seq
    \exp_args:Nnnx
    \begin{stex_annotate_env}{definition}{\seq_use:Nn \l_tmpb_seq {,}}
    \str_if_empty:NF \sdefinitiontype {
      \stex_annotate_invisible:nnn{typestrings}{\sdefinitiontype}{}
    }
    \str_if_empty:NF \sdefinitionname {
      \stex_annotate_invisible:nnn{statementname}{\sdefinitionname}{}
    }
    \clist_set:No \l_tmpa_clist \sdefinitiontype
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \l_tmpa_clist {
      \tl_if_exist:cT {_@@_sdefinition_##1_start:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sdefinition_##1_start:}}
      }
    }
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_sdefinition_start:
    }{
      \l_tmpa_tl
    }
  }
  \stex_ref_new_doc_target:n \sdefinitionid
  \stex_smsmode_do:
}{
  \stex_suppress_html:n {
    \str_if_empty:NF \sdefinitionname { \stex_symdecl_do:nn{}{\sdefinitionname} }
  }
  \stex_if_smsmode:F {
    \clist_set:No \l_tmpa_clist \sdefinitiontype
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \l_tmpa_clist {
      \tl_if_exist:cT {_@@_sdefinition_##1_end:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sdefinition_##1_end:}}
      }
    }
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_sdefinition_end:
    }{
      \l_tmpa_tl
    }
    \end{stex_annotate_env}
  }
}
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\stexpatchdefinition}
%    \begin{macrocode}
\cs_new_protected:Nn \_@@_sdefinition_start: {
  \stex_par:\noindent\titleemph{Definition\tl_if_empty:NF \sdefinitiontitle {
    ~(\sdefinitiontitle)
  }~}
}
\cs_new_protected:Nn \_@@_sdefinition_end: {\stex_par:\medskip}

\newcommand\stexpatchdefinition[3][] {
    \str_set:Nx \l_tmpa_str{ #1 }
    \str_if_empty:NTF \l_tmpa_str {
      \tl_set:Nn \_@@_sdefinition_start: { #2 }
      \tl_set:Nn \_@@_sdefinition_end: { #3 }
    }{
      \exp_after:wN \tl_set:Nn \csname _@@_sdefinition_#1_start:\endcsname{ #2 }
      \exp_after:wN \tl_set:Nn \csname _@@_sdefinition_#1_end:\endcsname{ #3 }
    }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\inlinedef}
% inline:
%    \begin{macrocode}
\keys_define:nn {stex / inlinedef }{
  type    .str_set_x:N  = \sdefinitiontype,
  id      .str_set_x:N  = \sdefinitionid,
  for     .clist_set:N  = \l_@@_sdefinition_for_clist ,
  name    .str_set_x:N  = \sdefinitionname
}
\cs_new_protected:Nn \_@@_inlinedef_args:n {
  \str_clear:N \sdefinitiontype
  \str_clear:N \sdefinitionid
  \str_clear:N \sdefinitionname
  \clist_clear:N \l_@@_sdefinition_for_clist
  \keys_set:nn { stex / inlinedef }{ #1 }
}
\NewDocumentCommand \inlinedef { O{} m } {
  \begingroup
  \_@@_inlinedef_args:n{ #1 }
  \stex_reactivate_macro:N \definiendum
  \stex_reactivate_macro:N \definame
  \stex_reactivate_macro:N \Definame
  \stex_reactivate_macro:N \premise
  \stex_reactivate_macro:N \definiens
  \stex_reactivate_macro:N \varbindforall
  \stex_ref_new_doc_target:n \sdefinitionid
  \stex_if_smsmode:TF{\stex_suppress_html:n {
    \str_if_empty:NF \sdefinitionname { \stex_symdecl_do:nn{}{\sdefinitionname} }
  }}{
    \seq_clear:N \l_tmpb_seq
    \clist_map_inline:Nn \l_@@_sdefinition_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \exp_args:NNo \seq_put_right:Nn \l_tmpb_seq {
          \l_stex_get_symbol_uri_str
        }
      }
    }
    \clist_set_from_seq:NN \l_@@_sdefinition_for_clist \l_tmpb_seq
    \ifvmode\noindent\fi
    \exp_args:Nnx
    \stex_annotate:nnn{definition}{\seq_use:Nn \l_tmpb_seq {,}}{
      \str_if_empty:NF \sdefinitiontype {
        \stex_annotate_invisible:nnn{typestrings}{\sdefinitiontype}{}
      }
      #2
      \str_if_empty:NF \sdefinitionname {
        \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sdefinitionname}}
        \stex_annotate_invisible:nnn{statementname}{\sdefinitionname}{}
      }
    }
  }
  \endgroup
  \stex_smsmode_do:
}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Assertions}
%
% \begin{environment}{sassertion}
%    \begin{macrocode}

\keys_define:nn {stex / sassertion }{
  type    .str_set_x:N  = \sassertiontype,
  id      .str_set_x:N  = \sassertionid,
  title   .tl_set:N     = \sassertiontitle ,
  for     .clist_set:N  = \l_@@_sassertion_for_clist ,
  name    .str_set_x:N  = \sassertionname
}
\cs_new_protected:Nn \_@@_sassertion_args:n {
  \str_clear:N \sassertiontype
  \str_clear:N \sassertionid
  \str_clear:N \sassertionname
  \clist_clear:N \l_@@_sassertion_for_clist
  \tl_clear:N \sassertiontitle
  \keys_set:nn { stex / sassertion }{ #1 }
}

%\tl_new:N \g_@@_aftergroup_tl

\NewDocumentEnvironment{sassertion}{O{}}{
  \_@@_sassertion_args:n{ #1 }
  \stex_reactivate_macro:N \premise
  \stex_reactivate_macro:N \conclusion
  \stex_reactivate_macro:N \varbindforall
  \stex_if_smsmode:F {
    \seq_clear:N \l_tmpb_seq
    \clist_map_inline:Nn \l_@@_sassertion_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \exp_args:NNo \seq_put_right:Nn \l_tmpb_seq {
          \l_stex_get_symbol_uri_str
        }
      }
    }
    \exp_args:Nnnx
    \begin{stex_annotate_env}{assertion}{\seq_use:Nn \l_tmpb_seq {,}}
    \str_if_empty:NF \sassertiontype {
      \stex_annotate_invisible:nnn{type}{\sassertiontype}{}
    }
    \str_if_empty:NF \sassertionname {
      \stex_annotate_invisible:nnn{statementname}{\sassertionname}{}
    }
    \clist_set:No \l_tmpa_clist \sassertiontype
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \l_tmpa_clist {
      \tl_if_exist:cT {_@@_sassertion_##1_start:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sassertion_##1_start:}}
      }
    }
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_sassertion_start:
    }{
      \l_tmpa_tl
    }
  }
  \str_if_empty:NTF \sassertionid {
    \str_if_empty:NF \sassertionname {
      \stex_ref_new_doc_target:n {}
    }
  } {
    \stex_ref_new_doc_target:n \sassertionid
  }
  \stex_smsmode_do:
}{
  \str_if_empty:NF \sassertionname { 
    \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sassertionname}}
    \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sassertionname}
  }
  \stex_if_smsmode:F {  
    \clist_set:No \l_tmpa_clist \sassertiontype
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \l_tmpa_clist {
      \tl_if_exist:cT {_@@_sassertion_##1_end:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sassertion_##1_end:}}
      }
    }
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_sassertion_end:
    }{
      \l_tmpa_tl
    }
    \end{stex_annotate_env}
  }
}
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\stexpatchassertion}
%    \begin{macrocode}

\cs_new_protected:Nn \_@@_sassertion_start: {
  \stex_par:\noindent\titleemph{Assertion~\tl_if_empty:NF \sassertiontitle {
    (\sassertiontitle)
  }~}
}
\cs_new_protected:Nn \_@@_sassertion_end: {\stex_par:\medskip}

\newcommand\stexpatchassertion[3][] {
    \str_set:Nx \l_tmpa_str{ #1 }
    \str_if_empty:NTF \l_tmpa_str {
      \tl_set:Nn \_@@_sassertion_start: { #2 }
      \tl_set:Nn \_@@_sassertion_end: { #3 }
    }{
      \exp_after:wN \tl_set:Nn \csname _@@_sassertion_#1_start:\endcsname{ #2 }
      \exp_after:wN \tl_set:Nn \csname _@@_sassertion_#1_end:\endcsname{ #3 }
    }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\inlineass}
% inline:
%    \begin{macrocode}
\keys_define:nn {stex / inlineass }{
  type    .str_set_x:N  = \sassertiontype,
  id      .str_set_x:N  = \sassertionid,
  for     .clist_set:N  = \l_@@_sassertion_for_clist ,
  name    .str_set_x:N  = \sassertionname
}
\cs_new_protected:Nn \_@@_inlineass_args:n {
  \str_clear:N \sassertiontype
  \str_clear:N \sassertionid
  \str_clear:N \sassertionname
  \clist_clear:N \l_@@_sassertion_for_clist
  \keys_set:nn { stex / inlineass }{ #1 }
}
\NewDocumentCommand \inlineass { O{} m } {
  \begingroup
  \stex_reactivate_macro:N \premise
  \stex_reactivate_macro:N \conclusion
  \stex_reactivate_macro:N \varbindforall
  \_@@_inlineass_args:n{ #1 }
  \str_if_empty:NTF \sassertionid {
    \str_if_empty:NF \sassertionname {
      \stex_ref_new_doc_target:n {}
    }
  } {
    \stex_ref_new_doc_target:n \sassertionid
  }

  \stex_if_smsmode:TF{  
    \str_if_empty:NF \sassertionname { 
      \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sassertionname}}
      \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sassertionname}
    }
  }{
    \seq_clear:N \l_tmpb_seq
    \clist_map_inline:Nn \l_@@_sassertion_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \exp_args:NNo \seq_put_right:Nn \l_tmpb_seq {
          \l_stex_get_symbol_uri_str
        }
      }
    }
    \ifvmode\noindent\fi
    \exp_args:Nnx
    \stex_annotate:nnn{assertion}{\seq_use:Nn \l_tmpb_seq {,}}{
      \str_if_empty:NF \sassertiontype {
        \stex_annotate_invisible:nnn{typestrings}{\sassertiontype}{}
      }
      #2  
      \str_if_empty:NF \sassertionname { 
        \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sassertionname}}
        \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sassertionname}
        \stex_annotate_invisible:nnn{statementname}{\sassertionname}{}
      }
    }
  }
  \endgroup
  \stex_smsmode_do:
}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Examples}
%
% \begin{environment}{sexample}
%    \begin{macrocode}

\keys_define:nn {stex / sexample }{
  type    .str_set_x:N  = \exampletype,
  id      .str_set_x:N  = \sexampleid,
  title   .tl_set:N     = \sexampletitle,
  name    .str_set_x:N  = \sexamplename ,
  for     .clist_set:N  = \l_@@_sexample_for_clist,
}
\cs_new_protected:Nn \_@@_sexample_args:n {
  \str_clear:N \sexampletype
  \str_clear:N \sexampleid
  \str_clear:N \sexamplename
  \tl_clear:N \sexampletitle
  \clist_clear:N \l_@@_sexample_for_clist
  \keys_set:nn { stex / sexample }{ #1 }
}

\NewDocumentEnvironment{sexample}{O{}}{
  \_@@_sexample_args:n{ #1 }
  \stex_reactivate_macro:N \premise
  \stex_reactivate_macro:N \conclusion
  \stex_if_smsmode:F {
    \seq_clear:N \l_tmpb_seq
    \clist_map_inline:Nn \l_@@_sexample_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \exp_args:NNo \seq_put_right:Nn \l_tmpb_seq {
          \l_stex_get_symbol_uri_str
        }
      }
    }
    \exp_args:Nnnx
    \begin{stex_annotate_env}{example}{\seq_use:Nn \l_tmpb_seq {,}}
    \str_if_empty:NF \sexampletype {
      \stex_annotate_invisible:nnn{typestrings}{\sexampletype}{}
    }
    \str_if_empty:NF \sexamplename {
      \stex_annotate_invisible:nnn{statementname}{\sexamplename}{}
    }
    \clist_set:No \l_tmpa_clist \sexampletype
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \l_tmpa_clist {
      \tl_if_exist:cT {_@@_sexample_##1_start:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sexample_##1_start:}}
      }
    }
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_sexample_start:
    }{
      \l_tmpa_tl
    }
  }
  \str_if_empty:NF \sexampleid {
    \stex_ref_new_doc_target:n \sexampleid
  }
  \stex_smsmode_do:
}{
  \str_if_empty:NF \sexamplename { 
    \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sexamplename}}
  }
  \stex_if_smsmode:F {
    \clist_set:No \l_tmpa_clist \sexampletype
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \l_tmpa_clist {
      \tl_if_exist:cT {_@@_sexample_##1_end:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sexample_##1_end:}}
      }
    }
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_sexample_end:
    }{
      \l_tmpa_tl
    }
    \end{stex_annotate_env}
  }
}
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\stexpatchexample}
%    \begin{macrocode}

\cs_new_protected:Nn \_@@_sexample_start: {
  \stex_par:\noindent\titleemph{Example~\tl_if_empty:NF \sexampletitle {
    (\sexampletitle)
  }~}
}
\cs_new_protected:Nn \_@@_sexample_end: {\stex_par:\medskip}

\newcommand\stexpatchexample[3][] {
    \str_set:Nx \l_tmpa_str{ #1 }
    \str_if_empty:NTF \l_tmpa_str {
      \tl_set:Nn \_@@_sexample_start: { #2 }
      \tl_set:Nn \_@@_sexample_end: { #3 }
    }{
      \exp_after:wN \tl_set:Nn \csname _@@_sexample_#1_start:\endcsname{ #2 }
      \exp_after:wN \tl_set:Nn \csname _@@_sexample_#1_end:\endcsname{ #3 }
    }
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\inlineex}
% inline:
%    \begin{macrocode}
\keys_define:nn {stex / inlineex }{
  type    .str_set_x:N  = \sexampletype,
  id      .str_set_x:N  = \sexampleid,
  for     .clist_set:N  = \l_@@_sexample_for_clist ,
  name    .str_set_x:N  = \sexamplename
}
\cs_new_protected:Nn \_@@_inlineex_args:n {
  \str_clear:N \sexampletype
  \str_clear:N \sexampleid
  \str_clear:N \sexamplename
  \clist_clear:N \l_@@_sexample_for_clist
  \keys_set:nn { stex / inlineex }{ #1 }
}
\NewDocumentCommand \inlineex { O{} m } {
  \begingroup
  \stex_reactivate_macro:N \premise
  \stex_reactivate_macro:N \conclusion
  \_@@_inlineex_args:n{ #1 }
  \str_if_empty:NF \sexampleid {
    \stex_ref_new_doc_target:n \sexampleid
  }
  \stex_if_smsmode:TF{
    \str_if_empty:NF \sexamplename { 
      \stex_suppress_html:n{\stex_symdecl_do:nn{}{\examplename}}
    }
  }{
    \seq_clear:N \l_tmpb_seq
    \clist_map_inline:Nn \l_@@_sexample_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \exp_args:NNo \seq_put_right:Nn \l_tmpb_seq {
          \l_stex_get_symbol_uri_str
        }
      }
    }
    \ifvmode\noindent\fi
    \exp_args:Nnx
    \stex_annotate:nnn{example}{\seq_use:Nn \l_tmpb_seq {,}}{
      \str_if_empty:NF \sexampletype {
        \stex_annotate_invisible:nnn{typestrings}{\sexampletype}{}
      }
      #2
      \str_if_empty:NF \sexamplename { 
        \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sexamplename}}
        \stex_annotate_invisible:nnn{statementname}{\sexamplename}{}
      }
    }
  }
  \endgroup
  \stex_smsmode_do:
}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Logical Paragraphs}
%
% \begin{environment}{sparagraph}
%    \begin{macrocode}
\keys_define:nn { stex / sparagraph} {
  id      .str_set_x:N   = \sparagraphid , 
  title   .tl_set:N      = \l_stex_sparagraph_title_tl , 
  type    .str_set_x:N   = \sparagraphtype ,
  for     .clist_set:N   = \l_@@_sparagraph_for_clist ,
  from    .tl_set:N      = \sparagraphfrom ,
  to      .tl_set:N      = \sparagraphto ,
  start   .tl_set:N      = \l_stex_sparagraph_start_tl ,
  name    .str_set:N     = \sparagraphname ,
  imports .tl_set:N      = \l_@@_sparagraph_imports_tl
}

\cs_new_protected:Nn \stex_sparagraph_args:n {
  \tl_clear:N \l_stex_sparagraph_title_tl
  \tl_clear:N \sparagraphfrom
  \tl_clear:N \sparagraphto
  \tl_clear:N \l_stex_sparagraph_start_tl
  \tl_clear:N \l_@@_sparagraph_imports_tl
  \str_clear:N \sparagraphid
  \str_clear:N \sparagraphtype
  \clist_clear:N \l_@@_sparagraph_for_clist
  \str_clear:N \sparagraphname
  \keys_set:nn { stex / sparagraph }{ #1 }
}
\newif\if@in@omtext\@in@omtextfalse

\NewDocumentEnvironment {sparagraph} { O{} } {
  \stex_sparagraph_args:n { #1 }
  \tl_if_empty:NTF \l_stex_sparagraph_start_tl {
    \tl_set_eq:NN \sparagraphtitle \l_stex_sparagraph_title_tl
  }{
    \tl_set_eq:NN \sparagraphtitle \l_stex_sparagraph_start_tl
  }
  \@in@omtexttrue
  \stex_if_smsmode:F {
    \seq_clear:N \l_tmpb_seq
    \clist_map_inline:Nn \l_@@_sparagraph_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \exp_args:NNo \seq_put_right:Nn \l_tmpb_seq {
          \l_stex_get_symbol_uri_str
        }
      }
    }
    \exp_args:Nnnx
    \begin{stex_annotate_env}{paragraph}{\seq_use:Nn \l_tmpb_seq {,}}
    \str_if_empty:NF \sparagraphtype {
      \stex_annotate_invisible:nnn{typestrings}{\sparagraphtype}{}
    }
    \str_if_empty:NF \sparagraphfrom {
      \stex_annotate_invisible:nnn{from}{\sparagraphfrom}{}
    }
    \str_if_empty:NF \sparagraphto {
      \stex_annotate_invisible:nnn{to}{\sparagraphto}{}
    }
    \str_if_empty:NF \sparagraphname {
      \stex_annotate_invisible:nnn{statementname}{\sparagraphname}{}
    }
    \clist_set:No \l_tmpa_clist \sparagraphtype
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \sparagraphtype {
      \tl_if_exist:cT {_@@_sparagraph_##1_start:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sparagraph_##1_start:}}
      }
    }
    \stex_csl_to_imports:No \usemodule \l_@@_sparagraph_imports_tl
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_sparagraph_start:
    }{
      \l_tmpa_tl
    }
  }
  \clist_set:No \l_tmpa_clist \sparagraphtype
  \exp_args:NNx \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}}
  {
    \stex_reactivate_macro:N \definiendum
    \stex_reactivate_macro:N \definame
    \stex_reactivate_macro:N \Definame
    \stex_reactivate_macro:N \premise
    \stex_reactivate_macro:N \definiens
  }
  \str_if_empty:NTF \sparagraphid {
    \str_if_empty:NTF \sparagraphname {
      \exp_args:NNx \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}}{
        \stex_ref_new_doc_target:n {}
      }
    } {
      \stex_ref_new_doc_target:n {}
    }
  } {
    \stex_ref_new_doc_target:n \sparagraphid
  }
  \exp_args:NNx
  \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}}{
    \clist_map_inline:Nn \l_@@_sparagraph_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \stex_ref_new_sym_target:n \l_stex_get_symbol_uri_str
      }
    }
  }
  \stex_smsmode_do:
  \ignorespacesandpars
}{  
  \str_if_empty:NF \sparagraphname { 
    \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sparagraphname}}
    \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sparagraphname}
  }
  \stex_if_smsmode:F {
    \clist_set:No \l_tmpa_clist \sparagraphtype
    \tl_clear:N \l_tmpa_tl
    \clist_map_inline:Nn \l_tmpa_clist {
      \tl_if_exist:cT {_@@_sparagraph_##1_end:}{
        \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sparagraph_##1_end:}}
      }
    }
    \tl_if_empty:NTF \l_tmpa_tl {
      \_@@_sparagraph_end:
    }{
      \l_tmpa_tl
    }
    \end{stex_annotate_env}
  }
}
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\stexpatchparagraph}
%    \begin{macrocode}

\cs_new_protected:Nn \_@@_sparagraph_start: {  
  \stex_par:\noindent\tl_if_empty:NTF \l_stex_sparagraph_start_tl {
    \tl_if_empty:NF \l_stex_sparagraph_title_tl {
      \titleemph{\l_stex_sparagraph_title_tl}:~
    }
  }{
    \titleemph{\l_stex_sparagraph_start_tl}~
  }
}
\cs_new_protected:Nn \_@@_sparagraph_end: {\stex_par:\medskip}

\newcommand\stexpatchparagraph[3][] {
    \str_set:Nx \l_tmpa_str{ #1 }
    \str_if_empty:NTF \l_tmpa_str {
      \tl_set:Nn \_@@_sparagraph_start: { #2 }
      \tl_set:Nn \_@@_sparagraph_end: { #3 }
    }{
      \exp_after:wN \tl_set:Nn \csname _@@_sparagraph_#1_start:\endcsname{ #2 }
      \exp_after:wN \tl_set:Nn \csname _@@_sparagraph_#1_end:\endcsname{ #3 }
    }
}

\keys_define:nn { stex / inlinepara} {
  id      .str_set_x:N   = \sparagraphid , 
  type    .str_set_x:N   = \sparagraphtype ,
  for     .clist_set:N   = \l_@@_sparagraph_for_clist ,
  from    .tl_set:N      = \sparagraphfrom ,
  to      .tl_set:N      = \sparagraphto ,
  name    .str_set:N     = \sparagraphname
}
\cs_new_protected:Nn \_@@_inlinepara_args:n {
  \tl_clear:N \sparagraphfrom
  \tl_clear:N \sparagraphto
  \str_clear:N \sparagraphid
  \str_clear:N \sparagraphtype
  \clist_clear:N \l_@@_sparagraph_for_clist
  \str_clear:N \sparagraphname
  \keys_set:nn { stex / inlinepara }{ #1 }
}
\NewDocumentCommand \inlinepara { O{} m } {
  \begingroup
  \_@@_inlinepara_args:n{ #1 }  
  \clist_set:No \l_tmpa_clist \sparagraphtype
  \str_if_empty:NTF \sparagraphid {
    \str_if_empty:NTF \sparagraphname {
      \exp_args:NNx \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}}{
        \stex_ref_new_doc_target:n {}
      }
    } {
      \stex_ref_new_doc_target:n {}
    }
  } {
    \stex_ref_new_doc_target:n \sparagraphid
  }
  \stex_if_smsmode:TF{
    \str_if_empty:NF \sparagraphname {
      \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sparagraphname}}
      \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sparagraphname}
    }
  }{
    \seq_clear:N \l_tmpb_seq
    \clist_map_inline:Nn \l_@@_sparagraph_for_clist {
      \tl_if_empty:nF{ ##1 }{
        \stex_get_symbol:n { ##1 }
        \exp_args:NNo \seq_put_right:Nn \l_tmpb_seq {
          \l_stex_get_symbol_uri_str
        }
      }
    }
    \ifvmode\noindent\fi
    \exp_args:Nnx
    \stex_annotate:nnn{paragraph}{\seq_use:Nn \l_tmpb_seq {,}}{
      \str_if_empty:NF \sparagraphtype {
        \stex_annotate_invisible:nnn{typestrings}{\sparagraphtype}{}
      }
      \str_if_empty:NF \sparagraphfrom {
        \stex_annotate_invisible:nnn{from}{\sparagraphfrom}{}
      }
      \str_if_empty:NF \sparagraphto {
        \stex_annotate_invisible:nnn{to}{\sparagraphto}{}
      }
      \str_if_empty:NF \sparagraphname { 
        \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sparagraphname}}
        \stex_annotate_invisible:nnn{statementname}{\sparagraphname}{}
        \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sparagraphname}
      }
      \exp_args:NNx \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}}{
        \clist_map_inline:Nn \l_tmpb_seq {
          \stex_ref_new_sym_target:n {##1}
        }
      }
      #2
    }
  }
  \endgroup
  \stex_smsmode_do:
}

%    \end{macrocode}
% \end{macro}
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%    \begin{macrocode}
%</package>
%    \end{macrocode}
%
% \end{implementation}
% \ifinfulldoc\else\printbibliography\fi
%
% \PrintIndex

% \endinput
% Local Variables:
% mode: doctex
% TeX-master: t
% End: