smart_implode "$AFP" as well;
authorwenzelm
Tue Jun 26 23:15:48 2018 +0200 (13 months ago)
changeset 68519e1c24b628ca5
parent 68515 0854edc4d415
child 68520 9d78b02b5506
smart_implode "$AFP" as well;
src/Pure/General/path.ML
     1.1 --- a/src/Pure/General/path.ML	Tue Jun 26 19:29:14 2018 +0200
     1.2 +++ b/src/Pure/General/path.ML	Tue Jun 26 23:15:48 2018 +0200
     1.3 @@ -214,15 +214,16 @@
     1.4    let
     1.5      val full_name = implode_path (expand path);
     1.6      fun fold_path a =
     1.7 -      let val b = implode_path (expand (explode_path a)) in
     1.8 -        if full_name = b then SOME a
     1.9 -        else
    1.10 -          (case try (unprefix (b ^ "/")) full_name of
    1.11 -            SOME name => SOME (a ^ "/" ^ name)
    1.12 -          | NONE => NONE)
    1.13 -      end;
    1.14 +      (case try (implode_path o expand o explode_path) a of
    1.15 +        SOME b =>
    1.16 +          if full_name = b then SOME a
    1.17 +          else
    1.18 +            (case try (unprefix (b ^ "/")) full_name of
    1.19 +              SOME name => SOME (a ^ "/" ^ name)
    1.20 +            | NONE => NONE)
    1.21 +      | NONE => NONE);
    1.22    in
    1.23 -    (case get_first fold_path ["~~", "$ISABELLE_HOME_USER", "~"] of
    1.24 +    (case get_first fold_path ["$AFP", "~~", "$ISABELLE_HOME_USER", "~"] of
    1.25        SOME name => name
    1.26      | NONE => implode_path path)
    1.27    end;