summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/schema/rng/omdocdg.rng
blob: 735bfd6ed89d39f0ae1464688664638810ec0e52 (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
<?xml version="1.0" encoding="UTF-8"?>
<!--
  A RelaxNG schema for Open Mathematical documents (OMDoc 1.3) Module CTH 
  $Id: omdocdg.rnc 8958 2011-09-02 06:01:13Z kohlhase $
  $HeadURL: https://svn.omdoc.org/repos/omdoc/branches/omdoc-1.3/schema/rnc/omdocdg.rnc $
  See the documentation and examples at http://www.omdoc.org
  Copyright (c) 2004-2007 Michael Kohlhase, released under the GNU Public License (GPL) 
-->
<grammar ns="http://omdoc.org/ns" xmlns:omdoc="http://omdoc.org/ns" xmlns="http://relaxng.org/ns/structure/1.0">
  <define name="omdoc.class" combine="interleave">
    <interleave>
      <zeroOrMore>
        <ref name="decomposition"/>
      </zeroOrMore>
      <zeroOrMore>
        <ref name="path-just"/>
      </zeroOrMore>
    </interleave>
  </define>
  <define name="omdoccth.theory-inclusion.justification" combine="interleave">
    <zeroOrMore>
      <ref name="decomposition"/>
    </zeroOrMore>
  </define>
  <define name="omdoccth.axiom-inclusion.justification" combine="interleave">
    <zeroOrMore>
      <ref name="path-just"/>
    </zeroOrMore>
  </define>
  <define name="decomposition.attribs">
    <interleave>
      <ref name="toplevel.attribs"/>
      <optional>
        <ref name="for.attrib"/>
      </optional>
      <attribute name="links">
        <ref name="omdocrefs"/>
      </attribute>
    </interleave>
  </define>
  <define name="decomposition.model">
    <empty/>
  </define>
  <define name="decomposition">
    <element name="decomposition">
      <choice>
        <ref name="tref"/>
        <interleave>
          <ref name="decomposition.attribs"/>
          <ref name="decomposition.model"/>
        </interleave>
      </choice>
    </element>
  </define>
  <!--
    attribute 'for' points to a 'theory-inclusion', which this 
    element justifies; attribute 'links' is an URIrefs, points to a 
    list of axiom-inlcusions and theory-inclusions
  -->
  <define name="path-just.attribs">
    <interleave>
      <optional>
        <ref name="for.attrib"/>
      </optional>
      <ref name="id.attribs"/>
      <attribute name="local">
        <ref name="omdocref"/>
      </attribute>
      <attribute name="globals">
        <ref name="omdocrefs"/>
      </attribute>
    </interleave>
  </define>
  <define name="path-just.model">
    <empty/>
  </define>
  <define name="path-just">
    <element name="path-just">
      <choice>
        <ref name="tref"/>
        <interleave>
          <ref name="path-just.attribs"/>
          <ref name="path-just.model"/>
        </interleave>
      </choice>
    </element>
  </define>
</grammar>
<!--
  attribute 'local' is an URIref, points to axiom-inclusion
            'globals' is an URIrefs, points to a list of theory-inclusions
-->