summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocdg.rnc
blob: af5cfe2fc5bc151200d0fa09528e31131d31cde7 (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
# 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) 

default namespace omdoc = "http://omdoc.org/ns"

omdoc.class &= decomposition* & path-just*
omdoccth.theory-inclusion.justification &= decomposition*
omdoccth.axiom-inclusion.justification  &= path-just*

decomposition.attribs = toplevel.attribs & for.attrib? &
	                               attribute links {omdocrefs}
decomposition.model = empty
decomposition = element decomposition {tref|(decomposition.attribs & decomposition.model)}
# 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

path-just.attribs = for.attrib? & id.attribs & 
	    	    	       attribute local {omdocref} & 
            	    	       attribute globals {omdocrefs}
path-just.model = empty
path-just = element path-just {tref|(path-just.attribs & path-just.model)}
# attribute 'local' is an URIref, points to axiom-inclusion
#           'globals' is an URIrefs, points to a list of theory-inclusions