src/Pure/General/path.ML
changeset 48866 034df7b05759
parent 48658 4c7932270d6d
child 50201 c26369c9eda6
equal deleted inserted replaced
48865:9824fd676bf4 48866:034df7b05759
   188   | eval x = [x];
   188   | eval x = [x];
   189 
   189 
   190 val expand = rep #> maps eval #> norm #> Path;
   190 val expand = rep #> maps eval #> norm #> Path;
   191 
   191 
   192 
   192 
   193 (* source position -- with smart replacement ISABELLE_HOME *)
   193 (* source position -- with smart replacement of ISABELLE_HOME *)
   194 
   194 
   195 val isabelle_home = explode_path "~~";
   195 val isabelle_home = explode_path "~~";
   196 
   196 
   197 fun position path =
   197 fun position path =
   198   let
   198   let