Modified Files:

[helm.git] / helm / mathql / xmathql.dtd

diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index 57b663f73c0264518b2a04eed766f9c8db4136b3..e32b0299fb7dbe57b8a7289fb0de99288cc6273e 100644 (file)
--- a/helm/mathql/xmathql.dtd
+++ b/helm/mathql/xmathql.dtd
@@ -43,6 +43,8 @@
 <!-- Operators are unambiguous (binary or unary), so there isn't any -->
 <!-- grouping operator.                                              -->
 <!-- CONST is the constant string.                                   -->
+<!-- The attributes binder and rvar declare variables which are      -->
+<!-- referred to and used by means of respectively BINDER and RVAR   -->
 <!--*****************************************************************-->
 
 <!ENTITY % position '(Conclusion|Hypothesis|Body|MainConclusion|
@@ -97,9 +99,7 @@
 
 <!ELEMENT ConstructorsOf %queryexpr;>
 
-<!ELEMENT Pattern EMPTY>
-<!ATTLIST Pattern
-          arg CDATA #REQUIRED>
+<!ELEMENT Pattern (Prefix, TokenList, (FragmentID?))>
 
 <!ELEMENT InTheory (%queryexpr;, ItemType)>
 
@@ -133,6 +133,30 @@
 <!ATTLIST Where
           rvar CDATA #REQUIRED>
 
+<!ELEMENT STAR EMPTY>
+
+<!ELEMENT TWOSTARS EMPTY>
+
+<!ELEMENT SLASH EMPTY>
+
+<!ELEMENT QUESTIONMARK EMPTY>
+
+<!ELEMENT NUMBER EMPTY>
+<!ATTLIST NUMBER
+          value NMTOKEN #REQUIRED>
+
+<!-- STAR expands only to objects of the specified dir before the last "/": 
+     ex. cic:/Algebra/* expands to every object in Algebra only            -->
+<!-- TWOSTARS expands till the most complete name (with extension if not 
+     specifified)                                                          -->
+<!-- QUESTIONMARK matches one character except "/"                         --> 
+<!ELEMENT TokenList (CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)+>
+
+<!ELEMENT Prefix (#PCDATA)>
+
+<!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
+<!ELEMENT FragmentID ((NUMBER|STAR), (NUMBER|STAR)?)>
+
 <!-- MathQL boolean expressions -->
 
 <!ELEMENT AND (%boolexpr;, %boolexpr;)>
@@ -148,6 +172,7 @@
           value %bool; #REQUIRED>
 
 <!-- MathQL string expressions -->
+
 <!ELEMENT CONST (#PCDATA)>
 
 <!ELEMENT RVAR EMPTY>
@@ -164,14 +189,14 @@
 
 <!ELEMENT NAME (RVAR)>
 
-<!ELEMENT PROPERTY (RVAR|CONST)>
+<!ELEMENT PROPERTY (RVAR)>
 <!ATTLIST PROPERTY
           name CDATA #REQUIRED>
 
-<!ELEMENT SUPERPROPERTY  (RVAR|CONST)>
+<!ELEMENT SUPERPROPERTY (RVAR)>
 <!ATTLIST SUPERPROPERTY
           name CDATA #REQUIRED>
 
-<!ELEMENT SUBPROPERTY (RVAR|CONST)>
+<!ELEMENT SUBPROPERTY (RVAR)>
 <!ATTLIST SUBPROPERTY
           name CDATA #REQUIRED>
\ No newline at end of file