src/Pure/General/path.ML
changeset 61877 276ad4354069
parent 59363 4660b0409096
child 62663 bea354f6ff21
equal deleted inserted replaced
61876:669f47397249 61877:276ad4354069
   169 
   169 
   170 fun pretty path =
   170 fun pretty path =
   171   let val s = implode_path path
   171   let val s = implode_path path
   172   in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
   172   in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
   173 
   173 
   174 val print = Pretty.str_of o pretty;
   174 val print = Pretty.unformatted_string_of o pretty;
   175 
   175 
   176 
   176 
   177 (* base element *)
   177 (* base element *)
   178 
   178 
   179 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
   179 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)