/[eiffelstudio]/FreeELKS/trunk/library/kernel/file.e
ViewVC logotype

Contents of /FreeELKS/trunk/library/kernel/file.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 91424 - (show annotations)
Tue Oct 26 18:39:32 2004 UTC (15 years, 3 months ago) by manus_eiffel
File size: 41861 byte(s)
Initial revision

1 indexing
2
3 description:
4 "Sequential files, viewed as persistent sequences of characters"
5
6 status: "See notice at end of class"
7 date: "$Date$"
8 revision: "$Revision$"
9
10 deferred class FILE inherit
11
12 UNBOUNDED [CHARACTER]
13
14 SEQUENCE [CHARACTER]
15 undefine
16 prune
17 redefine
18 off, append
19 end
20
21 IO_MEDIUM
22 rename
23 handle as descriptor,
24 handle_available as descriptor_available
25 end
26
27 feature -- Initialization
28
29 make (fn: STRING) is
30 -- Create file object with `fn' as file name.
31 require
32 string_exists: fn /= Void
33 string_not_empty: not fn.is_empty
34 do
35 name := fn
36 mode := Closed_file
37 ensure
38 file_named: name = fn
39 file_closed: is_closed
40 end
41
42 make_open_read (fn: STRING) is
43 -- Create file object with `fn' as file name
44 -- and open file in read mode.
45 require
46 string_exists: fn /= Void
47 string_not_empty: not fn.is_empty
48 do
49 make (fn)
50 open_read
51 ensure
52 file_named: name = fn
53 exists: exists
54 open_read: is_open_read
55 end
56
57 make_open_write (fn: STRING) is
58 -- Create file object with `fn' as file name
59 -- and open file for writing;
60 -- create it if it does not exist.
61 require
62 string_exists: fn /= Void
63 string_not_empty: not fn.is_empty
64 do
65 make (fn)
66 open_write
67 ensure
68 file_named: name = fn
69 exists: exists
70 open_write: is_open_write
71 end
72
73 make_open_append (fn: STRING) is
74 -- Create file object with `fn' as file name
75 -- and open file in append-only mode.
76 require
77 string_exists: fn /= Void
78 string_not_empty: not fn.is_empty
79 do
80 make (fn)
81 open_append
82 ensure
83 file_named: name = fn
84 exists: exists
85 open_append: is_open_append
86 end
87
88 make_open_read_write (fn: STRING) is
89 -- Create file object with `fn' as file name
90 -- and open file for both reading and writing.
91 require
92 string_exists: fn /= Void
93 string_not_empty: not fn.is_empty
94 do
95 make (fn)
96 open_read_write
97 ensure
98 file_named: name = fn
99 exists: exists
100 open_read: is_open_read
101 open_write: is_open_write
102 end
103
104 make_create_read_write (fn: STRING) is
105 -- Create file object with `fn' as file name
106 -- and open file for both reading and writing;
107 -- create it if it does not exist.
108 require
109 string_exists: fn /= Void
110 string_not_empty: not fn.is_empty
111 do
112 make (fn)
113 create_read_write
114 ensure
115 file_named: name = fn
116 exists: exists
117 open_read: is_open_read
118 open_write: is_open_write
119 end
120
121 make_open_read_append (fn: STRING) is
122 -- Create file object with `fn' as file name
123 -- and open file for reading anywhere
124 -- but writing at the end only.
125 -- Create file if it does not exist.
126 require
127 string_exists: fn /= Void
128 string_not_empty: not fn.is_empty
129 do
130 make (fn)
131 open_read_append
132 ensure
133 file_named: name = fn
134 exists: exists
135 open_read: is_open_read
136 open_append: is_open_append
137 end
138
139 feature -- Access
140
141 name: STRING
142 -- File name
143
144 item: CHARACTER is
145 -- Current item
146 do
147 read_character
148 Result := last_character
149 back
150 end
151
152 position: INTEGER is
153 -- Current cursor position.
154 do
155 if not is_closed then
156 Result := file_tell (file_pointer)
157 end
158 end
159
160 descriptor: INTEGER is
161 -- File descriptor as used by the operating system.
162 require else
163 file_opened: not is_closed
164 do
165 Result := file_fd (file_pointer)
166 descriptor_available := True
167 end
168
169 descriptor_available: BOOLEAN
170
171 separator: CHARACTER
172 -- ASCII code of character following last word read
173
174 file_pointer: POINTER
175 -- File pointer as required in C
176
177 file_info: UNIX_FILE_INFO is
178 -- Collected information about the file.
179 do
180 set_buffer
181 Result := buffered_file_info.twin
182 end
183
184 inode: INTEGER is
185 -- I-node number
186 require
187 file_exists: exists
188 do
189 set_buffer
190 Result := buffered_file_info.inode
191 end
192
193 links: INTEGER is
194 -- Number of links on file
195 require
196 file_exists: exists
197 do
198 set_buffer
199 Result := buffered_file_info.links
200 end
201
202 user_id: INTEGER is
203 -- User identification of owner
204 require
205 file_exists: exists
206 do
207 set_buffer
208 Result := buffered_file_info.user_id
209 end
210
211 group_id: INTEGER is
212 -- Group identification of owner
213 require
214 file_exists: exists
215 do
216 set_buffer
217 Result := buffered_file_info.group_id
218 end
219
220 protection: INTEGER is
221 -- Protection mode, in decimal value
222 require
223 file_exists: exists
224 do
225 set_buffer
226 Result := buffered_file_info.protection
227 end
228
229 owner_name: STRING is
230 -- Name of owner
231 require
232 file_exists: exists
233 do
234 set_buffer
235 Result := buffered_file_info.owner_name
236 end
237
238 date: INTEGER is
239 -- Time stamp (time of last modification)
240 require
241 file_exists: exists
242 do
243 set_buffer
244 Result := buffered_file_info.date
245 end
246
247 access_date: INTEGER is
248 -- Time stamp of last access made to the inode.
249 require
250 file_exists: exists
251 do
252 set_buffer
253 Result := buffered_file_info.access_date
254 end
255
256 retrieved: ANY is
257 -- Retrieved object structure
258 -- To access resulting object under correct type,
259 -- use assignment attempt.
260 -- Will raise an exception (code `Retrieve_exception')
261 -- if content is not a stored Eiffel structure.
262 do
263 (create {MISMATCH_CORRECTOR}).mismatch_information.do_nothing
264 Result := c_retrieved (descriptor)
265 end
266
267 feature -- Measurement
268
269 count: INTEGER is
270 -- Size in bytes (0 if no associated physical file)
271 do
272 if exists then
273 if not is_open_write then
274 set_buffer
275 Result := buffered_file_info.size
276 else
277 Result := file_size (file_pointer)
278 end
279 end
280 end
281
282 feature -- Status report
283
284 after: BOOLEAN is
285 -- Is there no valid cursor position to the right of cursor position?
286 do
287 Result := not is_closed and then (end_of_file or count = 0)
288 end
289
290 before: BOOLEAN is
291 -- Is there no valid cursor position to the left of cursor position?
292 do
293 Result := is_closed
294 end
295
296 off: BOOLEAN is
297 -- Is there no item?
298 do
299 Result := (count = 0) or else is_closed or else end_of_file
300 end
301
302 end_of_file: BOOLEAN is
303 -- Has an EOF been detected?
304 require
305 opened: not is_closed
306 do
307 Result := file_feof (file_pointer)
308 end
309
310 exists: BOOLEAN is
311 -- Does physical file exist?
312 -- (Uses effective UID.)
313 local
314 external_name: ANY
315 do
316 external_name := name.to_c
317 Result := file_exists ($external_name)
318 ensure then
319 unchanged_mode: mode = old mode
320 end
321
322 access_exists: BOOLEAN is
323 -- Does physical file exist?
324 -- (Uses real UID.)
325 local
326 external_name: ANY
327 do
328 external_name := name.to_c
329 Result := file_access ($external_name, 0)
330 end
331
332 path_exists: BOOLEAN is
333 -- Does physical file `name' exist without resolving
334 -- symbolic links?
335 local
336 external_name: ANY
337 do
338 external_name := name.to_c
339 Result := file_path_exists ($external_name)
340 ensure then
341 unchanged_mode: mode = old mode
342 end
343
344 is_readable: BOOLEAN is
345 -- Is file readable?
346 -- (Checks permission for effective UID.)
347 do
348 set_buffer
349 Result := buffered_file_info.is_readable
350 end
351
352 is_writable: BOOLEAN is
353 -- Is file writable?
354 -- (Checks write permission for effective UID.)
355 do
356 set_buffer
357 Result := buffered_file_info.is_writable
358 end
359
360 is_executable: BOOLEAN is
361 -- Is file executable?
362 -- (Checks execute permission for effective UID.)
363 do
364 set_buffer
365 Result := buffered_file_info.is_executable
366 end
367
368 is_creatable: BOOLEAN is
369 -- Is file creatable in parent directory?
370 -- (Uses effective UID to check that parent is writable
371 -- and file does not exist.)
372 local
373 external_name: ANY
374 do
375 external_name := name.to_c
376 Result := file_creatable ($external_name, name.count)
377 end
378
379 is_plain: BOOLEAN is
380 -- Is file a plain file?
381 require
382 file_exists: exists
383 do
384 set_buffer
385 Result := buffered_file_info.is_plain
386 end
387
388 is_device: BOOLEAN is
389 -- Is file a device?
390 require
391 file_exists: exists
392 do
393 set_buffer
394 Result := buffered_file_info.is_device
395 end
396
397 is_directory: BOOLEAN is
398 -- Is file a directory?
399 require
400 file_exists: exists
401 do
402 set_buffer
403 Result := buffered_file_info.is_directory
404 end
405
406 is_symlink: BOOLEAN is
407 -- Is file a symbolic link?
408 require
409 file_exists: exists
410 do
411 set_buffer
412 Result := buffered_file_info.is_symlink
413 end
414
415 is_fifo: BOOLEAN is
416 -- Is file a named pipe?
417 require
418 file_exists: exists
419 do
420 set_buffer
421 Result := buffered_file_info.is_fifo
422 end
423
424 is_socket: BOOLEAN is
425 -- Is file a named socket?
426 require
427 file_exists: exists
428 do
429 set_buffer
430 Result := buffered_file_info.is_socket
431 end
432
433 is_block: BOOLEAN is
434 -- Is file a block special file?
435 require
436 file_exists: exists
437 do
438 set_buffer
439 Result := buffered_file_info.is_block
440 end
441
442 is_character: BOOLEAN is
443 -- Is file a character special file?
444 require
445 file_exists: exists
446 do
447 set_buffer
448 Result := buffered_file_info.is_character
449 end
450
451 is_setuid: BOOLEAN is
452 -- Is file setuid?
453 require
454 file_exists: exists
455 do
456 set_buffer
457 Result := buffered_file_info.is_setuid
458 end
459
460 is_setgid: BOOLEAN is
461 -- Is file setgid?
462 require
463 file_exists: exists
464 do
465 set_buffer
466 Result := buffered_file_info.is_setgid
467 end
468
469 is_sticky: BOOLEAN is
470 -- Is file sticky (for memory swaps)?
471 require
472 file_exists: exists
473 do
474 set_buffer
475 Result := buffered_file_info.is_sticky
476 end
477
478 is_owner: BOOLEAN is
479 -- Is file owned by effective UID?
480 require
481 file_exists: exists
482 do
483 set_buffer
484 Result := buffered_file_info.is_owner
485 end
486
487 is_access_readable: BOOLEAN is
488 -- Is file readable by real UID?
489 require
490 file_exists: exists
491 do
492 set_buffer
493 Result := buffered_file_info.is_access_readable
494 end
495
496 is_access_writable: BOOLEAN is
497 -- Is file writable by real UID?
498 require
499 file_exists: exists
500 do
501 set_buffer
502 Result := buffered_file_info.is_access_writable
503 end
504
505 is_access_executable: BOOLEAN is
506 -- Is file executable by real UID?
507 require
508 file_exists: exists
509 do
510 set_buffer
511 Result := buffered_file_info.is_access_executable
512 end
513
514 is_access_owner: BOOLEAN is
515 -- Is file owned by real UID?
516 require
517 file_exists: exists
518 do
519 set_buffer
520 Result := buffered_file_info.is_access_owner
521 end
522
523 file_readable: BOOLEAN is
524 -- Is there a current item that may be read?
525 do
526 Result := (mode >= Read_write_file or mode = Read_file)
527 and readable
528 end
529
530 is_closed: BOOLEAN is
531 -- Is file closed?
532 do
533 Result := mode = Closed_file
534 end
535
536 is_open_read: BOOLEAN is
537 -- Is file open for reading?
538 do
539 Result := mode = Read_file or else
540 mode = Read_write_file or else
541 mode = Append_read_file
542 end
543
544 is_open_write: BOOLEAN is
545 -- Is file open for writing?
546 do
547 Result := mode = Write_file or else
548 mode = Read_write_file or else
549 mode = Append_read_file or else
550 mode = Append_file
551 end
552
553 is_open_append: BOOLEAN is
554 -- Is file open for appending?
555 do
556 Result := mode = Append_file or else
557 mode = Append_read_file
558 end
559
560 file_writable: BOOLEAN is
561 -- Is there a current item that may be modified?
562 do
563 Result := mode >= Write_file
564 end
565
566 extendible: BOOLEAN is
567 -- May new items be added?
568 do
569 Result := mode >= Write_file
570 end
571
572 file_prunable: BOOLEAN is
573 -- May items be removed?
574 obsolete
575 "Use `prunable' instead."
576 do
577 end
578
579 full: BOOLEAN is False
580 -- Is structure filled to capacity?
581
582 prunable: BOOLEAN is
583 -- Is there an item to be removed?
584 do
585 end
586
587 feature -- Status setting
588
589 open_read is
590 -- Open file in read-only mode.
591 require
592 is_closed: is_closed
593 local
594 external_name: ANY
595 do
596 external_name := name.to_c
597 file_pointer := file_open ($external_name, 0)
598 mode := Read_file
599 ensure
600 exists: exists
601 open_read: is_open_read
602 end
603
604 open_write is
605 -- Open file in write-only mode;
606 -- create it if it does not exist.
607 local
608 external_name: ANY
609 do
610 external_name := name.to_c
611 file_pointer := file_open ($external_name, 1)
612 mode := Write_file
613 ensure
614 exists: exists
615 open_write: is_open_write
616 end
617
618 open_append is
619 -- Open file in append-only mode;
620 -- create it if it does not exist.
621 require
622 is_closed: is_closed
623 local
624 external_name: ANY
625 do
626 external_name := name.to_c
627 file_pointer := file_open ($external_name, 2)
628 mode := Append_file
629 ensure
630 exists: exists
631 open_append: is_open_append
632 end
633
634 open_read_write is
635 -- Open file in read and write mode.
636 require
637 is_closed: is_closed
638 local
639 external_name: ANY
640 do
641 external_name := name.to_c
642 file_pointer := file_open ($external_name, 3)
643 mode := Read_write_file
644 ensure
645 exists: exists
646 open_read: is_open_read
647 open_write: is_open_write
648 end
649
650 create_read_write is
651 -- Open file in read and write mode;
652 -- create it if it does not exist.
653 require
654 is_closed: is_closed
655 local
656 external_name: ANY
657 do
658 external_name := name.to_c
659 file_pointer := file_open ($external_name, 4)
660 mode := Read_write_file
661 ensure
662 exists: exists
663 open_read: is_open_read
664 open_write: is_open_write
665 end
666
667 open_read_append is
668 -- Open file in read and write-at-end mode;
669 -- create it if it does not exist.
670 require
671 is_closed: is_closed
672 local
673 external_name: ANY
674 do
675 external_name := name.to_c
676 file_pointer := file_open ($external_name, 5)
677 mode := Append_read_file
678 ensure
679 exists: exists
680 open_read: is_open_read
681 open_append: is_open_append
682 end
683
684 fd_open_read (fd: INTEGER) is
685 -- Open file of descriptor `fd' in read-only mode.
686 do
687 file_pointer := file_dopen (fd, 0)
688 mode := Read_file
689 ensure
690 exists: exists
691 open_read: is_open_read
692 end
693
694 fd_open_write (fd: INTEGER) is
695 -- Open file of descriptor `fd' in write mode.
696 do
697 file_pointer := file_dopen (fd, 1)
698 mode := Write_file
699 ensure
700 exists: exists
701 open_write: is_open_write
702 end
703
704 fd_open_append (fd: INTEGER) is
705 -- Open file of descriptor `fd' in append mode.
706 do
707 file_pointer := file_dopen (fd, 2)
708 mode := Append_file
709 ensure
710 exists: exists
711 open_append: is_open_append
712 end
713
714 fd_open_read_write (fd: INTEGER) is
715 -- Open file of descriptor `fd' in read-write mode.
716 do
717 file_pointer := file_dopen (fd, 3)
718 mode := Read_write_file
719 ensure
720 exists: exists
721 open_read: is_open_read
722 open_write: is_open_write
723 end
724
725 fd_open_read_append (fd: INTEGER) is
726 -- Open file of descriptor `fd'
727 -- in read and write-at-end mode.
728 local
729 external_name: ANY
730 do
731 external_name := name.to_c
732 file_pointer := file_dopen (fd, 5)
733 mode := Append_read_file
734 ensure
735 exists: exists
736 open_read: is_open_read
737 open_append: is_open_append
738 end
739
740 reopen_read (fname: STRING) is
741 -- Reopen in read-only mode with file of name `fname';
742 -- create file if it does not exist.
743 require
744 is_open: not is_closed
745 valid_name: fname /= Void
746 local
747 external_name: ANY
748 do
749 external_name := fname.to_c
750 file_pointer := file_reopen ($external_name, 0, file_pointer)
751 name := fname
752 mode := Read_file
753 ensure
754 exists: exists
755 open_read: is_open_read
756 end
757
758 reopen_write (fname: STRING) is
759 -- Reopen in write-only mode with file of name `fname';
760 -- create file if it does not exist.
761 require
762 is_open: not is_closed
763 valid_name: fname /= Void
764 local
765 external_name: ANY
766 do
767 external_name := name.to_c
768 file_pointer := file_reopen ($external_name, 1, file_pointer)
769 name := fname
770 mode := Write_file
771 ensure
772 exists: exists
773 open_write: is_open_write
774 end
775
776 reopen_append (fname: STRING) is
777 -- Reopen in append mode with file of name `fname';
778 -- create file if it does not exist.
779 require
780 is_open: not is_closed
781 valid_name: fname /= Void
782 local
783 external_name: ANY
784 do
785 external_name := name.to_c
786 file_pointer := file_reopen ($external_name, 2, file_pointer)
787 name := fname
788 mode := Append_file
789 ensure
790 exists: exists
791 open_append: is_open_append
792 end
793
794 reopen_read_write (fname: STRING) is
795 -- Reopen in read-write mode with file of name `fname'.
796 require
797 is_open: not is_closed
798 valid_name: fname /= Void
799 local
800 external_name: ANY
801 do
802 external_name := name.to_c
803 file_pointer := file_reopen ($external_name, 3, file_pointer)
804 name := fname
805 mode := Read_write_file
806 ensure
807 exists: exists
808 open_read: is_open_read
809 open_write: is_open_write
810 end
811
812 recreate_read_write (fname: STRING) is
813 -- Reopen in read-write mode with file of name `fname';
814 -- create file if it does not exist.
815 require
816 is_open: not is_closed
817 valid_name: fname /= Void
818 local
819 external_name: ANY
820 do
821 external_name := name.to_c
822 file_pointer := file_reopen ($external_name, 4, file_pointer)
823 name := fname
824 mode := Read_write_file
825 ensure
826 exists: exists
827 open_read: is_open_read
828 open_write: is_open_write
829 end
830
831 reopen_read_append (fname: STRING) is
832 -- Reopen in read and write-at-end mode with file
833 -- of name `fname'; create file if it does not exist.
834 require
835 is_open: not is_closed
836 valid_name: fname /= Void
837 local
838 external_name: ANY
839 do
840 external_name := name.to_c
841 file_pointer := file_reopen ($external_name, 5, file_pointer)
842 name := fname
843 mode := Append_read_file
844 ensure
845 exists: exists
846 open_read: is_open_read
847 open_append: is_open_append
848 end
849
850 close is
851 -- Close file.
852 do
853 file_close (file_pointer)
854 mode := Closed_file
855 descriptor_available := False
856 ensure then
857 is_closed: is_closed
858 end
859
860 feature -- Cursor movement
861
862 start is
863 -- Go to first position.
864 require else
865 file_opened: not is_closed
866 do
867 file_go (file_pointer, 0)
868 end
869
870 finish is
871 -- Go to last position.
872 require else
873 file_opened: not is_closed
874 do
875 file_recede (file_pointer, 0)
876 end
877
878 forth is
879 -- Go to next position.
880 require else
881 file_opened: not is_closed
882 do
883 file_move (file_pointer, 1)
884 end
885
886 back is
887 -- Go back one position.
888 do
889 file_move (file_pointer, - 1)
890 end
891
892 move (offset: INTEGER) is
893 -- Advance by `offset' from current location.
894 require
895 file_opened: not is_closed
896 do
897 file_move (file_pointer, offset)
898 end
899
900 go (abs_position: INTEGER) is
901 -- Go to the absolute `position'.
902 -- (New position may be beyond physical length.)
903 require
904 file_opened: not is_closed
905 non_negative_argument: abs_position >= 0
906 do
907 file_go (file_pointer, abs_position)
908 end
909
910 recede (abs_position: INTEGER) is
911 -- Go to the absolute `position' backwards,
912 -- starting from end of file.
913 require
914 file_opened: not is_closed
915 non_negative_argument: abs_position >= 0
916 do
917 file_recede (file_pointer, abs_position)
918 end
919
920 next_line is
921 -- Move to next input line.
922 require
923 is_readable: file_readable
924 do
925 file_tnil (file_pointer)
926 end
927
928 feature -- Element change
929
930 extend (v: CHARACTER) is
931 -- Include `v' at end.
932 do
933 put_character (v)
934 end
935
936 flush is
937 -- Flush buffered data to disk.
938 -- Note that there is no guarantee that the operating
939 -- system will physically write the data to the disk.
940 -- At least it will end up in the buffer cache,
941 -- making the data visible to other processes.
942 require
943 is_open: not is_closed
944 do
945 file_flush (file_pointer)
946 end
947
948 link (fn: STRING) is
949 -- Link current file to `fn'.
950 -- `fn' must not already exist.
951 require
952 file_exists: exists
953 -- `fn' does not exist already
954 local
955 external_name: ANY
956 fn_name: ANY
957 do
958 external_name := name.to_c
959 fn_name := fn.to_c
960 file_link ($external_name, $fn_name)
961 end
962
963 append (f: like Current) is
964 -- Append a copy of the contents of `f'.
965 require else
966 target_is_closed: is_closed
967 source_is_closed: f.is_closed
968 do
969 -- Open in append mode.
970 open_append
971 -- Open `f' in read mode.
972 f.open_read
973 -- Append contents of `f'.
974 file_append (file_pointer, f.file_pointer, f.count)
975 -- Close both files.
976 close
977 f.close
978 ensure then
979 new_count: count = old count + f.count
980 files_closed: f.is_closed and is_closed
981 end
982
983 put_integer, putint (i: INTEGER) is
984 -- Write `i' at current position.
985 deferred
986 end
987
988 put_boolean, putbool (b: BOOLEAN) is
989 -- Write `b' at current position.
990 deferred
991 end
992
993 put_real, putreal (r: REAL) is
994 -- Write `r' at current position.
995 deferred
996 end
997
998 put_double, putdouble (d: DOUBLE) is
999 -- Write `d' at current position.
1000 deferred
1001 end
1002
1003 put_string, putstring (s: STRING) is
1004 -- Write `s' at current position.
1005 local
1006 ext_s: ANY
1007 do
1008 if s.count /= 0 then
1009 ext_s := s.area
1010 file_ps (file_pointer, $ext_s, s.count)
1011 end
1012 end
1013
1014 put_character, putchar (c: CHARACTER) is
1015 -- Write `c' at current position.
1016 do
1017 file_pc (file_pointer, c)
1018 end
1019
1020 put_new_line, new_line is
1021 -- Write a new line character at current position.
1022 do
1023 file_tnwl (file_pointer)
1024 end
1025
1026 stamp (time: INTEGER) is
1027 -- Stamp with `time' (for both access and modification).
1028 require
1029 file_exists: exists
1030 local
1031 external_name: ANY
1032 do
1033 external_name := name.to_c
1034 file_utime ($external_name, time, 2)
1035 ensure
1036 date_updated: date = time -- But race condition possible
1037 end
1038
1039 set_access (time: INTEGER) is
1040 -- Stamp with `time' (access only).
1041 require
1042 file_exists: exists
1043 local
1044 external_name: ANY
1045 do
1046 external_name := name.to_c
1047 file_utime ($external_name, time, 0)
1048 ensure
1049 acess_date_updated: access_date = time -- But race condition might occur
1050 date_unchanged: date = old date -- Modulo a race condition
1051 end
1052
1053 set_date (time: INTEGER) is
1054 -- Stamp with `time' (modification time only).
1055 require
1056 file_exists: exists
1057 local
1058 external_name: ANY
1059 do
1060 external_name := name.to_c
1061 file_utime ($external_name, time, 1)
1062 ensure
1063 access_date_unchanged: access_date = old access_date -- But race condition might occur
1064 date_updated: date = time -- Modulo a race condition
1065 end
1066
1067 change_name (new_name: STRING) is
1068 -- Change file name to `new_name'
1069 require
1070 new_name_not_void: new_name /= Void
1071 file_exists: exists
1072 local
1073 ext_old_name, ext_new_name: ANY
1074 do
1075 ext_old_name := name.to_c
1076 ext_new_name := new_name.to_c
1077 file_rename ($ext_old_name, $ext_new_name)
1078 name := new_name
1079 ensure
1080 name_changed: name.is_equal (new_name)
1081 end
1082
1083 add_permission (who, what: STRING) is
1084 -- Add read, write, execute or setuid permission
1085 -- for `who' ('u', 'g' or 'o') to `what'.
1086 require
1087 -- `who @ 1 in {u, g, o}'
1088 -- For every `i' in 1 .. `what'.`count', `what' @ `i' in {w, r, x, s, t}'
1089 who_is_not_void: who /= Void
1090 what_is_not_void: what /= Void
1091 file_descriptor_exists: exists
1092 local
1093 external_name, ext_who, ext_what: ANY
1094 do
1095 external_name := name.to_c
1096 ext_who := who.to_c
1097 ext_what := what.to_c
1098 file_perm ($external_name, $ext_who, $ext_what, 1)
1099 end
1100
1101 remove_permission (who, what: STRING) is
1102 -- Remove read, write, execute or setuid permission
1103 -- for `who' ('u', 'g' or 'o') to `what'.
1104 require
1105 -- `who @ 1 in {u, g, o}'
1106 -- For every `i' in 1 .. `what'.`count', `what' @ `i' in {w, r, x, s, t}'
1107 who_is_not_void: who /= Void
1108 what_is_not_void: what /= Void
1109 file_descriptor_exists: exists
1110 local
1111 external_name, ext_who, ext_what: ANY
1112 do
1113 external_name := name.to_c
1114 ext_who := who.to_c
1115 ext_what := what.to_c
1116 file_perm ($external_name, $ext_who, $ext_what, 0)
1117 end
1118
1119 change_mode (mask: INTEGER) is
1120 -- Replace mode by `mask'.
1121 require
1122 file_exists: exists
1123 local
1124 external_name: ANY
1125 do
1126 external_name := name.to_c
1127 file_chmod ($external_name, mask)
1128 end
1129
1130 change_owner (new_owner_id: INTEGER) is
1131 -- Change owner of file to `new_owner_id' found in
1132 -- system password file. On some systems this
1133 -- requires super-user privileges.
1134 require
1135 file_exists: exists
1136 local
1137 external_name: ANY
1138 do
1139 external_name := name.to_c
1140 file_chown ($external_name, new_owner_id)
1141 end
1142
1143 change_group (new_group_id: INTEGER) is
1144 -- Change group of file to `new_group_id' found in
1145 -- system password file.
1146 require
1147 file_exists: exists
1148 local
1149 external_name: ANY
1150 do
1151 external_name := name.to_c
1152 file_chgrp ($external_name, new_group_id)
1153 end
1154
1155 change_date: INTEGER is
1156 -- Time stamp of last change.
1157 require
1158 file_exists: exists
1159 do
1160 set_buffer
1161 Result := buffered_file_info.change_date
1162 end
1163
1164 touch is
1165 -- Update time stamp (for both access and modification).
1166 require
1167 file_exists: exists
1168 local
1169 external_name: ANY
1170 do
1171 external_name := name.to_c
1172 file_touch ($external_name)
1173 ensure
1174 date_changed: date /= old date -- Race condition nearly impossible
1175 end
1176
1177 basic_store (object: ANY) is
1178 -- Produce an external representation of the
1179 -- entire object structure reachable from `object'.
1180 -- Retrievable within current system only.
1181 do
1182 c_basic_store (descriptor, $object)
1183 end
1184
1185 general_store (object: ANY) is
1186 -- Produce an external representation of the
1187 -- entire object structure reachable from `object'.
1188 -- Retrievable from other systems for same platform
1189 -- (machine architecture).
1190 --| This feature may use a visible name of a class written
1191 --| in the `visible' clause of the Ace file. This makes it
1192 --| possible to overcome class name clashes.
1193 do
1194 c_general_store (descriptor, $object)
1195 end
1196
1197 independent_store (object: ANY) is
1198 -- Produce an external representation of the
1199 -- entire object structure reachable from `object'.
1200 -- Retrievable from other systems for the same or other
1201 -- platform (machine architecture).
1202 do
1203 c_independent_store (descriptor, $object)
1204 end
1205
1206 feature -- Removal
1207
1208 wipe_out is
1209 -- Remove all items.
1210 require else
1211 is_closed: is_closed
1212 do
1213 open_write
1214 close
1215 end
1216
1217 delete is
1218 -- Remove link with physical file.
1219 -- File does not physically disappear from the disk
1220 -- until no more processes reference it.
1221 -- I/O operations on it are still possible.
1222 -- A directory must be empty to be deleted.
1223 require
1224 exists: exists
1225 local
1226 external_name: ANY
1227 do
1228 external_name := name.to_c
1229 file_unlink ($external_name)
1230 end
1231
1232 reset (fn: STRING) is
1233 -- Change file name to `fn' and reset
1234 -- file descriptor and all information.
1235 require
1236 valid_file_name: fn /= Void
1237 do
1238 name := fn
1239 if mode /= Closed_file then
1240 close
1241 end
1242 last_integer := 0
1243 if last_string /= Void then
1244 last_string.wipe_out
1245 end
1246 last_real := 0.0
1247 last_character := '%U'
1248 last_double := 0.0
1249 ensure
1250 file_renamed: name = fn
1251 file_closed: is_closed
1252 end
1253
1254 feature -- Input
1255
1256 read_real, readreal is
1257 -- Read a new real.
1258 -- Make result available in `last_real'.
1259 require else
1260 is_readable: file_readable
1261 deferred
1262 end
1263
1264 read_double, readdouble is
1265 -- Read a new double.
1266 -- Make result available in `last_double'.
1267 require else
1268 is_readable: file_readable
1269 deferred
1270 end
1271
1272 read_character, readchar is
1273 -- Read a new character.
1274 -- Make result available in `last_character'.
1275 require else
1276 is_readable: file_readable
1277 do
1278 last_character := file_gc (file_pointer)
1279 end
1280
1281 read_integer, readint is
1282 -- Read a new integer.
1283 -- Make result available in `last_integer'.
1284 require else
1285 is_readable: file_readable
1286 deferred
1287 end
1288
1289 read_line, readline is
1290 -- Read a string until new line or end of file.
1291 -- Make result available in `last_string'.
1292 -- New line will be consumed but not part of `last_string'.
1293 require else
1294 is_readable: file_readable
1295 local
1296 str_cap: INTEGER
1297 read: INTEGER -- Amount of bytes already read
1298 str_area: ANY
1299 done: BOOLEAN
1300 do
1301 from
1302 if last_string = Void then
1303 create_last_string (0)
1304 end
1305 str_area := last_string.area
1306 str_cap := last_string.capacity
1307 until
1308 done
1309 loop
1310 read := read + file_gs (file_pointer, $str_area, str_cap, read)
1311 if read > str_cap then
1312 -- End of line not reached yet
1313 --|The string must be consistently set before
1314 --|resizing.
1315 last_string.set_count (str_cap)
1316 if str_cap < 2048 then
1317 last_string.grow (str_cap + 1024)
1318 else
1319 -- Increase capacity by `Growth_percentage' as
1320 -- defined in RESIZABLE.
1321 last_string.automatic_grow
1322 end
1323 str_cap := last_string.capacity
1324 read := read - 1 -- True amount of byte read
1325 str_area := last_string.area
1326 else
1327 last_string.set_count (read)
1328 done := True
1329 end
1330 end
1331 end
1332
1333 read_stream, readstream (nb_char: INTEGER) is
1334 -- Read a string of at most `nb_char' bound characters
1335 -- or until end of file.
1336 -- Make result available in `last_string'.
1337 require else
1338 is_readable: file_readable
1339 local
1340 new_count: INTEGER
1341 str_area: ANY
1342 do
1343 if last_string = Void then
1344 create_last_string (nb_char)
1345 else
1346 last_string.grow (nb_char)
1347 end
1348 str_area := last_string.area
1349 new_count := file_gss (file_pointer, $str_area, nb_char)
1350 last_string.set_count (new_count)
1351 end
1352
1353 read_word, readword is
1354 -- Read a string, excluding white space and stripping
1355 -- leading white space.
1356 -- Make result available in `last_string'.
1357 -- White space characters are: blank, new_line, tab,
1358 -- vertical tab, formfeed, end of file.
1359 require
1360 is_readable: file_readable
1361 local
1362 str_area: ANY
1363 str_cap: INTEGER
1364 read: INTEGER -- Amount of bytes already read
1365 do
1366 from
1367 if last_string = Void then
1368 create_last_string (0)
1369 end
1370 str_area := last_string.area
1371 str_cap := last_string.capacity
1372 until
1373 read > str_cap
1374 loop
1375 read := read +
1376 file_gw (file_pointer, $str_area, str_cap, read)
1377 if read > str_cap then
1378 -- End of word not reached yet.
1379 if str_cap < 2048 then
1380 last_string.grow (str_cap + 1024)
1381 else
1382 -- Increase capacity by `Growth_percentage' as
1383 -- defined in RESIZABLE.
1384 last_string.automatic_grow
1385 end
1386 str_area := last_string.area
1387 str_cap := last_string.capacity
1388 read := read - 1 -- True amount of byte read
1389 else
1390 last_string.set_count (read)
1391 read := str_cap + 1 -- End of loop
1392 end
1393 end
1394 separator := file_lh (file_pointer) -- Look ahead
1395 end
1396
1397 feature -- Convenience
1398
1399 copy_to (file: like Current) is
1400 -- Copy content of current from current cursor
1401 -- position to end of file into `file' from
1402 -- current cursor position of `file'.
1403 require
1404 file_not_void: file /= Void
1405 file_is_open_write: file.is_open_write
1406 current_is_open_read: is_open_read
1407 local
1408 l_modulo, l_read, nb: INTEGER
1409 l_pos: INTEGER
1410 l_old_last_string: STRING
1411 do
1412 from
1413 l_read := 0
1414 nb := count
1415 l_modulo := 51200
1416 l_old_last_string := last_string
1417 last_string := Void
1418 l_pos := position
1419 if l_pos /= 0 then
1420 go (0)
1421 end
1422 until
1423 l_read >= nb
1424 loop
1425 read_stream (l_modulo)
1426 file.put_string (last_string)
1427 l_read := l_read + l_modulo
1428 end
1429 -- Restore previous status of Current file.
1430 if l_pos /= 0 then
1431 go (l_pos)
1432 end
1433 last_string := l_old_last_string
1434 end
1435
1436 feature {NONE} -- Implementation
1437
1438 create_last_string (a_min_size: INTEGER) is
1439 -- Create new instance of `last_string' with a least `a_min_size'
1440 -- as capacity.
1441 require
1442 last_string_void: last_string = Void
1443 a_min_size_non_negative: a_min_size >= 0
1444 do
1445 create last_string.make (default_last_string_size.max (a_min_size))
1446 ensure
1447 last_string_not_void: last_string /= Void
1448 capacity_set: last_string.capacity >= a_min_size
1449 end
1450
1451 default_last_string_size: INTEGER is 256
1452 -- Default size for creating `last_string'
1453
1454 read_to_string (a_string: STRING; pos, nb: INTEGER): INTEGER is
1455 -- Fill `a_string', starting at position `pos' with at
1456 -- most `nb' characters read from current file.
1457 -- Return the number of characters actually read.
1458 require
1459 is_readable: file_readable
1460 not_end_of_file: not end_of_file
1461 a_string_not_void: a_string /= Void
1462 valid_position: a_string.valid_index (pos)
1463 nb_large_enough: nb > 0
1464 nb_small_enough: nb <= a_string.count - pos + 1
1465 deferred
1466 ensure
1467 nb_char_read_large_enough: Result >= 0
1468 nb_char_read_small_enough: Result <= nb
1469 character_read: not end_of_file implies Result > 0
1470 end
1471
1472 true_string: STRING is
1473 -- Character string "true"
1474 once
1475 Result := "True"
1476 end
1477
1478 false_string: STRING is
1479 -- Character string "false"
1480 once
1481 Result := "False"
1482 end
1483
1484 buffered_file_info: UNIX_FILE_INFO is
1485 -- Information about the file.
1486 once
1487 create Result.make
1488 end
1489
1490 set_buffer is
1491 -- Resynchronizes information on file
1492 require
1493 file_exists: exists
1494 do
1495 buffered_file_info.update (name)
1496 end
1497
1498 file_link (from_name, to_name: POINTER) is
1499 -- Link `to_name' to `from_name'
1500 external
1501 "C (char *, char *) | %"eif_file.h%""
1502 end
1503
1504 file_unlink (fname: POINTER) is
1505 -- Delete file `fname'.
1506 external
1507 "C signature (char *) use %"eif_file.h%""
1508 end
1509
1510 file_open (f_name: POINTER; how: INTEGER): POINTER is
1511 -- File pointer for file `f_name', in mode `how'.
1512 external
1513 "C signature (char *, int): EIF_POINTER use %"eif_file.h%""
1514 end
1515
1516 file_dopen (fd, how: INTEGER): POINTER is
1517 -- File pointer for file of descriptor `fd' in mode `how'
1518 -- (which must fit the way `fd' was obtained).
1519 external
1520 "C signature (int, int): EIF_POINTER use %"eif_file.h%""
1521 end
1522
1523 file_reopen (f_name: POINTER; how: INTEGER; file: POINTER): POINTER is
1524 -- File pointer to `file', reopened to have new name `f_name'
1525 -- in a mode specified by `how'.
1526 external
1527 "C (char *, int, FILE *): EIF_POINTER | %"eif_file.h%""
1528 end
1529
1530 file_close (file: POINTER) is
1531 -- Close `file'.
1532 external
1533 "C (FILE *) | %"eif_file.h%""
1534 end
1535
1536 file_flush (file: POINTER) is
1537 -- Flush `file'.
1538 external
1539 "C (FILE *) | %"eif_file.h%""
1540 end
1541
1542 file_fd (file: POINTER): INTEGER is
1543 -- Operating system's file descriptor
1544 external
1545 "C (FILE *): EIF_INTEGER | %"eif_file.h%""
1546 end
1547
1548 file_gc (file: POINTER): CHARACTER is
1549 -- Access the next character
1550 external
1551 "C (FILE *): EIF_CHARACTER | %"eif_file.h%""
1552 end
1553
1554 file_gs (file: POINTER; a_string: POINTER; length, begin: INTEGER): INTEGER is
1555 -- `a_string' updated with characters read from `file'
1556 -- until new line, with `begin' characters already read.
1557 -- If it does not fit, result is `length' - `begin' + 1.
1558 -- If it fits, result is number of characters read.
1559 external
1560 "C (FILE *, char *, EIF_INTEGER, EIF_INTEGER): EIF_INTEGER | %"eif_file.h%""
1561 end
1562
1563 file_gss (file: POINTER; a_string: POINTER; length: INTEGER): INTEGER is
1564 -- Read min (`length', remaining bytes in file) characters
1565 -- into `a_string'. If it does not fit, result is `length' + 1.
1566 -- Otherwise, result is the number of characters read.
1567 external
1568 "C (FILE *, char *, EIF_INTEGER): EIF_INTEGER | %"eif_file.h%""
1569 end
1570
1571 file_gw (file: POINTER; a_string: POINTER; length, begin: INTEGER): INTEGER is
1572 -- Read a string excluding white space and stripping
1573 -- leading white space from `file' into `a_string'.
1574 -- White space characters are: blank, new_line,
1575 -- tab, vertical tab, formfeed or end of file.
1576 -- If it does not fit, result is `length' - `begin' + 1,
1577 -- otherwise result is number of characters read.
1578 external
1579 "C (FILE *, char *, EIF_INTEGER, EIF_INTEGER): EIF_INTEGER | %"eif_file.h%""
1580 end
1581
1582 file_lh (file: POINTER): CHARACTER is
1583 -- Look ahead in `file' and find out the value of the next
1584 -- character. Do not read over character.
1585 external
1586 "C (FILE *): EIF_CHARACTER | %"eif_file.h%""
1587 end
1588
1589 file_size (file: POINTER): INTEGER is
1590 -- Size of `file'
1591 external
1592 "C (FILE *): EIF_INTEGER | %"eif_file.h%""
1593 end
1594
1595 file_tnil (file: POINTER) is
1596 -- Read upto next input line.
1597 external
1598 "C (FILE *) | %"eif_file.h%""
1599 end
1600
1601 file_tell (file: POINTER): INTEGER is
1602 -- Current cursor position in file.
1603 external
1604 "C (FILE *): EIF_INTEGER | %"eif_file.h%""
1605 end
1606
1607 file_touch (f_name: POINTER) is
1608 -- Touch file `f_name'.
1609 external
1610 "C signature (char *) use %"eif_file.h%""
1611 end
1612
1613 file_rename (old_name, new_name: POINTER) is
1614 -- Change file name from `old_name' to `new_name'.
1615 external
1616 "C signature (char *, char *) use %"eif_file.h%""
1617 end
1618
1619 file_perm (f_name, who, what: POINTER; flag: INTEGER) is
1620 -- Change permissions for `f_name' to `who' and `what'.
1621 -- `flag' = 1 -> add permissions,
1622 -- `flag' = 0 -> remove permissions.
1623 external
1624 "C signature (char *, char *, char *, int) use %"eif_file.h%""
1625 end
1626
1627 file_chmod (f_name: POINTER; mask: INTEGER) is
1628 -- Change mode of `f_name' to `mask'.
1629 external
1630 "C signature (char *, int) use %"eif_file.h%""
1631 end
1632
1633 file_chown (f_name: POINTER; new_owner: INTEGER) is
1634 -- Change owner of `f_name' to `new_owner'
1635 external
1636 "C signature (char *, int) use %"eif_file.h%""
1637 end
1638
1639 file_chgrp (f_name: POINTER; new_group: INTEGER) is
1640 -- Change group of `f_name' to `new_group'
1641 external
1642 "C signature (char *, int) use %"eif_file.h%""
1643 end
1644
1645 file_utime (f_name: POINTER; time, how: INTEGER) is
1646 -- Set access, modification time or both (`how' = 0,1,2) on
1647 -- `f_name', using `time' as time stamp.
1648 external
1649 "C signature (char *, int, int) use %"eif_file.h%""
1650 end
1651
1652 file_tnwl (file: POINTER) is
1653 -- Print a new-line to `file'.
1654 external
1655 "C (FILE *) | %"eif_file.h%""
1656 end
1657
1658 file_append (file, from_file: POINTER; length: INTEGER) is
1659 -- Append a copy of `from_file' to `file'
1660 external
1661 "C (FILE *, FILE *, EIF_INTEGER) | %"eif_file.h%""
1662 end
1663
1664 file_ps (file: POINTER; a_string: POINTER; length: INTEGER) is
1665 -- Print `a_string' to `file'.
1666 external
1667 "C (FILE *, char *, EIF_INTEGER) | %"eif_file.h%""
1668 end
1669
1670 file_pc (file: POINTER; c: CHARACTER) is
1671 -- Put `c' to end of `file'.
1672 external
1673 "C (FILE *, EIF_CHARACTER) | %"eif_file.h%""
1674 end
1675
1676 file_go (file: POINTER; abs_position: INTEGER) is
1677 -- Go to absolute `position', originated from start.
1678 external
1679 "C (FILE *, EIF_INTEGER) | %"eif_file.h%""
1680 end
1681
1682 file_recede (file: POINTER; abs_position: INTEGER) is
1683 -- Go to absolute `position', originated from end.
1684 external
1685 "C (FILE *, EIF_INTEGER) | %"eif_file.h%""
1686 end
1687
1688 file_move (file: POINTER; offset: INTEGER) is
1689 -- Move file pointer by `offset'.
1690 external
1691 "C (FILE *, EIF_INTEGER) | %"eif_file.h%""
1692 end
1693
1694 file_feof (file: POINTER): BOOLEAN is
1695 -- End of file?
1696 external
1697 "C (FILE *): EIF_BOOLEAN | %"eif_file.h%""
1698 end
1699
1700 file_exists (f_name: POINTER): BOOLEAN is
1701 -- Does `f_name' exist.
1702 external
1703 "C signature (char *): EIF_BOOLEAN use %"eif_file.h%""
1704 end
1705
1706 file_path_exists (f_name: POINTER): BOOLEAN is
1707 -- Does `f_name' exist.
1708 external
1709 "C signature (char *): EIF_BOOLEAN use %"eif_file.h%""
1710 end
1711
1712 file_access (f_name: POINTER; which: INTEGER): BOOLEAN is
1713 -- Perform access test `which' on `f_name' using real UID.
1714 external
1715 "C signature (char *, EIF_INTEGER): EIF_BOOLEAN use %"eif_file.h%""
1716 end
1717
1718 file_creatable (f_name: POINTER; n: INTEGER): BOOLEAN is
1719 -- Is `f_name' of count `n' creatable.
1720 external
1721 "C signature (char *, EIF_INTEGER): EIF_BOOLEAN use %"eif_file.h%""
1722 end
1723
1724 c_retrieved (file_handle: INTEGER): ANY is
1725 -- Object structured retrieved from file of pointer
1726 -- `file_ptr'
1727 external
1728 "C | %"eif_retrieve.h%""
1729 alias
1730 "eretrieve"
1731 end
1732
1733 c_basic_store (file_handle: INTEGER; object: POINTER) is
1734 -- Store object structure reachable form current object
1735 -- in file pointer `file_ptr'.
1736 external
1737 "C signature (EIF_INTEGER, EIF_REFERENCE) use %"eif_store.h%""
1738 alias
1739 "estore"
1740 end
1741
1742 c_general_store (file_handle: INTEGER; object: POINTER)is
1743 -- Store object structure reachable form current object
1744 -- in file pointer `file_ptr'.
1745 external
1746 "C signature (EIF_INTEGER, EIF_REFERENCE) use %"eif_store.h%""
1747 alias
1748 "eestore"
1749 end
1750
1751 c_independent_store (file_handle: INTEGER; object: POINTER) is
1752 -- Store object structure reachable form current object
1753 -- in file pointer `file_ptr'.
1754 external
1755 "C signature (EIF_INTEGER, EIF_REFERENCE) use %"eif_store.h%""
1756 alias
1757 "sstore"
1758 end
1759
1760 feature {NONE} -- Inapplicable
1761
1762 go_to (r: CURSOR) is
1763 -- Move to position marked `r'.
1764 do
1765 end
1766
1767 replace (v: like item) is
1768 -- Replace current item by `v'.
1769 require else
1770 is_writable: file_writable
1771 do
1772 ensure then
1773 item = v
1774 count = old count
1775 end
1776
1777 remove is
1778 -- Remove current item.
1779 do
1780 end
1781
1782 prune (v: like item) is
1783 -- Remove an occurrence of `v' if any.
1784 do
1785 ensure then
1786 count <= old count
1787 end
1788
1789 feature {FILE} -- Implementation
1790
1791 mode: INTEGER
1792 -- Input-output mode
1793
1794 Closed_file: INTEGER is 0
1795 Read_file: INTEGER is 1
1796 Write_file: INTEGER is 2
1797 Append_file: INTEGER is 3
1798 Read_Write_file: INTEGER is 4
1799 Append_Read_file: INTEGER is 5
1800
1801 set_read_mode is
1802 -- Define file mode as read.
1803 do
1804 mode := Read_file
1805 end
1806
1807 set_write_mode is
1808 -- Define file mode as write.
1809 do
1810 mode := Write_file
1811 end
1812
1813 invariant
1814
1815 valid_mode: Closed_file <= mode and mode <= Append_read_file
1816 name_exists: name /= Void
1817 name_not_empty: not name.is_empty
1818
1819 indexing
1820
1821 library: "[
1822 EiffelBase: Library of reusable components for Eiffel.
1823 ]"
1824
1825 status: "[
1826 Copyright 1986-2001 Interactive Software Engineering (ISE).
1827 For ISE customers the original versions are an ISE product
1828 covered by the ISE Eiffel license and support agreements.
1829 ]"
1830
1831 license: "[
1832 EiffelBase may now be used by anyone as FREE SOFTWARE to
1833 develop any product, public-domain or commercial, without
1834 payment to ISE, under the terms of the ISE Free Eiffel Library
1835 License (IFELL) at http://eiffel.com/products/base/license.html.
1836 ]"
1837
1838 source: "[
1839 Interactive Software Engineering Inc.
1840 ISE Building
1841 360 Storke Road, Goleta, CA 93117 USA
1842 Telephone 805-685-1006, Fax 805-685-6869
1843 Electronic mail <info@eiffel.com>
1844 Customer support http://support.eiffel.com
1845 ]"
1846
1847 info: "[
1848 For latest info see award-winning pages: http://eiffel.com
1849 ]"
1850
1851 end -- class FILE
1852
1853

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.23