src/Pure/General/file.ML
changeset 16002 e0557c452138
parent 15570 8d8c70b41bab
child 16261 28803c418b59
equal deleted inserted replaced
16001:554836ed1f1b 16002:e0557c452138
    94     (case file_info name of
    94     (case file_info name of
    95       "" => NONE
    95       "" => NONE
    96     | s => SOME (Info s))
    96     | s => SOME (Info s))
    97   end;
    97   end;
    98 
    98 
    99 val exists = isSome o info;
    99 val exists = is_some o info;
   100 
   100 
   101 
   101 
   102 (* directories *)
   102 (* directories *)
   103 
   103 
   104 fun system_command cmd =
   104 fun system_command cmd =