# 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 \"\")"; toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";