]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mathql/xmathql.dtd
Modified Files:
[helm.git] / helm / mathql / xmathql.dtd
index 57b663f73c0264518b2a04eed766f9c8db4136b3..f875f1022bc820351c64b8a72e7f83c606f833f9 100644 (file)
@@ -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, (Extension, FragmentID?)?)?)>
 
 <!ELEMENT InTheory (%queryexpr;, ItemType)>
 
 <!ATTLIST Where
           rvar CDATA #REQUIRED>
 
+<!ELEMENT STAR EMPTY>
+
+<!ELEMENT TWOSTARS EMPTY>
+
+<!ELEMENT SLASH EMPTY>
+
+<!ELEMENT QUESTIONMARK EMPTY>
+
+<!ELEMENT TokenList (CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)+>
+
+<!ELEMENT Prefix (#PCDATA)>
+
+<!ELEMENT Extension (#PCDATA)>
+
+<!ELEMENT FragmentID (#PCDATA)>
+
 <!-- MathQL boolean expressions -->
 
 <!ELEMENT AND (%boolexpr;, %boolexpr;)>
           value %bool; #REQUIRED>
 
 <!-- MathQL string expressions -->
+
 <!ELEMENT CONST (#PCDATA)>
 
 <!ELEMENT RVAR EMPTY>
 
 <!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