diff options
| author | Emilio Jesus Gallego Arias | 2020-02-20 13:06:22 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-03 23:40:09 -0500 |
| commit | 15ed46fffc962159ca6158aa791b5258fd42ab3c (patch) | |
| tree | 4ac202c9f45848cd812a0a28bd895f85e5e69f80 | |
| parent | 8de81cf2b6059e1e5aa84ea483dba38e42b35792 (diff) | |
[vernac] Use a record for VernacAddLoadPath
| -rw-r--r-- | vernac/g_vernac.mlg | 9 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 6 |
4 files changed, 16 insertions, 11 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index df85e004ed..37b584f8d9 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -912,10 +912,11 @@ GRAMMAR EXTEND Gram | IDENT "Locate"; l = locatable -> { VernacLocate l } (* Managing load paths *) - | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; "as"; logical_path = dirpath -> - { VernacAddLoadPath (false, dir, logical_path) } - | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; "as"; logical_path = dirpath -> - { VernacAddLoadPath (true, dir, logical_path) } + | IDENT "Add"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath -> + { VernacAddLoadPath { implicit = false; logical_path; physical_path } } + | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath -> + { VernacAddLoadPath { implicit = true; logical_path; physical_path } } + | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> { VernacRemoveLoadPath dir } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f58e9e7131..33d9e3d98a 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1016,13 +1016,13 @@ let string_of_definition_object_kind = let open Decls in function return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) (* Auxiliary file and library management *) - | VernacAddLoadPath (fl,s,dir) -> + | VernacAddLoadPath { implicit; physical_path; logical_path } -> return ( hov 2 (keyword "Add" ++ - (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ - keyword "LoadPath" ++ spc() ++ qs s ++ - spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) + (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++ + keyword "LoadPath" ++ spc() ++ qs physical_path ++ + spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path)) | VernacRemoveLoadPath s -> return (keyword "Remove LoadPath" ++ qs s) | VernacAddMLPath (s) -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e5cbb42fa6..3cf4b4a89d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2103,10 +2103,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with unsupported_attributes atts; vernac_solve_existential ~pstate n c) (* Auxiliary file and library management *) - | VernacAddLoadPath (implicit,s,coq_path) -> + | VernacAddLoadPath { implicit; physical_path; logical_path } -> VtDefault(fun () -> unsupported_attributes atts; - vernac_add_loadpath ~implicit s coq_path) + vernac_add_loadpath ~implicit physical_path logical_path) | VernacRemoveLoadPath s -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 7feb05fe34..22aaab2a68 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -362,7 +362,11 @@ type nonrec vernac_expr = | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) - | VernacAddLoadPath of bool * string * DirPath.t + | VernacAddLoadPath of { implicit : bool + ; physical_path : CUnix.physical_path + ; logical_path : DirPath.t + } + | VernacRemoveLoadPath of string | VernacAddMLPath of string | VernacDeclareMLModule of string list |