# HG changeset patch
# User wenzelm
# Date 1309357910 -7200
# Node ID 11140987d4152282ef877a267316e8423d396d54
# Parent  e67d104c0c5085c87655c9cb90cc550564c585f7
print Path.T with some markup;

diff -r e67d104c0c50 -r 11140987d415 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Jun 29 15:23:36 2011 +0200
+++ b/src/Pure/General/markup.ML	Wed Jun 29 16:31:50 2011 +0200
@@ -29,6 +29,7 @@
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
+  val pathN: string val path: string -> T
   val indentN: string
   val blockN: string val block: int -> T
   val widthN: string
@@ -195,6 +196,11 @@
 val (positionN, position) = markup_elem "position";
 
 
+(* path *)
+
+val (pathN, path) = markup_string "path" nameN;
+
+
 (* pretty printing *)
 
 val indentN = "indent";
diff -r e67d104c0c50 -r 11140987d415 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Jun 29 15:23:36 2011 +0200
+++ b/src/Pure/General/markup.scala	Wed Jun 29 16:31:50 2011 +0200
@@ -128,8 +128,21 @@
   val DEF_ID = "def_id"
 
   val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
+  val POSITION = "position"
 
-  val POSITION = "position"
+
+  /* path */
+
+  val PATH = "path"
+
+  object Path
+  {
+    def unapply(markup: Markup): Option[String] =
+      markup match {
+        case Markup(PATH, Name(name)) => Some(name)
+        case _ => None
+      }
+  }
 
 
   /* pretty printing */
diff -r e67d104c0c50 -r 11140987d415 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Jun 29 15:23:36 2011 +0200
+++ b/src/Pure/General/path.ML	Wed Jun 29 16:31:50 2011 +0200
@@ -20,9 +20,10 @@
   val append: T -> T -> T
   val appends: T list -> T
   val make: string list -> T
-  val print: T -> string
   val implode: T -> string
   val explode: string -> T
+  val pretty: T -> Pretty.T
+  val print: T -> string
   val dir: T -> T
   val base: T -> T
   val ext: string -> T -> T
@@ -120,8 +121,6 @@
 
 end;
 
-val print = quote o implode_path;
-
 
 (* explode *)
 
@@ -152,6 +151,15 @@
 end;
 
 
+(* print *)
+
+fun pretty path =
+  let val s = implode_path path
+  in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
+
+val print = Pretty.str_of o pretty;
+
+
 (* base element *)
 
 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
diff -r e67d104c0c50 -r 11140987d415 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jun 29 15:23:36 2011 +0200
+++ b/src/Pure/ROOT.ML	Wed Jun 29 16:31:50 2011 +0200
@@ -44,14 +44,14 @@
 use "General/balanced_tree.ML";
 use "General/graph.ML";
 use "General/linear_set.ML";
+use "General/buffer.ML";
+use "General/xml.ML";
+use "General/xml_data.ML";
+use "General/pretty.ML";
 use "General/path.ML";
 use "General/url.ML";
-use "General/buffer.ML";
 use "General/file.ML";
-use "General/xml.ML";
-use "General/xml_data.ML";
 use "General/yxml.ML";
-use "General/pretty.ML";
 use "General/long_name.ML";
 use "General/binding.ML";
 
diff -r e67d104c0c50 -r 11140987d415 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Wed Jun 29 15:23:36 2011 +0200
+++ b/src/Pure/pure_setup.ML	Wed Jun 29 16:31:50 2011 +0200
@@ -31,7 +31,7 @@
 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
 toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
-toplevel_pp ["Path", "T"] "Pretty.str o Path.print";
+toplevel_pp ["Path", "T"] "Path.pretty";
 toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";