added Path.decode in ML, in correspondence to Path.encode in Scala;
authorwenzelm
Wed Jan 14 11:52:08 2015 +0100 (2015-01-14)
changeset 593634660b0409096
parent 59362 41f1645a4f63
child 59364 3b5da177ae6b
added Path.decode in ML, in correspondence to Path.encode in Scala;
src/Pure/General/path.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/General/path.ML	Tue Jan 13 21:46:09 2015 +0100
     1.2 +++ b/src/Pure/General/path.ML	Wed Jan 14 11:52:08 2015 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4    val make: string list -> T
     1.5    val implode: T -> string
     1.6    val explode: string -> T
     1.7 +  val decode: T XML.Decode.T
     1.8    val split: string -> T list
     1.9    val pretty: T -> Pretty.T
    1.10    val print: T -> string
    1.11 @@ -161,6 +162,8 @@
    1.12    space_explode ":" str
    1.13    |> map_filter (fn s => if s = "" then NONE else SOME (explode_path s));
    1.14  
    1.15 +val decode = XML.Decode.string #> explode_path;
    1.16 +
    1.17  
    1.18  (* print *)
    1.19  
     2.1 --- a/src/Pure/ROOT.ML	Tue Jan 13 21:46:09 2015 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Wed Jan 14 11:52:08 2015 +0100
     2.3 @@ -65,6 +65,7 @@
     2.4  use "General/linear_set.ML";
     2.5  use "General/buffer.ML";
     2.6  use "General/pretty.ML";
     2.7 +use "PIDE/xml.ML";
     2.8  use "General/path.ML";
     2.9  use "General/url.ML";
    2.10  use "General/file.ML";
    2.11 @@ -78,7 +79,6 @@
    2.12  if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
    2.13  use "General/sha1_samples.ML";
    2.14  
    2.15 -use "PIDE/xml.ML";
    2.16  use "PIDE/yxml.ML";
    2.17  use "PIDE/document_id.ML";
    2.18