summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/modules/modules.dtx
blob: b65107d2aa678a28ef994e1da45f8324d3aa23b8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
% \iffalse meta-comment
% An Infrastructure for Semantic Macros and Module Scoping
% Copyright (C) 2004-2013 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/KWARC/sTeX/
% \fi
%  
% \iffalse
%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
%<package>\ProvidesPackage{modules}[2016/04/07 v1.4 Semantic Markup]
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{stex-logo,modules}
\usepackage{url,array,float,textcomp}
\usepackage[show]{ed}
\usepackage[hyperref=auto,style=alphabetic]{biblatex}
\addbibresource{kwarcpubs.bib}
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
\addbibresource{extcrossrefs.bib}
\usepackage{listings}
\usepackage{amsfonts}
\usepackage{ctangit}
\usepackage{xspace}
\usepackage{hyperref}
\makeindex
\floatstyle{boxed}
\newfloat{exfig}{thp}{lop}
\floatname{exfig}{Example}
\def\tracissue#1{\cite{sTeX:online}, \hyperlink{http://trac.kwarc.info/sTeX/ticket/#1}{issue #1}}
\begin{document}\DocInput{modules.dtx}\end{document} 
%</driver>
% \fi
% 
% \CheckSum{802}
%
% \changes{v0.9}{2005/06/14}{First Version with Documentation}
% \changes{v0.9a}{2005/07/01}{Completed Documentation}
% \changes{v0.9b}{2005/08/06}{Complete functionality and Updated Documentation}
% \changes{v0.9c}{2006/01/13}{more packaging}
% \changes{v0.9d}{2007/12/12}{fixing double loading of .tex and .sms}
% \changes{v0.9e}{2008/06/17}{fixing LaTeXML}
% \changes{v0.9f}{2008/06/17}{remove unused options uses and usesqualified}
% \changes{v0.9g}{2009/05/02}{adding resymdef functionality}
% \changes{v0.9g}{2009/08/12}{adding importOMDocmodule}
% \changes{v0.9h}{2010/01/19}{using {\texttt{\textbackslash mod@newcommand}} instead of
% {\texttt{\textbackslash providecommand}} for more intuitive inheritance.}
% \changes{v0.9h}{2010/03/05}{adding {\texttt{\textbackslash metalanguage}}}
% \changes{v1.0}{2010/06/18}{minor fixes}
% \changes{v1.1}{2010/12/30}{adding optional arguments to semantic macros for display
%   variants. The resymdef functionality introduced in 0.9g is now deprecated. It was hardly
%   used.}
% \changes{v1.1}{2012/06/25}{adding additional keys for the \texttt{\textbackslash symdef}
%   macro and exporting them to OMDoc}
% \changes{v1.1}{2012/07/06}{exporting requiremodules to the \texttt{aux} file, so that
%   they are preloaded (pre-required) so semantic macros in section titles can work.}
% \changes{v1.1}{2012/11/09}{Moving LaTeXML bindings into \texttt{modules.sty.ltxml} and
% disabling generation}
% \changes{v1.2}{2013/08/25}{No longer loading the aux file at the end of the document}
% \changes{v1.3}{2013/12/12}{adding MathHub support}
% \changes{v1.4}{2015/03/31}{Completely revamped importing modules this is much faster now,
% but can no longer do relative paths.}
% \changes{v1.4}{2015/04/02}{deprecated \texttt {\textbackslash sinput} and \texttt {\textbackslash sinputref}}
% \changes{v1.5}{2015/11/02}{Moved MH Versions to a separate \texttt{mathhub} package}
% 
% \GetFileInfo{modules.sty}
% 
% \MakeShortVerb{\|}
%\def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}\xspace}
% \def\xml{\scsys{Xml}}
% \def\mathml{\scsys{MathML}}
% \def\omdoc{\scsys{OMDoc}}
% \def\openmath{\scsys{OpenMath}}
% \def\latexml{\scsys{LaTeXML}}
% \def\perl{\scsys{Perl}}
% \def\cmathml{Content-{\sc MathML}\index{Content {\sc MathML}}\index{MathML@{\sc MathML}!content}}
% \def\activemath{\scsys{ActiveMath}}
% \def\twin#1#2{\index{#1!#2}\index{#2!#1}}
% \def\twintoo#1#2{{#1 #2}\twin{#1}{#2}}
% \def\atwin#1#2#3{\index{#1!#2!#3}\index{#3!#2 (#1)}}
% \def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}}
% \def\cT{\mathcal{T}}\def\cD{\mathcal{D}}
% \title{{\texttt{modules.sty}}: Semantic Macros and Module Scoping   in {\stex}\thanks{Version {\fileversion} (last revised
%        {\filedate})}}
%    \author{Michael Kohlhase \& Deyan Ginev \& Rares Ambrus\\
%            Jacobs University, Bremen\\
%            \url{http://kwarc.info/kohlhase}}
% \maketitle
%
% \begin{abstract}
%   The |modules| package is a central part of the {\stex} collection, a version of
%   {\TeX/\LaTeX} that allows to markup {\TeX/\LaTeX} documents semantically without
%   leaving the document format, essentially turning {\TeX/\LaTeX} into a document format
%   for mathematical knowledge management (MKM).
%
%   This package supplies a definition mechanism for semantic macros and a non-standard
%   scoping construct for them, which is oriented at the semantic dependency relation
%   rather than the document structure. This structure can be used by MKM systems for
%   added-value services, either directly from the {\sTeX} sources, or after translation.
% \end{abstract}
%
% \newpage\setcounter{tocdepth}{2}\tableofcontents\newpage
%
% \section{Introduction}\label{sec:intro}
% 
% Following general practice in the {\TeX/\LaTeX} community, we use the term ``semantic
% macro'' for a macro whose expansion stands for a mathematical object, and whose name
% (the command sequence) is inspired by the name of the mathematical object.  This can
% range from simple definitions like |\def\Reals{\mathbb{R}}| for individual mathematical
% objects to more complex (functional) ones object constructors like
% |\def\SmoothFunctionsOn#1{\mathcal{C}^\infty(#1,#1)}|. Semantic macros are traditionally
% used to make {\TeX/\LaTeX} code more portable. However, the {\TeX/\LaTeX} scoping model
% (macro definitions are scoped either in the local group or until the rest of the
% document), does not mirror mathematical practice, where notations are scoped by
% mathematical environments like statements, theories, or such. For an in-depth discussion
% of semantic macros and scoping we refer the reader~\cite{Kohlhase:ulsmf08}.
% 
% The |modules| package provides a {\LaTeX}-based markup infrastructure for defining
% module-scoped semantic macros and {\latexml} bindings~\cite{Miller:latexml:online} to
% create {\omdoc}~\cite{Kohlhase:OMDoc1.2} from {\stex} documents. In the {\stex} world
% semantic macros have a special status, since they allow the transformation of
% {\TeX/\LaTeX} formulae into a content-oriented markup format like
% {\openmath}~\cite{BusCapCar:2oms04} and (strict) content
% {\mathml}~\cite{CarlisleEd:MathML3}; see Figure~\ref{fig:omsemmac} for an example, where
% the semantic macros above have been defined by the |\symdef| macros (see
% Section~\ref{sec:symdef}) in the scope of a |\begin{module}[id=calculus]| (see
% Section~\ref{sec:modules}).
% 
% \begin{exfig}\lstset{basicstyle=\scriptsize,aboveskip=-.5em,belowskip=-1.5em}
% \begin{tabular}{l|p{9.7cm}}
% \LaTeX  & \verb|\SmoothFunctionsOn\Reals| \\\hline
% PDF/DVI & ${\mathcal{C}^\infty(\mathbb{R},\mathbb{R})}$\\\hline
%  {\openmath} & \lstset{morekeywords={OMA,OMS}}
% \begin{lstlisting}
% <OMA>
%   <OMS cd="calculus" name="SmoothFunctionsOn"/>
%   <OMS cd="calculus" name="Reals"/>
% </OMA>\end{lstlisting}\\\hline
% {\mathml}  & \lstset{morekeywords={apply,csymbol}}
% \begin{lstlisting}
% <apply>
%   <csymbol cd="calculus">SmoothFunctionsOn</csymbol>
%   <csymbol cd="calculus">Reals</csymbol>
% </apply>\end{lstlisting}\\
% \end{tabular}
% \caption{{\openmath} and {\mathml} generated from Semantic Macros}\label{fig:omsemmac}
% \end{exfig}
% 
% \section{The User Interface}
%
% The main contributions of the |modules| package are the |module| environment, which
% allows for lexical scoping of semantic macros with inheritance and the |\symdef| macro
% for declaration of semantic macros that underly the |module| scoping.
% 
% \subsection{Package Options}\label{sec:options}
%
% The |modules| package takes two options: If we set
% \DescribeMacro{showmods}|showmods|\ednote{This mechanism does not work yet, since we
% cannot disable it when importing modules and that leads to unwanted boxes. What we need
% to do instead is to tweak the sms utility to use an internal version that never shows
% anything during sms reading.}, then the views (see Section~\ref{sec:user:views}) are
% shown. If we set the \DescribeMacro{qualifiedimports}|qualifiedimports| option, then
% qualified imports are enabled. Qualified imports give more flexibility in module
% inheritance, but consume more internal memory. As qualified imports are not fully
% implemented at the moment, they are turned off by default see
% Limitation~\ref{sec:limitations:qualified-imports}. The option
% \DescribeMacro{noauxreq}|noauxreq| prohibits the registration of |\@requiremodules|
% commands in the |aux| file. They are necessary for preloading the module signatures so
% that entries in the table of contents can have semantic macros; but as they sometimes
% cause trouble the option allows to turn off preloading.
% 
% If the \DescribeMacro{showmeta}|showmeta| is set, then the metadata keys are shown
% (see~\cite{Kohlhase:metakeys:ctan} for details and customization options).
% 
% \subsection{Semantic Macros}\label{sec:symdef}
%
% The \DescribeMacro{\symdef} is the main constructor for semantic macros in {\sTeX}. A
% call to the |\symdef| macro has the general form
% \begin{quote}
% |\symdef[|\meta{keys}|]{|\meta{cseq}|}[|\meta{args}|]{|\meta{definiens}|}|
% \end{quote}
% where {\meta{cseq}} is a control sequence (the name of the semantic macro) {\meta{args}}
% is a number between 0 and 9 for the number of arguments {\meta{definiens}} is the token
% sequence used in macro expansion for {\meta{cseq}}. Finally {\meta{keys}} is a keyword
% list that further specifies the semantic status of the defined macro.
% 
% The two semantic macros in Figure~\ref{fig:omsemmac} would have been declared by
% invocations of the |\symdef| macro of the form:
% \begin{verbatim}
% \symdef{Reals}{\mathbb{R}}
% \symdef{SmoothFunctionsOn}[1]{\mathcal{C}^\infty(#1,#1)}
% \end{verbatim}
% 
% Note that both semantic macros correspond to {\openmath} or {\mathml} ``symbols'',
% i.e. named representations of mathematical concepts (the real numbers and the
% constructor for the space of smooth functions over a set); we call these names the
% \textbf{symbol name} of a semantic macro. Normally, the symbol name of a semantic macro
% declared by a |\symdef| directive is just \meta{cseq}. The key-value pair
% \DescribeMacro{name}|name=|\meta{symname} can be used to override this behavior and
% specify a differing name. There are two main use cases for this.
% 
% The first one is shown in Example~\ref{fig:symvariant}, where we define semantic macros
% for the ``exclusive or'' operator. Note that we define two semantic macros: |\xorOp| and
% |\xor| for the applied form and the operator. As both relate to the same mathematical
% concept, their symbol names should be the same, so we specify |name=xor| on the
% definition of |\xorOp|.
% 
% A key \DescribeMacro{local}|local| can be added to {\meta{keys}} to specify that the
% symbol is local to the module and is invisible outside. Note that even though |\symdef|
% has no advantage over |\def| for defining local semantic macros, it is still considered
% good style to use |\symdef| and |\abbrdef|, if only to make switching between local and
% exported semantic macros easier.
% 
% Finally, the key \DescribeMacro{primary}|primary| (no value) can be given for primary
% symbols.
% 
% \DescribeMacro{\abbrdef}The |\abbrdef| macro is a variant of |\symdef| that is only
% different in semantics, not in presentation. An abbreviative macro is like a semantic
% macro, and underlies the same scoping and inheritance rules, but it is just an
% abbreviation that is meant to be expanded, it does not stand for an atomic mathematical
% object.
%
% We will use a simple module for natural number arithmetics as a running example. It
% defines exponentiation and summation as new concepts while drawing on the basic
% operations like $+$ and $-$ from {\LaTeX}. In our example, we will define a semantic
% macro for summation |\Sumfromto|, which will allow us to express an expression like
% $\sum{i=1}^nx^i$ as |\Sumfromto{i}1n{2i-1}| (see Example~\ref{fig:semmodule} for an
% example). In this example we have also made use of a local semantic symbol for $n$,
% which is treated as an arbitrary (but fixed) symbol.
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=arith]
%   \symdef{Sumfromto}[4]{\sum_{#1=#2}^{#3}{#4}}
%   \symdef[local]{arbitraryn}{n}
%   What is the sum of the first $\arbitraryn$ odd numbers, i.e.
%   $\Sumfromto{i}1\arbitraryn{2i-1}?$
% \end{module}
% \end{verbatim}
% \vspace*{-3.5ex}\hrule\vspace*{1ex}
% \begin{module}[id=arith]
% \symdef{Sumfromto}[4]{\sum_{#1=#2}^{#3}{#4}}
% \symdef[local]{arbitraryn}{n}
% What is the sum of the first $\arbitraryn$ odd numbers, i.e.
% $\Sumfromto{i}1\arbitraryn{2i-1}?$
% \end{module}
% \caption{Semantic Markup in a {\texttt{module}} Context}\label{fig:semmodule}
% \end{exfig}
%
% The \DescribeMacro{\symvariant}|\symvariant| macro can be used to define presentation
% variants for semantic macros previously defined via the |\symdef| directive. In an
% invocation 
% \begin{quote}
% |\symdef[|\meta{keys}|]{|\meta{cseq}|}[|\meta{args}|]{|\meta{pres}|}|\\
% |\symvariant{|\meta{cseq}|}[|\meta{args}|]{|\meta{var}|}{|\meta{varpres}|}|
% \end{quote}
% the first line defines the semantic macro |\|\meta{cseq} that when applied to
% \meta{args} arguments is presented as \meta{pres}. The second line allows the semantic
% macro to be called with an optional argument \meta{var}: |\|\meta{cseq}|[var]| (applied
% to \meta{args} arguments) is then presented as \meta{varpres}. We can define a variant
% presentation for |\xor|; see Figure~\ref{fig:symvariant} for an example.
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=xbool]
%   \symdef[name=xor]{xorOp}{\oplus}
%   \symvariant{xorOp}{uvee}{\underline{\vee}}
%   \symdef{xor}[2]{#1\xorOp #2}
%   \symvariant{xor}[2]{uvee}{#1\xorOp[uvee] #2}
%   Exclusive disjunction is commutative: $\xor{p}q=\xor{q}p$\\
%   Some authors also write exclusive or with the $\xorOp[uvee]$ operator, 
%   then the formula above is $\xor[uvee]{p}q=\xor[uvee]{q}p$
% \end{module}
% \end{verbatim}
% \vspace*{-3.5ex}\hrule\vspace*{1ex}
% \begin{module}[id=xbool]
%   \symdef[name=xor]{xorOp}{\oplus}
%   \symvariant{xorOp}{uvee}{\underline{\vee}}
%   \symdef{xor}[2]{#1\xorOp #2}
%   \symvariant{xor}[2]{uvee}{#1\xorOp[uvee] #2}
%   Exclusive disjunction is commutative: $\xor{p}q=\xor{q}p$\\
%   Some authors also write exclusive or with the $\xorOp[uvee]$ operator, 
%   then the formula above is $\xor[uvee]{p}q=\xor[uvee]{q}p$
% \end{module}
% \caption{Presentation Variants of a Semantic Macro}\label{fig:symvariant}
% \end{exfig}
%
% Version 1.0 of the |modules| package had the \DescribeMacro{\resymdef}|\resymdef| macro
% that allowed to locally redefine the presentation of a macro. But this did not interact
% well with the |beamer| package and was less useful than the |\symvariant|
% functionality. Therefore it is deprecated now and leads to an according error message.
% \subsection{Testing Semantic Macros}\label{sec:user:testing}
% 
% One of the problems in managing large module graphs with many semantic macros, so the
% |module| package gives an infrastructure for unit testing.  The first macro is
% \DescribeMacro{\symtest}|\symtest|, which allows the author of a semantic macro to
% generate test output (if the |symtest| option is set) see figure~\ref{fig:symtest} for a
% ``tested semantic macro definition''.
% \begin{exfig}
% \begin{verbatim}
% \symdef[name=setst]{SetSt}[2]{\{#1\,\vert\,#2\}}
% \symtest[name=setst]{SetSt}{\SetSt{a}{a>0}}
% \end{verbatim}
% \vspace*{-2em} generates the output 
% \begin{module}[id=foo]
% \symdef[name=setst]{SetSt}[2]{\{#1\,\vert\,#2\}}
% \symtest[name=setst]{SetSt}{\SetSt{a}{a>0}}
% \end{module}
% \caption{A Semantic Macro Definition with Test}\label{fig:symtest}
% \end{exfig}
% Note that the language in this purely generated, so that it can be adapted (tbd).
% 
% The \DescribeMacro{\abbrtest}|\abbrtest| macro gives the analogous functionality for
% |\abbrdef|. 
%
% \subsection{Axiomatic Assumptions}\label{sec:user:assumptions}
% 
% In many ways, axioms and assumptions in definitions behave a lot like symbols
% (see~\cite{RabKoh:WSMSML10} for discussion). Therefore we provide the macro
% \DescribeMacro{\assdef}|\assdef| that can be used to mark up assumptions. Given a phrase
% \meta{phrase} in a definition\ednote{only definitions?}, we can use
% |\assdef{|\meta{name}|}{|\meta{phrase}|}| to give this the symbol name
% \meta{name}.\ednote{continue}
%
% \subsection{Semantic Macros for Variables}\label{sec:user:semvars}
%
% Up to now, the semantic macros generated \openmath and \mathml markup where the heads of
% the semantic macros become constants (the |OMS| and |csymbol| elements in
% Figure~\ref{fig:omsemmac}). But sometimes we want to have semantic macros for variables,
% e.g. to associate special notation conventions. For instance, if we want to define
% mathematical structures from components as in Figure~\ref{fig:monoid}, where the
% semigroup operation $\circ$ is a variable epistemologically, but is a $n$-ary
% associative operator -- we are in a semigroup after all. Let us call such variables
% \textbf{semantic variables} to contrast them from \textbf{semantic constants} generated
% by |\symdef| and |\symvariant|.
%
%\begin{exfig}
%  \textbf{Definition 3.17} Let $\langle G,\circ\rangle$ be a semigroup, then we call
%  $e\in G$ a \textbf{unit}, iff $e\circ x=x\circ e=x$. A semigroup with unit $\langle
%  G,\circ,e\rangle$ is called a \textbf{monoid}.
%  \caption{A Definition of a Structure with ``semantic
%  variables''.}\label{fig:monoid}
% \end{exfig}
%
% Semantic variables differ from semantic constants in two ways:
% \begin{inparaenum}[\em i\rm)]
% \item they do not participate
% in the imports mechanism and
% \item they generate markup with variables.
% \end{inparaenum}
%  In the case of
% Figure~\ref{fig:monoid} we (want to) have the \xml markup in Figure~\ref{fig:omsemvar}.
% To associate the notation to the variables, we define semantic macros for them, here the
% macro |\op| for the (semigroup) operation via the \DescribeMacro{\vardef}|\vardef|
% macro. |\vardef| works exactly like, except
% \begin{inparaenum}[\em i\rm)]
% \item semantic variables are local to the current {\TeX} group and 
% \item they generate variable markup in the \xml
% \end{inparaenum}
% 
% \begin{exfig}\lstset{basicstyle=\scriptsize,aboveskip=-.5em,belowskip=-1.5em}
% \begin{tabular}{l|p{9.7cm}}
% \sTeX   & \verb|\vardef{op}[1]{\assoc\circ{#1}}|\\\hline
% \omdoc & 
% \begin{lstlisting}
% <notation>
%   <prototype>
%     <OMA>
%       <OMV name="op"/>
%       <expr name="a1"/>
%       <expr name="a2"/>
%      </OMA>
%   </prototype>
%   <rendering>
%     <mrow>
%       <render name="a1"/>
%       <mo>&#x2384;</mo>
%       <render name="a2"/>
%     </mrow>
%   </rendering>
% </notation>\end{lstlisting}\\\hline
% \LaTeX  & \verb|\op{x,e}| \\\hline
% PDF/DVI & $x\circ e$\\\hline
%  {\openmath} & \lstset{morekeywords={OMA,OMV}}
% \begin{lstlisting}
% <OMA><OMV name="op"/><OMV name="x"/><OMV name="e"/></OMA>\end{lstlisting}\\\hline
% {\mathml}  & \lstset{morekeywords={apply,ci}}
% \begin{lstlisting}
% <apply><ci>op</ci><ci>x</ci><ci>e</ci></apply>\end{lstlisting}\\
% \end{tabular}
% \caption{Semantic Variables in {\openmath} and {\mathml}}\label{fig:omsemvar}
% \end{exfig}
% 
% \subsection{Symbol and Concept Names}\label{sec:user:termdef}
% 
% Just as the |\symdef| declarations define semantic macros for mathematical symbols, the
% |modules| package provides an infrastructure for {\emph{mathematical concepts}} that are
% expressed in mathematical vernacular. The key observation here is that concept names
% like ``finite symplectic group'' follow the same scoping rules as mathematical symbols,
% i.e. they are module-scoped. The \DescribeMacro{\termdef}|\termdef| macro is an analogue
% to |\symdef| that supports this: use
% |\termdef[|\meta{keys}|]{|\meta{cseq}|}{|\meta{concept}|}| to declare the macro
% |\|\meta{cseq} that expands to \meta{concept}. See Figure~\ref{fig:termref} for an
% example, where we use the \DescribeMacro{\capitalize}|\capitalize| macro to adapt
% \meta{concept} to the sentence beginning.\ednote{continue, describe \meta{keys}, they
% will have to to with plurals,\ldots once implemented}. The main use of the
% |\termdef|-defined concepts lies in automatic cross-referencing facilities via the
% \DescribeMacro{\termref}|\termref| and \DescribeMacro{\symref}|\symref| macros provided
% by the |statements| package~\ctancite{Kohlhase:smms}. Together with the |hyperref|
% package~\cite{RahObe:hmlmh10}, this provide cross-referencing to the definitions of the
% symbols and concepts. As discussed in section~\ref{sec:limitations:crossref}, the
% |\symdef| and |\termdef| declarations must be on top-level in a module, so the
% infrastructure provided in the |modules| package alone cannot be used to locate the
% definitions, so we use the infrastructure for mathematical statements for that.
%
%\begin{exfig}
% \begin{verbatim}
%   \termdef[name=xor]{xdisjunction}{exclusive disjunction}
%   \capitalize\xdisjunction is commutative: $\xor{p}q=\xor{q}p$
% \end{verbatim}
% \vspace*{-3.5ex}
% \caption{Extending Example~\ref{fig:symvariant} with Term References}\label{fig:termref}
% \end{exfig}
%
% \subsection{Modules and Inheritance}\label{sec:modules}
%
% The\DescribeEnv{module}|module| environment takes an optional |KeyVal|
% argument. Currently, only the |id| key is supported for specifying the identifier of a
% module (also called the {\twintoo{module}{name}}).  A module introduced by
% |\begin{module}[id=foo]| restricts the scope the semantic macros defined by the
%   |\symdef| form to the end of this module given by the corresponding |\end{module}|,
% and to any other |module| environments that import them by a |\importmodule{foo}|
% directive. If the module |foo| contains |\importmodule| directives of its own, these are
% also exported to the importing module.
%
% Thus the \DescribeMacro{\importmodule}|\importmodule| declarations induce the
% {\atwintoo{semantic}{inheritance}{relation}}. Figure~\ref{exf:importmodule} shows a
% module that imports the semantic macros from three others. In the simplest form,
% |\importmodule{|\meta{mod}|}| will activate the semantic macros and concepts declared by
% |\symdef| and |\termdef| in module \meta{mod} in the current module\footnote{Actually,
% in the current {\TeX} group, therefore \texttt{\textbackslash importmodule} should be
% placed directly after the \texttt{\textbackslash begin\{module\}}.}. To understand the
% mechanics of this, we need to understand a bit of the internals. The |module|
% environment sets up an internal macro pool, to which all the macros defined by the
% |\symdef| and |\termdef| declarations are added; |\importmodule| only activates this
% macro pool. Therefore |\importmodule{|\meta{mod}|}| can only work, if the {\TeX} parser
% --- which linearly goes through the {\sTeX} sources --- already came across the module
% \meta{mod}. In many situations, this is not obtainable; e.g. for ``semantic forward
% references'', where symbols or concepts are previewed or motivated to knowledgeable
% readers before they are formally introduced or for modularizations of documents into
% multiple files. To enable situations like these, the |module| package uses auxiliary
% files called {\textbf{\sTeX module signatures}}. For any file, \meta{file}|.tex|, we
% generate a corresponding \sTeX module signature \meta{file}|.sms| with the |sms| utility
% (see also Limitation~\ref{sec:limitations:sms}), which contains (copies of) all
% |\begin|/|\end{module}|, |\importmodule|, |\symdef|, and |\termdef| invocations in
% \meta{file}|.tex|. The value of an \sTeX module signature is that it can be loaded
% instead its corresponding \sTeX document, if we are only interested in the semantic
% macros. So |\importmodule[|load=\meta{filepath}|]{|\meta{mod}|}| will load the \sTeX
% module signature \meta{filepath}|.sms| (if it exists and has not been loaded before) and
% activate the semantic macros from module \meta{mod} (which was supposedly defined in
% \meta{filepath}|.tex|). Note that since \meta{filepath}|.sms| contains all
% |\importmodule| statements that \meta{filepath}|.tex| does, an |\importmodule|
% recursively loads all necessary files to supply the semantic macros inherited by the
% current module.\ednote{MK: document the other keys of |module|}
% 
% The \DescribeMacro{\metalanguage}|\metalanguage| macro is a variant of
% \lstinline|importmodule| that imports the meta language, i.e. the language in which the
% meaning of the new symbols is expressed. For mathematics this is often first-order logic
% with some set theory; see~\cite{RabKoh:WSMSML10} for discussion. 
% 
% \subsection{Dealing with multiple Files}\label{sec:user:multiple}
%
% The infrastructure presented above works well if we are dealing with small files or
% small collections of modules. In reality, collections of modules tend to grow, get
% re-used, etc, making it much more difficult to keep everything in one file. This general
% trend towards increasing entropy is aggravated by the fact that modules are very
% self-contained objects that are ideal for re-used. Therefore in the absence of a
% content management system for {\LaTeX} document (fragments), module collections tend to
% develop towards the ``one module one file'' rule, which leads to situations with lots
% and lots of little files.
%
% Moreover, most mathematical documents are not self-contained, i.e. they do not build up
% the theory from scratch, but pre-suppose the knowledge (and notation) from other
% documents. In this case we want to make use of the semantic macros from these
% prerequisite documents without including their text into the current document. One way
% to do this would be to have {\LaTeX} read the prerequisite documents without producing
% output. For efficiency reasons, {\stex} chooses a different route. It comes with a
% utility |sms| (see Section~\ref{sec:limitations:sms}) that exports the modules and macros
% defined inside them from a particular document and stores them inside |.sms| files. This
% way we can avoid overloading LaTeX with useless information, while retaining the
% important information which can then be imported in a more efficient way.
%
% \DescribeMacro{\importmodule} For such situations, the |\importmodule| macro can be
% given an optional first argument that is a path to a file that contains a path to the
% module file, whose module definition (the |.sms| file) is read. Note that the
% |\importmodule| macro can be used to make module files truly self-contained. To arrive
% at a file-based content management system, it is good practice to reuse the module
% identifiers as module names and to prefix module files with corresponding
% |\importmodule| statements that pre-load the corresponding module files.
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=foo]
% \importmodule[load=../other/bar]{bar}
% \importmodule[load=../mycolleaguesmodules]{baz}
% \importmodule[load=../other/bar]{foobar}
%   ...
% \end{module}
% \end{verbatim}
% \vspace{-1.7em}
% \caption{Self-contained Modules via {\texttt{importmodule}}}\label{exf:importmodule}
% \end{exfig}
%
% In Example~\ref{exf:importmodule}, we have shown the typical setup of a module
% file. The |\importmodule| macro takes great care that files are only read once, as
% {\sTeX} allows multiple inheritance and this setup would lead to an exponential (in the
% module inheritance depth) number of file loads.
%
% Sometimes we want to import an existing {\omdoc} theory\footnote{{\omdoc} theories are
%   the counterpart of {\stex} modules.} $\widehat\cT$ into (the {\omdoc} document
% $\widehat\cD$ generated from) a {\stex} document $\cD$. Naturally, we have to provide an
% {\stex} stub module $\cT$ that provides |\symdef| declarations for all symbols we use in
% $\cD$. In this situation, we use\DescribeMacro{\importOMDocmodule}
% |\importOMDocmodule[|\meta{spath}|]{|\meta{OURI}|}{|\meta{name}|}|, where \meta{spath}
% is the file system path to $\cT$ (as in |\importmodule|, this argument must not contain
% the file extension), \meta{OURI} is the URI to the {\omdoc} module (this time with
% extension), and \meta{name} is the name of the theory $\widehat\cT$ and the module in
% $\cT$ (they have to be identical for this to work). Note that since the \meta{spath}
% argument is optional, we can make ``local imports'', where the stub $\cT$ is in $\cD$
% and only contains the |\symdef|s needed there.
%
% Note that the recursive (depth-first) nature of the file loads induced by this setup is
% very natural, but can lead to problems with the depth of the file stack in the {\TeX}
% formatter (it is usually set to something like 15\footnote{If you have sufficient rights
% to change your {\TeX} installation, you can also increase the variable
% {\texttt{max\_in\_open}} in the relevant {\texttt{texmf.cnf}} file. Setting it to 50
% usually suffices}). Therefore, it may be necessary to circumvent the recursive load
% pattern providing (logically spurious) |\importmodule| commands. Consider for instance
% module |bar| in Example~\ref{exf:importmodule}, say that |bar| already has load depth
% 15, then we cannot naively import it in this way. If module |bar| depended say on a
% module |base| on the critical load path, then we could add a statement
% \DescribeMacro{\requiremodules} |\requiremodules{../base}| in the second line.  This
% would load the modules from |../base.sms| in advance (uncritical, since it has load
% depth 10) without activating them, so that it would not have to be re-loaded in the
% critical path of the module |foo|. Solving the load depth problem.
% 
% The \DescribeMacro{\inputref}|\inputref| macro behaves just like |\input| in the
% {\LaTeX} workflow, but in the {\latexml} conversion process creates a reference to the
% transformed version of the input file instead.
% 
% \subsection{Using Semantic Macros in Narrative Structures}\label{sec:user:using}
% 
% The |\importmodule| macro establishes the inheritance relation, a transitive relation
% among modules that governs visibility of semantic macros. In particular, it can only be
% used in modules (and has to be used at the top-level, otherwise it is hindered by
% {\LaTeX} groups). In many cases, we only want to \emph{use} the semantic macros in an
% environment (and not re-export them). Indeed, this is the normal situation for most
% parts of mathematical documents. For that \sTeX provides the
% \DescribeMacro{\usemodule}|\usemodule| macro, which takes the same arguments as
% |\importmodule|, but is treated differently in the \sTeX module signatures. A typical
% situation is shown in Figure~\ref{fig:use-ring}, where we open the module |ring| (see
% Figure~\ref{fig:ring}) and use its semantic macros (in the |omtext| environment). In
% earlier versions of \sTeX, we would have to wrap the |omtext| environment in an
% anonymous |module| environment to prevent re-export. 
% 
%\begin{exfig}
% \begin{verbatim}
% \begin{omtext}
%   \usemodule[../algebra/rings.tex]{ring}
%   We $R$ be a ring $(\rbase,\rplus,\rzero,\rminusOp,\rtimes,\rone)$, ...
% \end{omtext}
% \end{verbatim}
% \caption{Using Semantic Macros in Narrative Structures}\label{fig:use-ring}
% \end{exfig}
%
% \subsection{Including Externally Defined Semantic Macros }
% 
% In some cases, we use an existing {\LaTeX} macro package for typesetting objects that
% have a conventionalized mathematical meaning. In this case, the macros are ``semantic''
% even though they have not been defined by a |\symdef|. This is no problem, if we are
% only interested in the {\LaTeX} workflow. But if we want to e.g. transform them to
% {\omdoc} via {\latexml}, the {\latexml} bindings will need to contain references to an
% {\omdoc} theory that semantically corresponds to the {\LaTeX} package. In particular,
% this theory will have to be imported in the generated {\omdoc} file to make it
% {\omdoc}-valid. 
%
% \DescribeMacro{\requirepackage} To deal with this situation, the |modules| package
% provides the |\requirepackage| macro. It takes two arguments: a package name, and a URI
% of the corresponding {\omdoc} theory. In the {\LaTeX} workflow this macro behaves like a
% |\usepackage| on the first argument, except that it can --- and should --- be used
% outside the {\LaTeX} preamble. In the {\latexml} workflow, this loads the {\latexml}
% bindings of the package specified in the first argument and generates an appropriate
% |imports| element using the URI in the second argument.
%
% \section{Limitations \& Extensions}\label{sec:limitations}
% 
% In this section we will discuss limitations and possible extensions of the |modules|
% package. Any contributions and extension ideas are welcome; please discuss ideas,
% requests, fixes, etc on the {\sTeX} TRAC~\cite{sTeX:online}.
% 
% \subsection{Perl Utility \texttt{sms}}\label{sec:limitations:sms}
% 
% Currently we have to use an external perl utility |sms| to extract \sTeX module
% signatures from \sTeX files. This considerably adds to the complexity of the \sTeX
% installation and workflow. If we can solve security setting problems that allows us to
% write to \sTeX module signatures outside the current directory, writing them from \sTeX
% may be an avenue of future development see~\cite[issue \#1522]{sTeX:online} for a
% discussion.
% 
% \subsection{Qualified Imports}\label{sec:limitations:qualified-imports}
% 
% In an earlier version of the \texttt{modules} package we used the \texttt{usesqualified}
% for importing macros with a disambiguating prefix (this is used whenever we have
% conflicting names for macros inherited from different modules). This is not accessible
% from the current interface. We need something like a |\importqualified| macro for this;
% see~\cite[issue \#1505]{sTeX:online}. Until this is implemented the infrastructure is
% turned off by default, but we have already introduced the
% \DescribeMacro{qualifiedimports}|qualifiedimports| option for the future.
% 
% \subsection{Error Messages}\label{sec:limitations:errormsg}
% 
% The error messages generated by the |modules| package are still quite bad. For instance
% if |thyA| does note exists we get the cryptic error message 
% \begin{verbatim}
% ! Undefined control sequence.
% \module@defs@thyA ...hy 
%                        \expandafter \mod@newcomma...
% l.490 ...ortmodule{thyA}
% \end{verbatim}
% This should definitely be improved. 
% 
% \subsection{Crossreferencing}\label{sec:limitations:crossref}
% 
% Note that the macros defined by |\symdef| are still subject to the normal {\TeX} scoping
% rules. Thus they have to be at the top level of a module to be visible throughout the
% module as intended. As a consequence, the location of the |\symdef| elements cannot be
% used as targets for crossreferencing, which is currently supplied by the |statement|
% package~\ctancite{Kohlhase:smms}. A way around this limitation would be to import
% the current module from the \sTeX module signature (see Section~\ref{sec:modules}) via
% the |\importmodule| declaration.
% 
% \subsection{No Forward Imports}\label{sec:limitations:forward-imports}
% 
% {\sTeX} allows imports in the same file via |\importmodule{|\meta{mod}|}|, but due to
% the single-pass linear processing model of {\TeX}, \meta{mod} must be the name of a
% module declared {\emph{before}} the current point. So we cannot have forward imports as
% in \ednote{usemodule should work here; revise}
% \begin{verbatim}
% \begin{module}[id=foo]
%   \importmodule{mod}
%   ...
% \end{module}
% ... 
% \begin{module}[id=mod]
%   ... 
% \end{module}
% \end{verbatim}
% a workaround, we can extract the module \meta{mod} into a file {{{mod.tex}}} and replace
% it with |\sinput{mod}|, as in
% \begin{verbatim}
% \begin{module}[id=foo]
%   \importmodule[load=mod]{mod}
%   ...
% \end{module}
% ... 
% \sinput{mod}
% \end{verbatim}
% then the |\importmodule| command can read |mod.sms| (created via the |sms| utility)
% without having to wait for the module \meta{mod} to be defined.
% 
% \StopEventually{\newpage\PrintIndex\newpage\PrintChanges\newpage\printbibliography}\newpage
%
% \section{The Implementation} 
%
% The |modules| package generates two files: the {\LaTeX} package (all the code between
% {\textlangle\textsf{*package}\textrangle} and {\textsf{\textlangle/package\textrangle}})
% and the {\latexml} bindings (between {\textsf{\textlangle*ltxml\textrangle}} and
% {\textsf{\textlangle/ltxml\textrangle}}). We keep the corresponding code fragments
% together, since the documentation applies to both of them and to prevent them from
% getting out of sync.
%
% \subsection{Package Options}\label{sec:impl:options}
% 
% We declare some switches which will modify the behavior according to the package
% options. Generally, an option |xxx| will just set the appropriate switches to true
% (otherwise they stay false). The options we are not using, we pass on to the |sref|
% package we require next.
%    \begin{macrocode}
%<*package>
\newif\if@modules@mh@\@modules@mh@false
\DeclareOption{mh}{\@modules@mh@true}
\newif\ifmod@show\mod@showfalse
\DeclareOption{showmods}{\mod@showtrue}
\newif\ifaux@req\aux@reqtrue
\DeclareOption{noauxreq}{\aux@reqfalse}
\newif\ifmod@qualified\mod@qualifiedfalse
\DeclareOption{qualifiedimports}{\mod@qualifiedtrue}
\newif\if@mmt\@mmtfalse
\DeclareOption{mmt}{\@mmttrue}
\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{sref}}
\ProcessOptions
%    \end{macrocode}
%
% {\latexml} does not support module options yet, so we do not have to do anything here
% for the {\latexml} bindings. We only set up the {\perl} packages (and tell {\texttt{emacs}}
% about the appropriate mode for convenience  
% 
% The next measure is to ensure that the |sref| and |xcomment| packages are loaded (in the
% right version). For {\latexml}, we also initialize the package inclusions.
%    \begin{macrocode}
\RequirePackage{sref}
\if@modules@mh@\RequirePackage{modules-mh}\fi 
\if@mmt\RequirePackage{mmt}\fi
\RequirePackage{xspace}
\RequirePackage{mdframed}
\RequirePackage{pathsuris}
%    \end{macrocode}
%
% \subsection{Modules and Inheritance}\label{sec:impl:modules}
% 
% We define the keys for the |module| environment and the actions that are undertaken,
% when the keys are encountered.
%
% \begin{macro}{module:cd}
%    This |KeyVal| key is only needed for {\latexml} at the moment; use this to specify a
%    content dictionary name that is different from the module name.
%    \begin{macrocode}
\addmetakey{module}{cd}% no longer used
\addmetakey{module}{load}% ignored
\addmetakey*{module}{title}
\addmetakey*{module}{creators}
\addmetakey*{module}{contributors}
\addmetakey*{module}{srccite}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{module:id}
%   For a module with |[id=|\meta{name}|]|, we have a macro |\module@defs@|\meta{name}
%   that acts as a repository for semantic macros of the current module. I will be called
%   by |\importmodule| to activate them. We will add the internal forms of the semantic
%   macros whenever |\symdef| is invoked. To do this, we will need an unexpended form
%   |\this@module| that expands to |\module@defs@|\meta{name}; we define it first and then
%   initialize |\module@defs@|\meta{name} as empty. Then we do the same for qualified
%   imports as well (if the |qualifiedimports| option was specified). Furthermore, we save
%   the module name in the token register |\mod@id|.
%    \begin{macrocode}
\define@key{module}{id}{%
  \edef\this@module{%
    \expandafter\noexpand\csname module@defs@#1\endcsname%
  }%
  \csgdef{module@defs@#1}{}%
  \ifmod@qualified%
    \edef\this@qualified@module{%
      \expandafter\noexpand\csname module@defs@#1\endcsname%
    }%
    \csgdef{module@defs@qualified@#1}{}%
  \fi%
  \def\mod@id{#1}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{module@heading}
%   Then we make a convenience macro for the module heading. This can be customized. 
%    \begin{macrocode}
\newcounter{module}[section]%
\newrobustcmd\module@heading{%
  \stepcounter{module}%
  \ifmod@show%
    \noindent{\textbf{Module} \thesection.\themodule [\mod@id]}%
    \sref@label@id{Module \thesection.\themodule [\mod@id]}%
    \ifx\module@title\@empty :\quad\else\quad(\module@title)\hfill\\\fi%
  \fi%
}% mod@show
%    \end{macrocode}
% \end{macro}
%
% \begin{environment}{module}
%   Finally, we define the begin module command for the module environment. Much of the
%   work has already been done in the keyval bindings, so this is quite simple. We store
%   the file name (without extension) and extension of the module file in the global
%   macros |\module@|\meta{name}|@path| and |\module@|\meta{name}|@ext|, so that we can
%   use them later. The source of these two macros, |\mod@path| and |\mod@ext|, are
%   defined in |\requiremodules|.
%    \begin{macrocode}
\newenvironment{module}[1][]{%
  \begin{@module}[#1]%
  \ifcsundef{mod@id}{}{% only define if components are!
    \ifcsundef{mod@path}{}{\csxdef{module@\mod@id @path}{\mod@path}}%
    \ifcsundef{mod@ext}{}{\csxdef{module@\mod@id @ext}{\mod@ext}}%
  }%
  \if@mmt\if@importing\else\mmtheory{\mod@id}{????}\fi\fi%
  \module@heading% make the headings
  \ignorespaces}{%
  \if@mmt\if@importing\else\mmtheoryend\fi\fi%
  \end{@module}%
  \ignorespacesafterend%
}%
\ifmod@show\surroundwithmdframed{module}\fi%
%    \end{macrocode}
% \end{environment}
%
% \begin{environment}{@module}
%   A variant of the |module| environment that does not create printed representations (in
%   particular no frames) 
%    \begin{macrocode}
\newenvironment{@module}[1][]{\metasetkeys{module}{#1}}{}%
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\activate@defs}
%   To activate the |\symdef|s from a given module \meta{mod}, we call the macro
%   |\module@defs@|\meta{mod}. But to make sure that every module is activated only once,
%   we only activate if the macro |\module@defs@|\meta{mod} is undefined, and define it
%   directly afterwards to prohibit further activations.
%    \begin{macrocode}
\def\activate@defs#1{%
  \ifcsundef{module@#1@activated}{\csname module@defs@#1\endcsname}{}%
  \@namedef{module@#1@activated}{true}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\export@defs}
%   |\export@defs{|\meta{mod}|}| exports all the |\symdef|s from module \meta{mod} to the
%   current module (if it has the name \meta{currmod}), by adding a call to
%   |\module@defs@|\meta{mod} to the registry |\module@defs@|\meta{currmod}.\ednote{MK: I
%   have the feeling that we may be exporting modules multiple times here, is that a
%   problem?}\ednote{Jinbo: This part of code is extremely easy to generate bugs, cautiously edit this part of code.}\newline
%   Naive understanding of this code: |#1| be will be expanded first, then |\this@module|, then |\active@defs|, then |\g@addto@macro|. 
%    \begin{macrocode}
\def\export@defs#1{%
	\@ifundefined{mod@id}{}{%
		\expandafter\expandafter\expandafter\g@addto@macro%
                \expandafter\this@module\expandafter{\activate@defs{#1}}%
	}%
}%
%    \end{macrocode}
% \end{macro}
%
% Now we come to the implementation of |\importmodule|, but before we do, we define 
% conditional and an auxiliary macro: 
% \begin{macro}{\if@importing} 
%   |\if@importing| can be used to shut up macros in an import situation. 
%    \begin{macrocode}
\newif\if@importing\@importingfalse
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\update@used@modules}
%   This updates the register |\used@modules|
%    \begin{macrocode}
\newcommand\update@used@modules[1]{%
  \ifx\used@modules\@empty%
    \edef\used@modules{#1}%
  \else%
    \edef\used@modules{\used@modules,#1}%
  \fi}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\importmodule} 
%   The |\importmodule[|\meta{file}|]{|\meta{mod}|}| macro is an interface macro that
%   loads \meta{file} and activates and re-exports the |\symdef|s from module
%   \meta{mod}. As we will (probably) need to keep a record of the currently imported modules
%   (top-level only), we divide the functionality into a user-visible macro that records
%   modules in the |\used@modules| register and an internal one (|\@importmodule|)
%   that does the actual work.
%    \begin{macrocode}
\gdef\used@modules{}
\srefaddidkey{importmodule}
\addmetakey{importmodule}{load}
\addmetakey[sms]{importmodule}{ext}
\addmetakey[false]{importmodule}{conservative}[true]
\newcommand\importmodule[2][]{%
  \metasetkeys{importmodule}{#1}%
  \update@used@modules{#2}%
  \@importmodule[\importmodule@load]{#2}{\importmodule@ext}{export}%
  \ignorespacesandpars%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@importmodule} 
%   |\@importmodule[|\meta{filepath}|]{|\meta{mod}|}{|\meta{ext}|}{|\meta{export?}|}|
%   loads \meta{filepath}|.|\meta{ext} (if it is given) and activates the module
%   \meta{mod}. If \meta{export?} is |export|, then it also re-exports the |\symdef|s from
%   \meta{mod}.
%
%   First |\@load| will store the base file name with full path, then check if
%   |\module@|\meta{mod}|@path| is defined. If this macro is defined, a module of this
%   name has already been loaded, so we check whether the paths coincide, if they do, all
%   is fine and we do nothing otherwise we give a suitable error. If this macro is
%   undefined we load the path by |\requiremodules|.
%    \begin{macrocode}
\newcommand\@importmodule[4][]{%
  {\@importingtrue% to shut up macros while in the group opened here
  \edef\@load{#1}%
  \ifx\@load\@empty%
    \relax%
  \else%
    \ifcsundef{module@#2@path}{%
      \requiremodules{#1}{#3}%
    }{%
      \edef\@path{\csname module@#2@path\endcsname}%
      \IfStrEq\@load\@path{% if the known path is the same as the requested one
        \relax% do nothing, it has already been loaded, else signal an error
	  }{%
        \PackageError{modules}
        {{Module Name Clash\MessageBreak
        A module with name #2 was already loaded under the path "\@path"\MessageBreak
        The imported path "\@load" is probably a different module with the\MessageBreak
        same name; this is dangerous -- not importing}%
        {Check whether the Module name is correct}}%
      }%
    }%
  \fi}%
  \activate@defs{#2}% activate the module
  \edef\@export{#4}\def\@@export{export}%prepare comparison
  \ifx\@export\@@export\export@defs{#2}\fi% export the module
  \if@importing\else\if@mmt\mmtinclude{#1?#2}\fi\fi%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\usemodule} 
%   |\usemodule| acts like |\importmodule|, except that the |sms| utility does not
%   transfer it to the module signatures and it does not re-export the symdefs.
%    \begin{macrocode}
\newcommand\usemodule[2][]{%
  \metasetkeys{importmodule}{#1}%
  \update@used@modules{#2}%
  \@importmodule[\importmodule@load]{#2}{\importmodule@ext}{noexport}%
  \ignorespacesandpars%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\withusedmodules} 
%   This variant just imports all the modules in a comma-separated list (usually
%   |\used@modules|)
%    \begin{macrocode}
\newcommand\withusedmodules[2]{{\@for\@I:=#1\do{\activate@defs\@I}{#2}}}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\importOMDocmodule} 
%   for the {\LaTeX} side we can just re-use |\importmodule|, for the {\latexml} side we
%   have a full URI anyways. So things are easy.\ednote{MK@DG: this macro is seldom used,
%   maybe I should just switch arguments.}
%    \begin{macrocode}
\newrobustcmd\importOMDocmodule[3][]{\importmodule[#1]{#3}}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\metalanguage} 
%   |\metalanguage| behaves exactly like |\importmodule| for formatting. For {\latexml},
%   we only add the |type| attribute.
%    \begin{macrocode}
\let\metalanguage=\importmodule%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Semantic Macros}\label{sec:impl:symdef}
% 
% \begin{macro}{\mod@newcommand}
%   We first hack the {\LaTeX} kernel macros to obtain a version of the |\newcommand|
%   macro that does not check for definedness.
%    \begin{macrocode}
\let\mod@newcommand=\providerobustcmd%
%    \end{macrocode}
% \end{macro}
% 
% Now we define the optional KeyVal arguments for the |\symdef| form and the actions that
% are taken when they are encountered.
%
% \begin{environment}{conceptdef}
%    \begin{macrocode}
\srefaddidkey{conceptdef}%
\addmetakey*{conceptdef}{title}%
\addmetakey{conceptdef}{subject}%
\addmetakey*{conceptdef}{display}%
\def\conceptdef@type{Symbol}%
\newrobustcmd\conceptdef[2][]{%
  \metasetkeys{conceptdef}{#1}%
  \ifx\conceptdef@display\st@flow\else{\stDMemph{\conceptdef@type} #2:}\fi%
  \ifx\conceptdef@title\@empty~\else~(\stDMemph{\conceptdef@title})\par\fi%
}%
%    \end{macrocode}
% \ednote{MK@DG: maybe we need to add DefKeyVals here?}
% \end{environment}
% 
% \begin{macro}{symdef:keys}
%   The optional argument local specifies the scope of the function to be defined. If
%   local is not present as an optional argument then |\symdef| assumes the scope of the
%   function is global and it will include it in the pool of macros of the current
%   module. Otherwise, if local is present then the function will be defined only locally
%   and it will not be added to the current module (i.e. we cannot inherit a local
%   function).  Note, the optional key local does not need a value: we write
%   |\symdef[local]{somefunction}[0]{some expansion}|. The other keys are not used in the
%   {\LaTeX} part.
%    \begin{macrocode}
\newif\if@symdeflocal%
\srefaddidkey{symdef}%
\define@key{symdef}{local}[true]{\@symdeflocaltrue}%
\define@key{symdef}{primary}[true]{}%
\define@key{symdef}{assocarg}{}%
\define@key{symdef}{bvars}{}%
\define@key{symdef}{bargs}{}%
\addmetakey{symdef}{name}%
\addmetakey*{symdef}{title}%
\addmetakey*{symdef}{description}%
\addmetakey{symdef}{subject}%
\addmetakey*{symdef}{display}%
%    \end{macrocode}
% \end{macro}
% \ednote{MK@MK: we need to document the binder keys above.}
% \begin{macro}{\symdef}
%    The the |\symdef|, and |\@symdef| macros just handle optional arguments.
%    \begin{macrocode}
\def\symdef{%
  \@ifnextchar[{\@symdef}{\@symdef[]}%
}%
\def\@symdef[#1]#2{%
  \@ifnextchar[{\@@symdef[#1]{#2}}{\@@symdef[#1]{#2}[0]}%
}%
%    \end{macrocode}
% \end{macro}
%
% next we locally abbreviate |\mod@newcommand| to simplify argument passing.
%    \begin{macrocode}
\def\@mod@nc#1{\mod@newcommand{#1}[1]}%
%    \end{macrocode}
% and we copy a very useful piece of code from
% \url{http://tex.stackexchange.com/questions/23100/looking-for-an-ignorespacesandpars},
% it ignores spaces and following implicit paragraphs (double newlines), explicit |\par|s
% are respected however
%    \begin{macrocode}
\def\ignorespacesandpars{%
  \begingroup
  \catcode13=10
  \@ifnextchar\relax
    {\endgroup}%
    {\endgroup}%
}
%    \end{macrocode}
% and more adapted from \url{http://tex.stackexchange.com/questions/179016/ignore-spaces-and-pars-after-an-environment}
%    \begin{macrocode}
\def\ignorespacesandparsafterend#1\ignorespaces\fi{#1\fi\ignorespacesandpars}
\def\ignorespacesandpars{
  \ifhmode\unskip\fi%
  \@ifnextchar\par%
    {\expandafter\ignorespacesandpars\@gobble}%
    {}%
}
%    \end{macrocode}
% 
% \begin{macro}{\@@symdef}
%    now comes the real meat: the |\@@symdef| macro does two things, it adds the macro
%    definition to the macro definition pool of the current module and also provides it.
%    \begin{macrocode}
\def\@@symdef[#1]#2[#3]#4{%
%    \end{macrocode}
% We use a switch to keep track of the local optional argument. We initialize the switch
% to false and set all the keys that have been provided as arguments: |name|, |local|.
%    \begin{macrocode}
  \@symdeflocalfalse%
  \metasetkeys{symdef}{#1}%
%    \end{macrocode}
% If the |mmt| option is set and we are not importing, then we write out the constant
% declaration for this symdef\ednote{eventually we may want to do something about the
% notations. This would pass \#4 to MMT via a macro that makes the \# (argumentmarkers)
% active and empty. I am not clear how well this works, so we leave out notations.}
%    \begin{macrocode}
 \if@mmt\if@importing\else%
\ifx\symdef@name\@empty\mmtconstdec{#2}\else\mmtconstdec{\symdef@name}\fi%
\fi\fi%
%    \end{macrocode}
% First, using |\mod@newcommand| we initialize the intermediate macro
% |\module@|\meta{sym}|@pres@|, the one that can be extended with |\symvariant|
%    \begin{macrocode}
  \expandafter\mod@newcommand\csname modules@#2@pres@\endcsname[#3]{#4}%
%    \end{macrocode}
% and then we define the actual semantic macro, which when invoked with an optional
% argument \meta{opt} calls |\modules@|\meta{sym}|@pres@|\meta{opt} provided by the
% |\symvariant| macro.
%    \begin{macrocode}
  \expandafter\mod@newcommand\csname #2\endcsname[1][]%
  {\csname modules@#2@pres@##1\endcsname}%
%    \end{macrocode}
% Finally, we prepare the internal macro to be used in the |\symref| call.
%    \begin{macrocode}
  \expandafter\@mod@nc\csname mod@symref@#2\expandafter\endcsname\expandafter%
  {\expandafter\mod@termref\expandafter{\mod@id}{#2}{##1}}%
%    \end{macrocode}
% We check if the switch for the local scope is set: if it is we are done, since this
% function has a local scope. Similarly, if we are not inside a module, which we could
% export from.  
%    \begin{macrocode}
  \if@symdeflocal%
  \else%
    \ifcsundef{mod@id}{}{%
%    \end{macrocode}
% Otherwise, we add three functions to the module's pool of defined macros using
% |\g@addto@macro|. We first add the definition of the intermediate function
% |\modules@|\meta{sym}|@pres@|.
%    \begin{macrocode}
      \expandafter\g@addto@macro\this@module%
      {\expandafter\mod@newcommand\csname modules@#2@pres@\endcsname[#3]{#4}}%
%    \end{macrocode}
% Then we add add the definition of |\|\meta{sym}  which calls the intermediate
% function and handles the optional argument.
%    \begin{macrocode}
      \expandafter\g@addto@macro\this@module%
      {\expandafter\mod@newcommand\csname #2\endcsname[1][]%
      {\csname modules@#2@pres@##1\endcsname}}%
%    \end{macrocode}
% We also add |\mod@symref@|\meta{sym} macro to the macro pool so that the |\symref| macro
% can pick it up.
%    \begin{macrocode}
      \expandafter\g@addto@macro\csname  module@defs@\mod@id\expandafter\endcsname\expandafter%
      {\expandafter\@mod@nc\csname mod@symref@#2\expandafter\endcsname\expandafter%
      {\expandafter\mod@termref\expandafter{\mod@id}{#2}{##1}}}%
%    \end{macrocode}
% Finally, using |\g@addto@macro| we add the two functions to the qualified version of the
% module if the |qualifiedimports| option was set.
%    \begin{macrocode}
      \ifmod@qualified%
        \expandafter\g@addto@macro\this@qualified@module%
        {\expandafter\mod@newcommand\csname modules@#2@pres@qualified\endcsname[#3]{#4}}%
        \expandafter\g@addto@macro\this@qualified@module%
        {\expandafter\def\csname#2@qualified\endcsname{\csname modules@#2@pres@qualified\endcsname}}%
      \fi%
    }% mod@qualified
  \fi% symdeflocal
%    \end{macrocode}
% So now we only need to show the data in the symdef, if the options allow. 
%    \begin{macrocode}
  \ifmod@show%
    \ifx\symdef@display\st@flow\else{\noindent\stDMemph{\symdef@type} #2:}\fi%
    \ifx\symdef@title\@empty~\else~(\stDMemph{\symdef@title})\par\fi%
  \fi%
  \ignorespacesandpars%
}% mod@show
\def\symdef@type{Symbol}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\symvariant}
%   |\symvariant{|\meta{sym}|}[|\meta{args}|]{|\meta{var}|}{|\meta{cseq}|}| just extends
%   the internal macro |\modules@|\meta{sym}|@pres@| defined by
%   |\symdef{|\meta{sym}|}[|\meta{args}|]{|\ldots|}| with a variant
%   |\modules@|\meta{sym}|@pres@|\meta{var} which expands to \meta{cseq}. Recall that this
%   is called by the macro |\|\meta{sym}|[|\meta{var}|]| induced by the
%   |\symdef|.\ednote{MK@DG: this needs to be implemented in LaTeXML}
%    \begin{macrocode}
\def\symvariant#1{%
  \@ifnextchar[{\@symvariant{#1}}{\@symvariant{#1}[0]}%
  }%
\def\@symvariant#1[#2]#3#4{%
  \expandafter\mod@newcommand\csname modules@#1@pres@#3\endcsname[#2]{#4}%
%    \end{macrocode}
% and if we are in a named module, then we need to export the function
% |\modules@|\meta{sym}|@pres@|\meta{opt} just as we have done that in |\symdef|.
%    \begin{macrocode}
  \ifcsundef{mod@id}{}{%
    \expandafter\g@addto@macro\this@module%
    {\expandafter\mod@newcommand\csname modules@#1@pres@#3\endcsname[#2]{#4}}%
  }%
\ignorespacesandpars}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\resymdef}
%   This is now deprecated.
%    \begin{macrocode}
\def\resymdef{%
  \@ifnextchar[{\@resymdef}{\@resymdef[]}%
}%
\def\@resymdef[#1]#2{%
  \@ifnextchar[{\@@resymdef[#1]{#2}}{\@@resymdef[#1]{#2}[0]}%
}%
\def\@@resymdef[#1]#2[#3]#4{%
  \PackageError{modules}%
  {The \protect\resymdef macro is deprecated}{use the \protect\symvariant instead!}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\abbrdef}
%   The |\abbrdef| macro is a variant of |\symdef| that does the same on the {\LaTeX}
%   level.
%    \begin{macrocode}
\let\abbrdef\symdef%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Defining Math Operators}\label{sec:impl:defmathop}
%
% \begin{macro}{\DefMathOp} 
% |\DefMathOp[|\meta{key pair}|]{definition}| will take 2 arguments. ||\meta{key pair}|| should be something like |[name=...]|, for example, |[name=equal]|. Though |\setkeys|, |\defmathop@name| will be set. Further definition will be done by |\symdef|.
%    \begin{macrocode}
\define@key{DefMathOp}{name}{%
  \def\defmathop@name{#1}%
}%
\newrobustcmd\DefMathOp[2][]{%
  \setkeys{DefMathOp}{#1}%
  \symdef[#1]{\defmathop@name}{#2}%
}%
%    \end{macrocode}
% \end{macro}
%
%
% \subsection{Axiomatic Assumptions}\label{sec:impl:assumptions}
% 
% \begin{macro}{\assdef} 
%   We fake it for now, not clear what we should do on the {\LaTeX} side.
%    \begin{macrocode}
\newcommand\assdef[2][]{#2}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Semantic Macros for Variables}\label{sec:impl:semvars}
%
% \begin{macro}{\vardef} 
%   We do the argument parsing like in |\symdef| above, but add the |local| key. All the
%   other changes are in the \latexml binding exclusively.
%    \begin{macrocode}
\def\vardef{\@ifnextchar[{\@vardef}{\@vardef[]}}%
\def\@vardef[#1]#2{%
  \@ifnextchar[{\@@vardef[#1]{#2}}{\@@vardef[#1]{#2}[0]}}
\def\@@vardef[#1]#2[#3]#4{%
  \def\@test{#1}%
  \ifx\@test\@empty%
    \@@symdef[local]{#2}[#3]{#4}%
  \else%
    \symdef[local,#1]{#2}[#3]{#4}%
  \fi%
  \ignorespacesandpars}%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Testing Semantic Macros}\label{sec:impl:testing}
%
% \begin{macro}{\symtest}
%   Allows to test a |\symdef| in place, this shuts up when being imported.
%    \begin{macrocode}
\addmetakey{symtest}{name}%
\addmetakey{symtest}{variant}%
\newrobustcmd\symtest[3][]{%
  \if@importing%
  \else%
    \metasetkeys{symtest}{#1}%
    \par\noindent \textbf{Symbol}~%
    \ifx\symtest@name\@empty\texttt{#2}\else\texttt{\symtest@name}\fi%
    \ifx\symtest@variant\@empty\else\ (variant \texttt{\symtest@variant})\fi%
    \ with semantic macro %
    \texttt{\textbackslash #2\ifx\symtest@variant\@empty\else[\symtest@variant]\fi}%
    : used e.g. in \ensuremath{#3}%
  \fi%
  \ignorespacesandpars%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\abbrtest}
%    \begin{macrocode}
\addmetakey{abbrtest}{name}%
\newrobustcmd\abbrtest[3][]{%
  \if@importing%
  \else%
    \metasetkeys{abbrtest}{#1}%
    \par\noindent \textbf{Abbreviation}~%
    \ifx\abbrtest@name\@empty\texttt{#2}\else\texttt{\abbrtest@name}\fi%
    : used e.g. in \ensuremath{#3}%
  \fi%
  \ignorespacesandpars}%
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Symbol and Concept Names}\label{sec:impl:concepts}
%
% \begin{macro}{\termdef} 
%    \begin{macrocode}
\def\mod@true{true}%
\addmetakey[false]{termdef}{local}%
\addmetakey{termdef}{name}%
\newrobustcmd\termdef[3][]{%
  \metasetkeys{termdef}{#1}%
  \expandafter\mod@newcommand\csname#2\endcsname[0]{#3\xspace}%
  \ifx\termdef@local\mod@true%
  \else%
    \ifcsundef{mod@id}{}{%
      \expandafter\g@addto@macro\this@module%
      {\expandafter\mod@newcommand\csname#2\endcsname[0]{#3\xspace}}%
    }%
  \fi%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\capitalize} 
%    \begin{macrocode}
\def\@capitalize#1{\uppercase{#1}}%
\newrobustcmd\capitalize[1]{\expandafter\@capitalize #1}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@termref} 
%   |\mod@termref{|\meta{module}|}{|\meta{name}|}{|\meta{nl}|}| determines whether the
%   macro |\module@|\meta{module}|@path| is defined. If it is, we make it the prefix of a
%   URI reference in the local macro |\@uri|, which we compose to the hyper-reference,
%   otherwise we give a warning.\ednote{MK: this should be rethought, in particular the
%   local reference does not work!}
%    \begin{macrocode}
\def\mod@termref#1#2#3{%
  \def\@test{#3}%
  \@ifundefined{module@defs@#1}{%
    \protect\G@refundefinedtrue%
    \@latex@warning{\protect\termref with unidentified cd "#1": the cd key must reference an active module}%
    \def\@label{sref@#2@target}%
  }%
  {\def\@label{sref@#2@#1@target}}%
  \@ifundefined{module@#1@path}% local reference
    {\sref@hlink@ifh{\@label}{\ifx\@test\@empty #2\else #3\fi}}%
    {\def\@uri{\csname module@#1@path\endcsname.pdf\#\@label}%
    \sref@href@ifh{\@uri}{\ifx\@test\@empty #2\else #3\fi}}%
}%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Dealing with Multiple Files}\label{sec:impl:multiple}
%
% We use the |pathsuris| package deals with the canonicalization of paths. |\@cpath| will
% canonicalize a path and store the result into |\@CanPath|. To print a canoncalized path,
% simply use |\cpath{|\meta{path}|}|.
% 
% \begin{macro}{\@rinput}
%   |\@rinput{|\meta{path to the current file without extension}|}{|\meta{extension}|}| allows loading 
%   modules with relative path. For example, |\@rinput{foo/bar/B}{tex}| will load |foo/bar/B.tex|.
%   \ednote{Jinbo: How to handle |mod@path|?}
%    \begin{macrocode}
\def\CurrentDir{}%
\newrobustcmd{\@rinput}[2]{%
  \@cpath{\CurrentDir#1}%
  \StrCut[\value{RealAddrNum}]{/\@CanPath}{/}\@TempPath\@Rubbish%
  \StrCut[1]{\@TempPath/}{/}\@Rubbish\@DirPath%
  \edef\CurrentDir{\@DirPath}%
%  \edef\mod@path{}% what should I put in here???
%  \edef\mod@ext{}%
  \input{\@CanPath.#2}%
  \def\CurrentDir{}%
}%
%    \end{macrocode}
% \end{macro} 
%
% \subsection{Loading Module Signatures}
%
% \subsubsection{Selective Inclusion}
%
% \begin{macro}{\requiremodules}
%   this macro loads the modules in a file and makes sure that no text is deposited (we
%   set the flags |\mod@showfalse| and |\@importingtrue| in the local group). It also
%   remembers the file name and extension in |\mod@path| and |\mod@ext| so that
%   |\begin{module}| can pick them up later.
%    \begin{macrocode}
\newrobustcmd\requiremodules[2]{%
  \mod@showfalse%
  \@importingtrue% save state and ensure silence while reading sms
  \edef\mod@path{#1}%
  \edef\mod@ext{#2}% set up path/ext
  \input{#1.#2}%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\@requiremodules}
%   the internal version of |\requiremodules| for use in the |*.aux| file. We disable it
%   at the end of the document, so that when the |aux| file is read again, nothing is
%   loaded.
%    \begin{macrocode}
\newrobustcmd\@requiremodules[2]{%
  \if@tempswa\requiremodules{#1}{#2}\fi%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\inputref}
%   |\inputref{|\meta{path to the current file without extension}|}| supports both
%   absolute path and relative path, meanwhile, records the path and the extension (not
%   for relative path).  \ednote{MK: maybe do something with a non-standard
%   (i.e. non-\texttt{tex}) extension with an optional argument?}
%    \begin{macrocode}
\newrobustcmd\inputref[2][]{%
  \def\@Slash{/}
  \edef\@load{#2}%
  \StrChar{\@load}{1}[\@testchar]
  \ifx\@testchar\@Slash%
    \edef\mod@path{#2}%
    \edef\mod@ext{tex}%
    \input{#2}%
  \else%
    \@rinput{#2}{tex}%
  \fi%
}%
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Including Externally Defined Semantic Macros }\label{sec:impl:packages}
% 
% \begin{macro}{\requirepackage}
%    \begin{macrocode}
\def\requirepackage#1#2{\makeatletter\input{#1.sty}\makeatother}%
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Deprecated Functionality}\label{sec:impl:deprecated}
%
% \begin{macro}{\sinput*}
%    \begin{macrocode}
\newrobustcmd\sinput[1]{%
  \PackageError{modules}%
  {The \protect\sinput macro is deprecated}{use the \protect\input instead!}%
}%
\newrobustcmd\sinputref[1]{%
  \PackageError{modules}%
  {The \protect\sinputref macro is deprecated}{use the \protect\inputref instead!}%
}%
%    \end{macrocode}
% \end{macro}
%
% In this section we centralize old interfaces that are only partially supported any more. 
% \begin{macro}{module:uses}
%   For each the module name |xxx| specified in the |uses| key, we activate their symdefs
%   and we export the local symdefs.\ednote{this issue is deprecated, it will be removed
%     before 1.0.}
%    \begin{macrocode}
\define@key{module}{uses}{%
  \@for\module@tmp:=#1\do{\activate@defs\module@tmp\export@defs\module@tmp}%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{module:usesqualified}
%   This option operates similarly to the module:uses option defined above. The only
%   difference is that here we import modules with a prefix. This is useful when two
%   modules provide a macro with the same name.
%    \begin{macrocode}
\define@key{module}{usesqualified}{%
  \@for\module@tmp:=#1\do{\activate@defs{qualified@\module@tmp}\export@defs\module@tmp}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\coolurion/off}
%    \begin{macrocode}
\def\coolurion{\PackageWarning{modules}{coolurion is obsolete, please remove}}%
\def\coolurioff{\PackageWarning{modules}{coolurioff is obsolete, please remove}}%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Experiments}
% In this section we develop experimental functionality. Currently support for complex
% expressions, see
% \url{https://svn.kwarc.info/repos/stex/doc/blue/comlex_semmacros/note.pdf} for details.
%
% \begin{macro}{\csymdef}
% For the {\LaTeX} we use |\symdef| and forget the last argument. The code here is just
% needed for parsing the (non-standard) argument structure. 
%    \begin{macrocode}
\def\csymdef{\@ifnextchar[{\@csymdef}{\@csymdef[]}}%
\def\@csymdef[#1]#2{%
  \@ifnextchar[{\@@csymdef[#1]{#2}}{\@@csymdef[#1]{#2}[0]}%
}%
\def\@@csymdef[#1]#2[#3]#4#5{%
  \@@symdef[#1]{#2}[#3]{#4}%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\notationdef}
% For the {\LaTeX} side, we just make |\notationdef| invisible.
%    \begin{macrocode}
\def\notationdef[#1]#2#3{}
%    \end{macrocode}
% \end{macro}
% 
% The code for avoiding duplicate loading is very very complex and brittle (and does not
% quite work). Therefore I would like to replace it with something better. It has two
% parts: 
% \begin{itemize}
% \item keeping a registry of file paths, and only loading when the file path has not been
%   mentioned in that, and
% \item dealing with relative paths (for that we have to string together prefixes and pass
%   them one)
% \end{itemize}
% For the first problem, there is a very nice and efficient solution using |etoolbox| which
% I document below. If I decide to do away with relative paths, this would be it.
% 
% \begin{macro}{\reqmodules}
%   We keep a file path registry |\@register| and only load a module signature, if it is
%   not in there.
%    \begin{macrocode}
\newrobustcmd\reqmodules[2]{%
  \ifinlist{#1}{\@register}{}{\listadd\@register{#1}\input{#1.#2}}%
}%
%    \end{macrocode}
% \end{macro}
% for the relative paths, I have to find out the directory prefix and the file name. Here
% are two helper functions, which work well, but do not survive being called in an
% |\edef|, which is what we would need. First some preparation: we set up a path parser
%    \begin{macrocode}
\newcounter{@pl}
\DeclareListParser*{\forpathlist}{/}
%    \end{macrocode}
%
% \begin{macro}{\file@name}
%   |\file@name| selects the filename of the file path: |\file@name{/foo/bar/baz.tex}| is
%   |baz.tex|.
%    \begin{macrocode}
\def\file@name#1{%
  \setcounter{@pl}{0}%
  \forpathlist{\stepcounter{@pl}\listadd\@pathlist}{#1}
  \def\do##1{%
    \ifnumequal{\value{@pl}}{1}{##1}{\addtocounter{@pl}{-1}}
  }%
  \dolistloop{\@pathlist}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\file@path}
%   |\file@path| selects the path of the file path |\file@path{/foo/bar/baz.tex}| is
%   |/foo/bar|
%    \begin{macrocode}
\def\file@path#1{%
  \setcounter{@pl}{0}%
  \forpathlist{\stepcounter{@pl}\listadd\@pathlist}{#1}%
  \def\do##1{%
    \ifnumequal{\value{@pl}}{1}{}{%
      \addtocounter{@pl}{-1}%
      \ifnumequal{\value{@pl}}{1}{##1}{##1/}%
    }%
  }%
  \dolistloop{\@pathlist}%
}%
%</package>
%    \end{macrocode}
% \end{macro}
% what I would really like to do in this situation is 
% \begin{macro}{\NEWrequiremodules}
%   but this does not work, since the |\file@name| and |\file@path| do not survive the
%   |\edef|.
%    \begin{macrocode}
\def\@NEWcurrentprefix{}
\def\NEWrequiremodules#1{%
  \def\@pref{\file@path{#1}}%
  \ifx\@pref\@empty%
  \else%
    \xdef\@NEWcurrentprefix{\@NEWcurrentprefix/\@pref}%
  \fi%
  \edef\@input@me{\@NEWcurrentprefix/\file@name{#1}}%
  \message{requiring \@input@me}\reqmodule{\@input@me}%
}%
%    \end{macrocode}
% \end{macro}
% \Finale
\endinput
%%% Local Variables: 
%%% mode: doctex
%%% TeX-master: t
%%% End: 
% LocalWords:  GPL structuresharing STR dtx env envfalse idfalse displayfalse filedate nl
% LocalWords:  usesfalse usesqualified usesqualifiedfalse envtrue idtrue CPERL Rares pres
% LocalWords:  usestrue displaytrue usesqualifiedtrue RequirePackage keyval tmp 2oms04 eg
% LocalWords:  defs foreach LookupValue activateScope DefEnvironment keyvals cd varpres
% LocalWords:  OptionalKeyVals getValue toString AssignValue openElement omdoc uvee vee
% LocalWords:  closeElement beforeDigest useTheoryItemizations afterDigestBegin symtest
% LocalWords:  whatsit setProperty getArg qw symdef  iffalse importOMDocmodule symtest ci
% LocalWords:  DefKeyVal Semiverbatim symdeflocal atqualified DefMacro STDERR setst spath
% LocalWords:  args unlist DefPrimitive nargs Stringify eq attr omcd ltx XMTok abbrtest
% LocalWords:  convertLaTeXArgs scriptpos XMApp OMA XMArg simpl abbrtest 2oms04 circ ary
% LocalWords:  blaaaa savedprefix aaa simplhelp tust tist tost reguse spath baz rangle
% LocalWords:  updatedpre ReturnAfterFi updateall updatedpost updatesms bgroup includeref
% LocalWords:  texclude tinclude getGullet requiredmodule tex sms egroup pmml sincluderef
% LocalWords:  toks mixfixi mixfixa mixfixii mixfixia mixfixai mixfixiii arg cr OPaths
% LocalWords:  undef tok PARAM thyid BerFieMas inparaenum omsemvar vardef vardef mhview
% LocalWords:  getString showfalse showtrue xcomment stex srcref KeyVal omext osslepsdl13
% LocalWords:  beginItemize getProperty introdcue afterOpen numberIt Tokenize mathhub
% LocalWords:  OptionalSemiverbatim omdocmod PushValue assocarg getStomach prs HorIacJuc
% LocalWords:  begingroup beginMode endMode endgroup insertElement resymdef sym cscpnrr11
% LocalWords:  updir nargkey PresFormatters mixfixaii formatters argname expr behavior
% LocalWords:  getSymmdefProperties XMath mcdcr exprlist recurse texttt scsys foobar mrow
% LocalWords:  textbackslash newcommand providecommand sc sc mathml openmath nx st@flow
% LocalWords:  latexml cmathml activemath twintoo atwin atwintoo mathcal Deyan viewsketch
% LocalWords:  mathcal fileversion Ginev maketitle  newpage infty ulsmf08 exfig endinput
% LocalWords:  omsemmac lstset basicstyle scriptsize aboveskip belowskip hline mh-variant
% LocalWords:  morekeywords lstlisting csymbol showmods foo exf cseq mdframed usemhmodule
% LocalWords:  qualifiedimports qualifiedimports termdef textbf filepath RabKoh mhinput
% LocalWords:  symname varSmoothfunctionsOn ednote abbrdef Sumfromto semmodule mhinputref
% LocalWords:  vspace hrule vspace arith arbitraryn xbool oplus xdisjunction tw mhinput
% LocalWords:  emph capitalize ldots termref termref symref symref ctancite nc mhinputref
% LocalWords:  smms hyperref RahObe hmlmh10 widehat texmf.cnf requiremodules cs 2oms04
% LocalWords:  sinput sinputref sinputref cname csname 2oms04
% LocalWords:  OPhats usepackage importqualified Crossreferencing jobname ltxml etoolbox
% LocalWords:  jobname printbibliography textsf langle textsf langle textlangle listadd
% LocalWords:  textrangle textlangle newif ifmod qualifiedfalse qualifiedtrue usemhmodule
% LocalWords:  sref xspace expandafter noexpand endcsname namedef setkeys ifx mh-variants
% LocalWords:  newenvironment parentmod usemodule ifundefined coolurion cooluri reqmodule
% LocalWords:  coolurioff cwd ouri ifdefinable testopt ifnextchar xargdef bvars 2oms04
% LocalWords:  argdef yargdef somefunction symdeflocaltrue bvar xpath assoc qr reqmodules
% LocalWords:  symdeflocalfalse localpres isbound symdefs COMPLEXTOKEN localp  fromrepos
% LocalWords:  findnodes localname carg renewcommand bbb showmeta showmeta exp ifnumequal
% LocalWords:  refundefinedtrue subsubsection blaaa makeatletter makeatother rm ifinlist
% LocalWords:  ifmodules gdef xdef xdef modulestrue modulesfalse pathpostfix abbreviative
% LocalWords:  updatedsms newreg xref texorpdfstring srefaddidkey newsavebox importmodule
% LocalWords:  viewbox newcounter thesection theview theproblem hfill lrbox req torepos
% LocalWords:  stepcounter textwidth hbox noindent smallskip fbox vbox usebox forpathlist
% LocalWords:  smallskip newxcomment vassign ensuremath mapsto doctex tocdepth dolistloop
% LocalWords:  setcounter tableofcontents mathbb symvariant importmodulevia  assdef Jinbo
% LocalWords:  importmodulevia compactdesc tassign tassign tname source-tname frompath
% LocalWords:  ttassign metakeys addmetakey themodule metasetkeys aftergroup addtocounter
% LocalWords:  groupling requation IMPORTCD CURRENTCD bindargs defmathop cnode topath
% LocalWords:  icvariant aftercounter prestok inputref oref loadfrom loadto customization
% LocalWords:  csymdef notationdef noauxreq noauxreq rinput ifaux reqtrue bargs assdef
% LocalWords:  reqfalse currmod importmoduleenv conceptdef stDMemph  tempswa mhviewsketch
% LocalWords:  auxout omtext surroundwithmdframed ignorespaces NeedsTeXFormat lstinline
%  LocalWords:  modularizations conventionalized initialize xstring srccite csgdef csxdef
%  LocalWords:  customized newrobustcmd ifcsundef definedness providerobustcmd cpath
%  LocalWords:  canonicalization canonicalize canoncalized RealAddrNum itemize
%  LocalWords:  NEWrequiremodules