diff options
Diffstat (limited to 'toplevel/mltop.ml4')
| -rw-r--r-- | toplevel/mltop.ml4 | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 3fc937724..d9325a2e7 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -89,7 +89,7 @@ let ocaml_toploop () = | _ -> () (* errorlabstrm "Mltop.ocaml_toploop" - [< 'sTR"Cannot access the ML toplevel" >] + [< str"Cannot access the ML toplevel" >] *) (* Dynamic loading of .cmo *) @@ -101,11 +101,11 @@ let dir_ml_load s = with | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u | _ -> errorlabstrm "Mltop.load_object" - [< 'sTR"Cannot link ml-object "; 'sTR s; - 'sTR" to Coq code." >] + [< str"Cannot link ml-object "; str s; + str" to Coq code." >] else errorlabstrm "Mltop.load_object" - [< 'sTR"File not found on loadpath : "; 'sTR s >] + [< str"File not found on loadpath : "; str s >] | WithoutTop -> ifdef Byte then (if is_in_path !coq_mlpath_copy s then @@ -119,14 +119,14 @@ let dir_ml_load s = with | Dynlink.Error(a) -> errorlabstrm "Mltop.load_object" - [< 'sTR (Dynlink.error_message a) >] + [< str (Dynlink.error_message a) >] else errorlabstrm "Mltop.load_object" - [< 'sTR"File not found on loadpath : "; 'sTR s >]) + [< str"File not found on loadpath : "; str s >]) else () | Native -> errorlabstrm "Mltop.no_load_object" - [< 'sTR"Loading of ML object file forbidden in a native Coq" >] + [< str"Loading of ML object file forbidden in a native Coq" >] (* Dynamic interpretation of .ml *) let dir_ml_use s = @@ -147,14 +147,14 @@ let add_rec_ml_dir dir = (* Adding files to Coq and ML loadpath *) -let add_path dir coq_dirpath = +let add_path ~unix_path:dir ~coq_root:coq_dirpath = if exists_dir dir then begin add_ml_dir dir; Library.add_load_path_entry (dir,coq_dirpath) end else - wARNING [< 'sTR ("Cannot open " ^ dir) >] + msg_warning [< str ("Cannot open " ^ dir) >] let convert_string d = try Names.id_of_string d @@ -164,7 +164,7 @@ let convert_string d = flush_all (); failwith "caught" -let add_rec_path dir coq_dirpath = +let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = let dirs = all_subdirs dir in let prefix = Names.repr_dirpath coq_dirpath in if dirs <> [] then @@ -177,7 +177,7 @@ let add_rec_path dir coq_dirpath = List.iter Library.add_load_path_entry dirs end else - wARNING [< 'sTR ("Cannot open " ^ dir) >] + msg_warning [< str ("Cannot open " ^ dir) >] (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = @@ -244,7 +244,7 @@ let unfreeze_ml_modules x = load_object mname fname else errorlabstrm "Mltop.unfreeze_ml_modules" - [< 'sTR"Loading of ML object file forbidden in a native Coq" >]; + [< str"Loading of ML object file forbidden in a native Coq" >]; add_loaded_module mname) x @@ -266,11 +266,11 @@ let cache_ml_module_object (_,{mnames=mnames}) = begin try if_verbose - mSG [< 'sTR"[Loading ML file "; 'sTR fname; 'sTR" ..." >]; + msg [< str"[Loading ML file "; str fname; str" ..." >]; load_object mname fname; - if_verbose mSGNL [< 'sTR"done]" >] + if_verbose msgnl [< str"done]" >] with e -> - if_verbose mSGNL [< 'sTR"failed]" >]; + if_verbose msgnl [< str"failed]" >]; raise e end; add_loaded_module mname) @@ -290,11 +290,11 @@ let declare_ml_modules l = let print_ml_path () = let l = !coq_mlpath_copy in - pPNL [< 'sTR"ML Load Path:"; 'fNL; 'sTR" "; - hV 0 (prlist_with_sep pr_fnl pr_str l) >] + ppnl [< str"ML Load Path:"; fnl (); str" "; + hv 0 (prlist_with_sep pr_fnl pr_str l) >] (* Printing of loaded ML modules *) let print_ml_modules () = let l = get_loaded_modules () in - pP [< 'sTR"Loaded ML Modules: " ; pr_vertical_list pr_str l >] + pp [< str"Loaded ML Modules: " ; pr_vertical_list pr_str l >] |