From: Ferruccio Guidi 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 *) | IS (* case sensitive matching *) - := (* pattern costante *) + := <"-quoted-constant-string> (* pattern costante *) - := (* costante letterale *) + := <'-quoted-constant-string> (* costante letterale *) | CONCLUSION | HYPOTHESIS | BODY (* costanti simboliche *) | MAINCONCLUSION | MAINHYPOTHESIS | (* 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"