src/Pure/General/path.ML
changeset 69784 24bbc4e30e5b
parent 69670 114ae60c4be7
child 70013 6de8b7a5cd44
     1.1 --- a/src/Pure/General/path.ML	Sat Feb 02 14:51:11 2019 +0100
     1.2 +++ b/src/Pure/General/path.ML	Sat Feb 02 15:52:14 2019 +0100
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature PATH =
     1.6  sig
     1.7 -  val check_elem: string -> unit
     1.8    eqtype T
     1.9    val is_current: T -> bool
    1.10    val current: T
    1.11 @@ -20,6 +19,7 @@
    1.12    val has_parent: T -> bool
    1.13    val is_absolute: T -> bool
    1.14    val is_basic: T -> bool
    1.15 +  val all_basic: T -> bool
    1.16    val starts_basic: T -> bool
    1.17    val append: T -> T -> T
    1.18    val appends: T list -> T
    1.19 @@ -57,8 +57,6 @@
    1.20  val illegal_elem = ["", "~", "~~", ".", ".."];
    1.21  val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
    1.22  
    1.23 -in
    1.24 -
    1.25  fun check_elem s =
    1.26    if member (op =) illegal_elem s then err_elem "Illegal" s
    1.27    else
    1.28 @@ -69,6 +67,8 @@
    1.29          err_elem ("Illegal character " ^ quote c ^ " in") s
    1.30        else ());
    1.31  
    1.32 +in
    1.33 +
    1.34  val root_elem = Root o tap check_elem;
    1.35  val basic_elem = Basic o tap check_elem;
    1.36  val variable_elem = Variable o tap check_elem;
    1.37 @@ -103,6 +103,9 @@
    1.38  fun is_basic (Path [Basic _]) = true
    1.39    | is_basic _ = false;
    1.40  
    1.41 +fun all_basic (Path elems) =
    1.42 +  forall (fn Basic _ => true | _ => false) elems;
    1.43 +
    1.44  fun starts_basic (Path xs) =
    1.45    (case try List.last xs of
    1.46      SOME (Basic _) => true