- we implemented the hierarchy and sort names declaration in text parser

[helm.git] / helm / software / lambda-delta / text / txt.ml

diff --git a/helm/software/lambda-delta/text/txt.ml b/helm/software/lambda-delta/text/txt.ml
index f874a273e6b40b4dfec6f246320d889ad899ebfa..264b76873f7f835edfafde747514bc10fcb346c1 100644 (file)
--- a/helm/software/lambda-delta/text/txt.ml
+++ b/helm/software/lambda-delta/text/txt.ml
@@ -13,7 +13,12 @@ type ix = int (* index *)
 
 type id = string (* identifier *)
 
-type comm = string (* comment *)
+type desc = string (* description *)
+
+type kind = Decl (* generic declaration *) 
+          | Ax   (* axiom               *)
+         | Def  (* generic definition  *)
+         | Th   (* theorem             *)
 
 type bind = Abst of (id * term) list (* name, domain *)
           | Abbr of (id * term) list (* name, bodies *)
@@ -27,5 +32,7 @@ and term = Sort of ix               (* level               *)
         | Appl of term list * term (* arguments, function *)
         | Bind of bind * term      (* binder, scope       *)
 
-type entity = Section of id option              (* section: Some id = open, None = close last *)
-           | Global of bool * id * comm * term (* global entity: false = decl, true = def    *) 
+type command = Graph of id                       (* hierarchy graph: name *) 
+             | Sorts of (int option * id) list   (* sorts: index, name *)
+            | Section of id option              (* section: Some id = open, None = close last *)
+            | Entity of kind * id * desc * term (* entity: class, name, description, contents *)