From 4ac2712b2a615135ecd00ae2501d341ecaa143ab Mon Sep 17 00:00:00 2001
From: Irene Schena <irene.schena@unibo.it>
Date: Tue, 3 Sep 2002 14:55:02 +0000
Subject: [PATCH] Added Files: 1)result.xml xmqlresult.dtd: example and dtd for
 MathQL query results

---
 helm/mathql/result.xml     | 20 +++++++++++++
 helm/mathql/xmqlresult.dtd | 59 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 79 insertions(+)
 create mode 100644 helm/mathql/result.xml
 create mode 100644 helm/mathql/xmqlresult.dtd

diff --git a/helm/mathql/result.xml b/helm/mathql/result.xml
new file mode 100644
index 000000000..dc79c0879
--- /dev/null
+++ b/helm/mathql/result.xml
@@ -0,0 +1,20 @@
+<?xml version="1.0" encoding="ISO-8859-1"?>
+
+<!DOCTYPE MQLresult SYSTEM "xmqlresult.dtd">
+
+<!-- To validate: xmllint -valid -loaddtd -noout result.xml -->
+
+<MQLresult>
+ <ResourceSet>
+  <RESOURCE name="cic:/Coq/Init/Logic/Equality/eq.ind">
+   <AttributeSet>
+    <ATTRIBUTE name="POSITION">
+     <CONST>MainHypothesis</CONST>
+    </ATTRIBUTE>
+    <ATTRIBUTE name="POSITION">
+     <CONST>InConclusion</CONST>
+    </ATTRIBUTE>
+   </AttributeSet>
+  </RESOURCE>
+ </ResourceSet>
+</MQLresult>
diff --git a/helm/mathql/xmqlresult.dtd b/helm/mathql/xmqlresult.dtd
new file mode 100644
index 000000000..9b3333d38
--- /dev/null
+++ b/helm/mathql/xmqlresult.dtd
@@ -0,0 +1,59 @@
+<?xml version="1.0" encoding="ISO-8859-1"?>
+
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
+<!--*****************************************************************-->
+<!-- DTD for RESULTS of XMathQL queries                              -->
+<!-- First draft: September 2002, Irene Schena                       -->
+<!--*****************************************************************-->
+
+
+<!-- MQL result expression declaration -->
+
+<!ENTITY % resultexpr '(ResourceSet)'>
+
+
+<!-- MQL result top-element -->
+
+<!ELEMENT MQLresult %resultexpr;>
+
+<!-- Result expressions and sub-expressions -->
+
+<!ELEMENT ResourceSet (RESOURCE*)>
+
+<!ELEMENT RESOURCE (AttributeSet*)>
+<!ATTLIST RESOURCE
+          name CDATA #REQUIRED>
+
+<!ELEMENT AttributeSet (ATTRIBUTE+)>
+
+<!ELEMENT ATTRIBUTE (CONST*)>
+<!ATTLIST ATTRIBUTE
+          name CDATA #REQUIRED>
+
+<!-- MQL result string expressions -->
+
+<!ELEMENT CONST (#PCDATA)>
+
-- 
2.39.2