From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 22 May 2002 17:07:58 +0000 (+0000)
Subject: constant string quoting was fixed
X-Git-Tag: V_0_3_0_debian_8~81
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cd7145b8ad4118a9854eaff0feced9352ab87e94;p=helm.git

constant string quoting was fixed
---

diff --git a/helm/mathql/grammar.txt b/helm/mathql/grammar.txt
index 1408b0d24..4f2ff8c76 100644
--- a/helm/mathql/grammar.txt
+++ b/helm/mathql/grammar.txt
@@ -34,9 +34,9 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
        |  FALSE                                (* falso *)
        |  <string> IS <string>                 (* case sensitive matching *)
        
-<pattern> := <quoted-constant-string>          (* pattern costante *)
+<pattern> := <"-quoted-constant-string>        (* pattern costante *)
           
-<string> := <quoted-constant-string>           (* costante letterale *)
+<string> := <'-quoted-constant-string>         (* costante letterale *)
          |  CONCLUSION | HYPOTHESIS | BODY     (* costanti simboliche *)
          |  MAINCONCLUSION | MAINHYPOTHESIS
          |  <rvar>                             (* variabile *)
@@ -104,11 +104,17 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
   (cioe` delle uri eventualmente seguite da un fragment identifier)
   L'espressione regolare contiene i seguenti costrutti:
 
-  costrutto        semanticamente fa match con
-  ?                un singolo carattere diverso da / e #
-  *                la piu' lunga sottostringa che non contiene / e #
-  **               la piu' lunga sottostringa che non contiene #
+  costrutto        semanticamente fa match con                       
+  ?                un singolo carattere diverso da / # :             
+  *                la piu' lunga sottostringa che non contiene / # : 
+  **               la piu' lunga sottostringa che non contiene # :
   altro carattere  solo se' stesso
 
-  Il costrutto ? non puo' comparire nella parte dell'espressione che
-  fa match con un fragment identifier (tutti gli altri si).
+  costrutto        puo' appareire in
+  ?                "body"
+  *                dovunque
+  **               "body" e "fragment"
+  altro carattere  dovunque
+
+  "body"     parte compresa fra le occorrenze di ":/" e "#1" escluse
+  "fragment" parte successiva all'occorrenza "#1"