From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Jul 2005 10:38:32 +0000 (+0000)
Subject: "include" command implemented.
X-Git-Tag: PRE_GETTER_STORAGE~23
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b6101c89b49ad1df07df62ec661c8b30bda99a2a;p=helm.git

"include" command implemented.
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 25c15c575..760b34a42 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -635,14 +635,16 @@ EXTEND
             ind_types
         in
         TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
-    | [ IDENT "coercion" ] ; name = IDENT -> 
+    | IDENT "coercion" ; name = IDENT -> 
         TacticAst.Coercion (loc, CicAst.Ident (name,Some []))
-    | [ IDENT "coercion" ] ; name = URI -> 
+    | IDENT "coercion" ; name = URI -> 
         TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
-    | [ IDENT "alias"   ]; spec = alias_spec ->
+    | IDENT "alias" ; spec = alias_spec ->
         TacticAst.Alias (loc, spec)
-    | [ IDENT "record" ]; (params,name,ty,fields) = record_spec ->
+    | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields))
+    | IDENT "include" ; path = QSTRING ->
+        TacticAst.Include (loc,path)
   ]];
 
   executable: [
@@ -718,7 +720,8 @@ module EnvironmentP3 =
             s :: acc)
           env []
       in
-      String.concat "\n" (List.sort compare aliases)
+      String.concat "\n" (List.sort compare aliases) ^
+       (if aliases = [] then "" else "\n")
 
     EXTEND
       GLOBAL: aliases;
diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index c4f2a29ac..a051c2af6 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -126,6 +126,7 @@ type obj =
       (string * CicAst.term) list
 
 type ('term,'obj) command =
+  | Include of loc * string
   | Set of loc * string * string
   | Drop of loc
   | Qed of loc
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 86c7185ec..3a8b5213c 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -220,6 +220,7 @@ let pp_obj = function
 
 
 let pp_command = function
+  | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
   | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value