Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set Implicit Arguments' and co

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1122 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 43 insertions, 7 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index e1c2191057..ec7c84b47b 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -91,16 +91,29 @@ GEXTEND Gram
       | IDENT "Locate"; id = qualidarg; "." ->
 	  <:ast< (Locate $id) >>
 
-       (* For compatibility (now turned into a table) *)
-      | IDENT "AddPath"; dir = stringarg; IDENT "As"; alias = qualidarg; "." ->
+      (* Managing load paths *)
+      | IDENT "Add"; IDENT "LoadPath"; dir = stringarg; 
+	"as"; alias = qualidarg; "." -> <:ast< (ADDPATH $dir $alias) >>
+      | IDENT "Add"; IDENT "LoadPath"; dir = stringarg; "." ->
+	  <:ast< (ADDPATH $dir) >>
+      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = stringarg;
+	"as"; alias=qualidarg; "." -> <:ast< (RECADDPATH $dir $alias) >>
+      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = stringarg; "." ->
+         <:ast< (RECADDPATH $dir) >>
+      | IDENT "Remove"; IDENT "LoadPath"; dir = stringarg; "." ->
+	  <:ast< (DELPATH $dir) >>
+      | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
+
+       (* For compatibility *)
+      | IDENT "AddPath"; dir = stringarg; "as"; alias = qualidarg; "." ->
          <:ast< (ADDPATH $dir $alias) >>
       | IDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >>
-      | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >>
-      | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
-      | IDENT "AddRecPath"; dir = stringarg;IDENT "As"; alias=qualidarg; "." ->
+      | IDENT "AddRecPath"; dir = stringarg; "as"; alias=qualidarg; "." ->
          <:ast< (RECADDPATH $dir $alias) >>
       | IDENT "AddRecPath"; dir = stringarg; "." ->
          <:ast< (RECADDPATH $dir) >>
+      | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >>
+
       | IDENT "Print"; IDENT "Modules"; "." -> <:ast< (PrintModules) >>
       | IDENT "Print"; "Proof"; id = identarg; "." ->
           <:ast< (PrintOpaqueId $id) >>
@@ -147,6 +160,14 @@ GEXTEND Gram
       | IDENT "Unset"; IDENT "Hyps_limit"; "." ->
           <:ast< (UNSETHYPSLIMIT) >>
 
+      (* Standardized syntax for Implicit Arguments *)
+      | "Set"; IDENT "Implicit"; IDENT "Arguments"; "." ->
+          <:ast< (IMPLICIT_ARGS_ON) >>
+      | IDENT "Unset"; IDENT "Implicit"; IDENT "Arguments"; "." ->
+          <:ast< (IMPLICIT_ARGS_OFF) >>
+      | IDENT "Test"; IDENT "Implicit"; IDENT "Arguments"; "." ->
+          <:ast< (TEST_IMPLICIT_ARGS) >>
+
       (* Pour intervenir sur les tables de paramètres *)
       | "Set"; table = identarg; field = identarg;
                       value = option_value; "." ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c194917721..012dc2ca3a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -126,10 +126,14 @@ let locate_qualid qid =
   with Not_found ->
     error ((string_of_qualid qid) ^ " not a defined object")
 
+let print_path_entry s =
+  [< 'sTR s.directory; 'tBRK (0,2); 'sTR (string_of_dirpath s.coq_dirpath) >]
+
 let print_loadpath () =
   let l = get_load_path () in
-  mSGNL [< 'sTR"Load Path:"; 'fNL; 'sTR"  ";
-           hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s.directory >]) l) >]
+  mSGNL (Pp.t [< 'sTR "Physical path:                                 ";
+		 'tAB; 'sTR "Logical Path:"; 'fNL; 
+		 prlist_with_sep pr_fnl print_path_entry l >])
 
 let get_current_context_of_args = function
   | [VARG_NUMBER n] -> get_goal_context n
@@ -453,6 +457,17 @@ let _ =
        | [] -> (fun () -> Impargs.make_implicit_args false)
        | _  -> bad_vernac_args "IMPLICIT_ARGS_OFF")
 
+let _ =
+  add "TEST_IMPLICIT_ARGS"
+    (function 
+       | [] ->
+	   (fun () ->
+	      if Impargs.is_implicit_args () then
+		message "Implicit arguments mode is set"
+	      else 
+		message "Implicit arguments mode is unset")
+       | _  -> bad_vernac_args "IMPLICIT_ARGS_OFF")
+
 let number_list = 
   List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list")