]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mathql/xmathql.dtd
Modified Files:
[helm.git] / helm / mathql / xmathql.dtd
index f875f1022bc820351c64b8a72e7f83c606f833f9..a5bd242e7b108bd98d09e8386aba45db3527edcf 100644 (file)
@@ -99,7 +99,7 @@
 
 <!ELEMENT ConstructorsOf %queryexpr;>
 
-<!ELEMENT Pattern (Prefix, (TokenList, (Extension, FragmentID?)?)?)>
+<!ELEMENT Pattern (Prefix, TokenList, (FragmentID?))>
 
 <!ELEMENT InTheory (%queryexpr;, ItemType)>
 
 
 <!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 -->