src/Pure/library.ML
changeset 3832 17a20a2af8f5
parent 3762 f20b071a429a
child 3874 552ce5ad6a2e
     1.1 --- a/src/Pure/library.ML	Fri Oct 10 15:48:43 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Oct 10 15:50:46 1997 +0200
     1.3 @@ -432,8 +432,8 @@
     1.4  (*concatenate messages, one per line, into a string*)
     1.5  val cat_lines = space_implode "\n";
     1.6  
     1.7 -(*space_explode "." "h.e..l.lo"; gives ["h", "e", "l", "lo"]*)
     1.8 -fun space_explode sep s =
     1.9 +(*BAD_space_explode "." "h.e..l.lo"; gives ["h", "e", "l", "lo"]*)
    1.10 +fun BAD_space_explode sep s =
    1.11    let fun divide [] "" = []
    1.12          | divide [] part = [part]
    1.13          | divide (c::s) part =
    1.14 @@ -442,6 +442,19 @@
    1.15              else divide s (part ^ c)
    1.16    in divide (explode s) "" end;
    1.17  
    1.18 +(*space_explode "." "h.e..l.lo"; gives ["h", "e", "", "l", "lo"]*)
    1.19 +fun space_explode _ "" = []
    1.20 +  | space_explode sep str =
    1.21 +      let
    1.22 +        fun expl chs =
    1.23 +          (case take_prefix (not_equal sep) chs of
    1.24 +            (cs, []) => [implode cs]
    1.25 +          | (cs, _ :: cs') => implode cs :: expl cs');
    1.26 +      in expl (explode str) end;
    1.27 +
    1.28 +val split_lines = space_explode "\n";
    1.29 +
    1.30 +
    1.31  
    1.32  (** lists as sets **)
    1.33  
    1.34 @@ -739,13 +752,8 @@
    1.35    fun out s =
    1.36      (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    1.37  
    1.38 -  fun lines cs =
    1.39 -    (case take_prefix (not_equal "\n") cs of
    1.40 -      (cs', []) => [implode cs']
    1.41 -    | (cs', _ :: cs'') => implode cs' :: lines cs'');
    1.42 -
    1.43    fun prefix_lines prfx txt =
    1.44 -    txt |> explode |> lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
    1.45 +    txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
    1.46  in
    1.47  
    1.48  (*hooks for output channels: normal, warning, error*)
    1.49 @@ -897,15 +905,15 @@
    1.50          dest_path = "" orelse hd (explode dest_path) <> "/" then
    1.51         error "Relative or empty path passed to relative_path"
    1.52       else ();
    1.53 -     space_implode "/" (mk_relative (space_explode "/" cur_path)
    1.54 -                                    (space_explode "/" dest_path))
    1.55 +     space_implode "/" (mk_relative (BAD_space_explode "/" cur_path)
    1.56 +                                    (BAD_space_explode "/" dest_path))
    1.57    end;
    1.58  
    1.59  (*Determine if absolute path1 is a subdirectory of absolute path2*)
    1.60  fun path1 subdir_of path2 =
    1.61    if hd (explode path1) <> "/" orelse hd (explode path2) <> "/" then
    1.62      error "Relative or empty path passed to subdir_of"
    1.63 -  else (space_explode "/" path2) prefix (space_explode "/" path1);
    1.64 +  else (BAD_space_explode "/" path2) prefix (BAD_space_explode "/" path1);
    1.65  
    1.66  fun absolute_path cwd file =
    1.67    let fun rm_points [] result = rev result
    1.68 @@ -915,7 +923,7 @@
    1.69    in if file = "" then ""
    1.70       else if hd (explode file) = "/" then file
    1.71       else "/" ^ space_implode "/"
    1.72 -                  (rm_points (space_explode "/" (tack_on cwd file)) [])
    1.73 +                  (rm_points (BAD_space_explode "/" (tack_on cwd file)) [])
    1.74    end;
    1.75  
    1.76  fun file_exists file = (file_info file <> "");