From 95fdf37ed38d64c6358fcf8f5b841a56157db0b8 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 23 Nov 2000 14:07:46 +0000 Subject: Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@929 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/names.ml | 10 +++++----- kernel/names.mli | 6 +++--- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'kernel') diff --git a/kernel/names.ml b/kernel/names.ml index 76f17525d..c8eb17ca9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -55,7 +55,7 @@ let id_of_string s = let atompart_of_id id = id.atom let index_of_id id = snd (repr_ident id) -let print_id id = +let pr_id id = match repr_ident id with | ("",None) -> [< 'sTR"[]" >] | ("",Some n) -> [< 'sTR"[" ; 'iNT n ; 'sTR"]" >] @@ -134,7 +134,7 @@ let make_qualid p s = (p,s) let repr_qualid q = q let string_of_qualid (l,s) = String.concat "." (l@[s]) -let print_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s]) +let pr_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s]) (*s Section paths *) @@ -158,8 +158,8 @@ let string_of_dirpath sl = String.concat "#" (""::sl) let string_of_path sp = let (sl,id,k) = repr_path sp in String.concat "" - ((List.flatten (List.map (fun s -> ["#";s]) sl)) - @ [ "#"; string_of_id id; "."; string_of_kind k ]) + ("#"::(List.flatten (List.map (fun s -> [s;"."]) sl)) + @ [ string_of_id id ]) let path_of_string s = try @@ -168,7 +168,7 @@ let path_of_string s = with | Invalid_argument _ -> invalid_arg "path_of_string" -let print_sp sp = [< 'sTR (string_of_path sp) >] +let pr_sp sp = [< 'sTR (string_of_path sp) >] let sp_of_wd = function | [] -> invalid_arg "Names.sp_of_wd" diff --git a/kernel/names.mli b/kernel/names.mli index 3a380a42d..070e7917f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -23,7 +23,7 @@ val index_of_id : identifier -> int option (* Parsing and printing of identifiers *) val string_of_id : identifier -> string val id_of_string : string -> identifier -val print_id : identifier -> std_ppcmds +val pr_id : identifier -> std_ppcmds (* Identifiers sets and maps *) module Idset : Set.S with type elt = identifier @@ -58,7 +58,7 @@ val make_qualid : string list -> string -> qualid val repr_qualid : qualid -> string list * string val string_of_qualid : qualid -> string -val print_qualid : qualid -> std_ppcmds +val pr_qualid : qualid -> std_ppcmds (*s Section paths *) type section_path @@ -78,7 +78,7 @@ val wd_of_sp : section_path -> string list (* Parsing and printing of section path as ["#module#id#kind"] *) val path_of_string : string -> section_path val string_of_path : section_path -> string -val print_sp : section_path -> std_ppcmds +val pr_sp : section_path -> std_ppcmds (*i val string_of_path_mind : section_path -> identifier -> string -- cgit v1.2.3