1.1 --- a/src/Pure/General/path.ML	Wed Jun 29 15:23:36 2011 +0200
     1.2 +++ b/src/Pure/General/path.ML	Wed Jun 29 16:31:50 2011 +0200
     1.3 @@ -20,9 +20,10 @@
     1.4    val append: T -> T -> T
     1.5    val appends: T list -> T
     1.6    val make: string list -> T
     1.7 -  val print: T -> string
     1.8    val implode: T -> string
     1.9    val explode: string -> T
    1.10 +  val pretty: T -> Pretty.T
    1.11 +  val print: T -> string
    1.12    val dir: T -> T
    1.13    val base: T -> T
    1.14    val ext: string -> T -> T
    1.15 @@ -120,8 +121,6 @@
    1.16  
    1.17  end;
    1.18  
    1.19 -val print = quote o implode_path;
    1.20 -
    1.21  
    1.22  (* explode *)
    1.23  
    1.24 @@ -152,6 +151,15 @@
    1.25  end;
    1.26  
    1.27  
    1.28 +(* print *)
    1.29 +
    1.30 +fun pretty path =
    1.31 +  let val s = implode_path path
    1.32 +  in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
    1.33 +
    1.34 +val print = Pretty.str_of o pretty;
    1.35 +
    1.36 +
    1.37  (* base element *)
    1.38  
    1.39  fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)