summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocdg.rnc
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocdg.rnc')
-rw-r--r--Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocdg.rnc28
1 files changed, 28 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocdg.rnc b/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocdg.rnc
new file mode 100644
index 00000000000..af5cfe2fc5b
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocdg.rnc
@@ -0,0 +1,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
+