1.1 --- a/src/Pure/General/markup.ML	Wed Jun 29 15:23:36 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Wed Jun 29 16:31:50 2011 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val position_properties': string list
     1.5    val position_properties: string list
     1.6    val positionN: string val position: T
     1.7 +  val pathN: string val path: string -> T
     1.8    val indentN: string
     1.9    val blockN: string val block: int -> T
    1.10    val widthN: string
    1.11 @@ -195,6 +196,11 @@
    1.12  val (positionN, position) = markup_elem "position";
    1.13  
    1.14  
    1.15 +(* path *)
    1.16 +
    1.17 +val (pathN, path) = markup_string "path" nameN;
    1.18 +
    1.19 +
    1.20  (* pretty printing *)
    1.21  
    1.22  val indentN = "indent";

     2.1 --- a/src/Pure/General/markup.scala	Wed Jun 29 15:23:36 2011 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Wed Jun 29 16:31:50 2011 +0200
     2.3 @@ -128,8 +128,21 @@
     2.4    val DEF_ID = "def_id"
     2.5  
     2.6    val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
     2.7 +  val POSITION = "position"
     2.8  
     2.9 -  val POSITION = "position"
    2.10 +
    2.11 +  /* path */
    2.12 +
    2.13 +  val PATH = "path"
    2.14 +
    2.15 +  object Path
    2.16 +  {
    2.17 +    def unapply(markup: Markup): Option[String] =
    2.18 +      markup match {
    2.19 +        case Markup(PATH, Name(name)) => Some(name)
    2.20 +        case _ => None
    2.21 +      }
    2.22 +  }
    2.23  
    2.24  
    2.25    /* pretty printing */

     3.1 --- a/src/Pure/General/path.ML	Wed Jun 29 15:23:36 2011 +0200
     3.2 +++ b/src/Pure/General/path.ML	Wed Jun 29 16:31:50 2011 +0200
     3.3 @@ -20,9 +20,10 @@
     3.4    val append: T -> T -> T
     3.5    val appends: T list -> T
     3.6    val make: string list -> T
     3.7 -  val print: T -> string
     3.8    val implode: T -> string
     3.9    val explode: string -> T
    3.10 +  val pretty: T -> Pretty.T
    3.11 +  val print: T -> string
    3.12    val dir: T -> T
    3.13    val base: T -> T
    3.14    val ext: string -> T -> T
    3.15 @@ -120,8 +121,6 @@
    3.16  
    3.17  end;
    3.18  
    3.19 -val print = quote o implode_path;
    3.20 -
    3.21  
    3.22  (* explode *)
    3.23  
    3.24 @@ -152,6 +151,15 @@
    3.25  end;
    3.26  
    3.27  
    3.28 +(* print *)
    3.29 +
    3.30 +fun pretty path =
    3.31 +  let val s = implode_path path
    3.32 +  in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
    3.33 +
    3.34 +val print = Pretty.str_of o pretty;
    3.35 +
    3.36 +
    3.37  (* base element *)
    3.38  
    3.39  fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)

     4.1 --- a/src/Pure/ROOT.ML	Wed Jun 29 15:23:36 2011 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Wed Jun 29 16:31:50 2011 +0200
     4.3 @@ -44,14 +44,14 @@
     4.4  use "General/balanced_tree.ML";
     4.5  use "General/graph.ML";
     4.6  use "General/linear_set.ML";
     4.7 +use "General/buffer.ML";
     4.8 +use "General/xml.ML";
     4.9 +use "General/xml_data.ML";
    4.10 +use "General/pretty.ML";
    4.11  use "General/path.ML";
    4.12  use "General/url.ML";
    4.13 -use "General/buffer.ML";
    4.14  use "General/file.ML";
    4.15 -use "General/xml.ML";
    4.16 -use "General/xml_data.ML";
    4.17  use "General/yxml.ML";
    4.18 -use "General/pretty.ML";
    4.19  use "General/long_name.ML";
    4.20  use "General/binding.ML";
    4.21  

     5.1 --- a/src/Pure/pure_setup.ML	Wed Jun 29 15:23:36 2011 +0200
     5.2 +++ b/src/Pure/pure_setup.ML	Wed Jun 29 16:31:50 2011 +0200
     5.3 @@ -31,7 +31,7 @@
     5.4  toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
     5.5  toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
     5.6  toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
     5.7 -toplevel_pp ["Path", "T"] "Pretty.str o Path.print";
     5.8 +toplevel_pp ["Path", "T"] "Path.pretty";
     5.9  toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
    5.10  toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
    5.11  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";