X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fxmathql.dtd;h=f875f1022bc820351c64b8a72e7f83c606f833f9;hb=7b7d26322d3bd9be8d6cdde79c74ff38e921290b;hp=57b663f73c0264518b2a04eed766f9c8db4136b3;hpb=ca6aaf6c6b4c5fc37ef61c56ed6fc9d81c76b626;p=helm.git

diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index 57b663f73..f875f1022 100644
--- 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, (Extension, FragmentID?)?)?)>
 
 <!ELEMENT InTheory (%queryexpr;, ItemType)>
 
@@ -133,6 +133,22 @@
 <!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;)>
@@ -148,6 +164,7 @@
           value %bool; #REQUIRED>
 
 <!-- MathQL string expressions -->
+
 <!ELEMENT CONST (#PCDATA)>
 
 <!ELEMENT RVAR EMPTY>
@@ -164,14 +181,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