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

diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index f875f1022..7b4f71045 100644
--- a/helm/mathql/xmathql.dtd
+++ b/helm/mathql/xmathql.dtd
@@ -50,13 +50,11 @@
 <!ENTITY % position '(Conclusion|Hypothesis|Body|MainConclusion|
                         MainHypothesis)'>
 
-<!ENTITY % order '(ascendant|descendant)'>
-
 <!ENTITY % bool '(True|False)'>
 
 <!-- MathQL query expression declaration -->
 
-<!ENTITY % queryexpr '(Union|Intersect|Diff|SortBy|Select|Exists|Use|UsedBy|
+<!ENTITY % queryexpr '(Union|Intersect|Diff|Select|Exists|Use|UsedBy|
                    ConstructorsOf|Pattern|InTheory|TheoryRefTo|TypeOf|
                    SuperTypeOf|SubTypeOf|Group)'>
 
@@ -83,8 +81,6 @@
 
 <!ELEMENT Diff (%queryexpr;, %queryexpr;)>
 
-<!ELEMENT SortBy (%queryexpr;, SortField)>
-
 <!ELEMENT Select (In, Where)>
 
 <!ELEMENT Exists (In, Where)>
@@ -99,7 +95,7 @@
 
 <!ELEMENT ConstructorsOf %queryexpr;>
 
-<!ELEMENT Pattern (Prefix, (TokenList, (Extension, FragmentID?)?)?)>
+<!ELEMENT Pattern (Prefix, TokenList, (FragmentID?))>
 
 <!ELEMENT InTheory (%queryexpr;, ItemType)>
 
@@ -123,10 +119,6 @@
 
 <!-- MathQL query sub-expressions -->
 
-<!ELEMENT SortField %functexpr;>
-<!ATTLIST SortField 
-          order %order; #IMPLIED>
-
 <!ELEMENT In %queryexpr;>
 
 <!ELEMENT Where %boolexpr;>
@@ -141,13 +133,21 @@
 
 <!ELEMENT QUESTIONMARK EMPTY>
 
-<!ELEMENT TokenList (CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)+>
+<!ELEMENT NUMBER EMPTY>
+<!ATTLIST NUMBER
+          value NMTOKEN #REQUIRED>
 
-<!ELEMENT Prefix (#PCDATA)>
+<!-- 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 Extension (#PCDATA)>
+<!ELEMENT Prefix (CONST|STAR)>
 
-<!ELEMENT FragmentID (#PCDATA)>
+<!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
+<!ELEMENT FragmentID (NUMBER|TWOSTARS|STAR)+>
 
 <!-- MathQL boolean expressions -->