New syntax -H1 .. Hn for clear

[helm.git] / matita / components / grafite / grafiteAst.ml

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index e32131a0670afb1819b1b057e197fe0f9e3887a5..32a29c2158a98e8f1dda73f10191a6a6f6fe3d54 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -41,6 +41,7 @@ type ntactic =
    | NCases of loc * NotationPt.term * npattern  
    | NCase1 of loc * string
    | NChange of loc * npattern * NotationPt.term
+   | NClear of loc * string list
    | NConstructor of loc * int option * NotationPt.term list
    | NCut of loc * NotationPt.term
 (* | NDiscriminate of loc * NotationPt.term
@@ -83,12 +84,18 @@ type nmacro =
  * marshalling *)
 let magic = 35
 
-type command =
-  | Include of loc * string 
-  | Set of loc * string * string
-  | Print of loc * string
+(* composed magic: term + command magics. No need to change this value *)
+let magic = magic + 10000 * NotationPt.magic
+
+type alias_spec =
+  | Ident_alias of string * string        (* identifier, uri *)
+  | Symbol_alias of string * int * string (* name, instance no, description *)
+  | Number_alias of int * string          (* instance no, description *)
+
+type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
 
-type ncommand =
+type command =
+  | Include of loc * inclusion_mode * string (* _,buri,_,path *)
   | UnificationHint of loc * NotationPt.term * int (* term, precedence *)
   | NObj of loc * NotationPt.term NotationPt.obj
   | NDiscriminator of loc * NotationPt.term
@@ -99,10 +106,19 @@ type ncommand =
       NotationPt.term * NotationPt.term *
       (string * NotationPt.term) * NotationPt.term
   | NQed of loc
+  (* ex lexicon commands *)
+  | Alias of loc * alias_spec
+      (** parameters, name, type, fields *) 
+  | Notation of loc * direction option * NotationPt.term * Gramext.g_assoc *
+      int * NotationPt.term
+      (* direction, l1 pattern, associativity, precedence, l2 pattern *)
+  | Interpretation of loc *
+      string * (string * NotationPt.argument_pattern list) *
+        NotationPt.cic_appl_pattern
+      (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
 type code =
-  | Command of loc * command
-  | NCommand of loc * ncommand
+  | NCommand of loc * command
   | NMacro of loc * nmacro 
   | NTactic of loc * ntactic list
              
@@ -113,3 +129,9 @@ type comment =
 type statement =
   | Executable of loc * code
   | Comment of loc * comment
+
+let description_of_alias =
+ function
+    Ident_alias (_,desc)
+  | Symbol_alias (_,_,desc)
+  | Number_alias (_,desc) -> desc