/[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 91477 - (show annotations)
Sun Jan 14 09:47:13 2007 UTC (13 years ago) by ericb
File size: 42468 byte(s)
Synchronized with ISE 6.0.65740
1 indexing
2 description:
3 "Sequential files, viewed as persistent sequences of characters"
4 library: "Free implementation of ELKS library"
5 copyright: "Copyright (c) 1986-2006, Eiffel Software and others"
6 license: "Eiffel Forum License v2 (see forum.txt)"
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 -- Comparison
588
589 same_file (fn: STRING): BOOLEAN is
590 -- Is current file the same as `a_filename'?
591 require
592 fn_not_void: fn /= Void
593 fn_not_empty: not fn.is_empty
594 local
595 l_comparer: FILE_COMPARER
596 do
597 create l_comparer
598 Result := l_comparer.same_files (name, fn)
599 end
600
601 feature -- Status setting
602
603 open_read is
604 -- Open file in read-only mode.
605 require
606 is_closed: is_closed
607 local
608 external_name: ANY
609 do
610 external_name := name.to_c
611 file_pointer := file_open ($external_name, 0)
612 mode := Read_file
613 ensure
614 exists: exists
615 open_read: is_open_read
616 end
617
618 open_write is
619 -- Open file in write-only mode;
620 -- create it if it does not exist.
621 local
622 external_name: ANY
623 do
624 external_name := name.to_c
625 file_pointer := file_open ($external_name, 1)
626 mode := Write_file
627 ensure
628 exists: exists
629 open_write: is_open_write
630 end
631
632 open_append is
633 -- Open file in append-only mode;
634 -- create it if it does not exist.
635 require
636 is_closed: is_closed
637 local
638 external_name: ANY
639 do
640 external_name := name.to_c
641 file_pointer := file_open ($external_name, 2)
642 mode := Append_file
643 ensure
644 exists: exists
645 open_append: is_open_append
646 end
647
648 open_read_write is
649 -- Open file in read and write mode.
650 require
651 is_closed: is_closed
652 local
653 external_name: ANY
654 do
655 external_name := name.to_c
656 file_pointer := file_open ($external_name, 3)
657 mode := Read_write_file
658 ensure
659 exists: exists
660 open_read: is_open_read
661 open_write: is_open_write
662 end
663
664 create_read_write is
665 -- Open file in read and write mode;
666 -- create it if it does not exist.
667 require
668 is_closed: is_closed
669 local
670 external_name: ANY
671 do
672 external_name := name.to_c
673 file_pointer := file_open ($external_name, 4)
674 mode := Read_write_file
675 ensure
676 exists: exists
677 open_read: is_open_read
678 open_write: is_open_write
679 end
680
681 open_read_append is
682 -- Open file in read and write-at-end mode;
683 -- create it if it does not exist.
684 require
685 is_closed: is_closed
686 local
687 external_name: ANY
688 do
689 external_name := name.to_c
690 file_pointer := file_open ($external_name, 5)
691 mode := Append_read_file
692 ensure
693 exists: exists
694 open_read: is_open_read
695 open_append: is_open_append
696 end
697
698 fd_open_read (fd: INTEGER) is
699 -- Open file of descriptor `fd' in read-only mode.
700 do
701 file_pointer := file_dopen (fd, 0)
702 mode := Read_file
703 ensure
704 exists: exists
705 open_read: is_open_read
706 end
707
708 fd_open_write (fd: INTEGER) is
709 -- Open file of descriptor `fd' in write mode.
710 do
711 file_pointer := file_dopen (fd, 1)
712 mode := Write_file
713 ensure
714 exists: exists
715 open_write: is_open_write
716 end
717
718 fd_open_append (fd: INTEGER) is
719 -- Open file of descriptor `fd' in append mode.
720 do
721 file_pointer := file_dopen (fd, 2)
722 mode := Append_file
723 ensure
724 exists: exists
725 open_append: is_open_append
726 end
727
728 fd_open_read_write (fd: INTEGER) is
729 -- Open file of descriptor `fd' in read-write mode.
730 do
731 file_pointer := file_dopen (fd, 3)
732 mode := Read_write_file
733 ensure
734 exists: exists
735 open_read: is_open_read
736 open_write: is_open_write
737 end
738
739 fd_open_read_append (fd: INTEGER) is
740 -- Open file of descriptor `fd'
741 -- in read and write-at-end mode.
742 local
743 external_name: ANY
744 do
745 external_name := name.to_c
746 file_pointer := file_dopen (fd, 5)
747 mode := Append_read_file
748 ensure
749 exists: exists
750 open_read: is_open_read
751 open_append: is_open_append
752 end
753
754 reopen_read (fname: STRING) is
755 -- Reopen in read-only mode with file of name `fname';
756 -- create file if it does not exist.
757 require
758 is_open: not is_closed
759 valid_name: fname /= Void
760 local
761 external_name: ANY
762 do
763 external_name := fname.to_c
764 file_pointer := file_reopen ($external_name, 0, file_pointer)
765 name := fname
766 mode := Read_file
767 ensure
768 exists: exists
769 open_read: is_open_read
770 end
771
772 reopen_write (fname: STRING) is
773 -- Reopen in write-only mode with file of name `fname';
774 -- create file if it does not exist.
775 require
776 is_open: not is_closed
777 valid_name: fname /= Void
778 local
779 external_name: ANY
780 do
781 external_name := name.to_c
782 file_pointer := file_reopen ($external_name, 1, file_pointer)
783 name := fname
784 mode := Write_file
785 ensure
786 exists: exists
787 open_write: is_open_write
788 end
789
790 reopen_append (fname: STRING) is
791 -- Reopen in append mode with file of name `fname';
792 -- create file if it does not exist.
793 require
794 is_open: not is_closed
795 valid_name: fname /= Void
796 local
797 external_name: ANY
798 do
799 external_name := name.to_c
800 file_pointer := file_reopen ($external_name, 2, file_pointer)
801 name := fname
802 mode := Append_file
803 ensure
804 exists: exists
805 open_append: is_open_append
806 end
807
808 reopen_read_write (fname: STRING) is
809 -- Reopen in read-write mode with file of name `fname'.
810 require
811 is_open: not is_closed
812 valid_name: fname /= Void
813 local
814 external_name: ANY
815 do
816 external_name := name.to_c
817 file_pointer := file_reopen ($external_name, 3, file_pointer)
818 name := fname
819 mode := Read_write_file
820 ensure
821 exists: exists
822 open_read: is_open_read
823 open_write: is_open_write
824 end
825
826 recreate_read_write (fname: STRING) is
827 -- Reopen in read-write mode with file of name `fname';
828 -- create file if it does not exist.
829 require
830 is_open: not is_closed
831 valid_name: fname /= Void
832 local
833 external_name: ANY
834 do
835 external_name := name.to_c
836 file_pointer := file_reopen ($external_name, 4, file_pointer)
837 name := fname
838 mode := Read_write_file
839 ensure
840 exists: exists
841 open_read: is_open_read
842 open_write: is_open_write
843 end
844
845 reopen_read_append (fname: STRING) is
846 -- Reopen in read and write-at-end mode with file
847 -- of name `fname'; create file if it does not exist.
848 require
849 is_open: not is_closed
850 valid_name: fname /= Void
851 local
852 external_name: ANY
853 do
854 external_name := name.to_c
855 file_pointer := file_reopen ($external_name, 5, file_pointer)
856 name := fname
857 mode := Append_read_file
858 ensure
859 exists: exists
860 open_read: is_open_read
861 open_append: is_open_append
862 end
863
864 close is
865 -- Close file.
866 do
867 file_close (file_pointer)
868 mode := Closed_file
869 descriptor_available := False
870 ensure then
871 is_closed: is_closed
872 end
873
874 feature -- Cursor movement
875
876 start is
877 -- Go to first position.
878 require else
879 file_opened: not is_closed
880 do
881 file_go (file_pointer, 0)
882 end
883
884 finish is
885 -- Go to last position.
886 require else
887 file_opened: not is_closed
888 do
889 file_recede (file_pointer, 0)
890 end
891
892 forth is
893 -- Go to next position.
894 require else
895 file_opened: not is_closed
896 do
897 file_move (file_pointer, 1)
898 end
899
900 back is
901 -- Go back one position.
902 do
903 file_move (file_pointer, - 1)
904 end
905
906 move (offset: INTEGER) is
907 -- Advance by `offset' from current location.
908 require
909 file_opened: not is_closed
910 do
911 file_move (file_pointer, offset)
912 end
913
914 go (abs_position: INTEGER) is
915 -- Go to the absolute `position'.
916 -- (New position may be beyond physical length.)
917 require
918 file_opened: not is_closed
919 non_negative_argument: abs_position >= 0
920 do
921 file_go (file_pointer, abs_position)
922 end
923
924 recede (abs_position: INTEGER) is
925 -- Go to the absolute `position' backwards,
926 -- starting from end of file.
927 require
928 file_opened: not is_closed
929 non_negative_argument: abs_position >= 0
930 do
931 file_recede (file_pointer, abs_position)
932 end
933
934 next_line is
935 -- Move to next input line.
936 require
937 is_readable: file_readable
938 do
939 file_tnil (file_pointer)
940 end
941
942 feature -- Element change
943
944 extend (v: CHARACTER) is
945 -- Include `v' at end.
946 do
947 put_character (v)
948 end
949
950 flush is
951 -- Flush buffered data to disk.
952 -- Note that there is no guarantee that the operating
953 -- system will physically write the data to the disk.
954 -- At least it will end up in the buffer cache,
955 -- making the data visible to other processes.
956 require
957 is_open: not is_closed
958 do
959 file_flush (file_pointer)
960 end
961
962 link (fn: STRING) is
963 -- Link current file to `fn'.
964 -- `fn' must not already exist.
965 require
966 file_exists: exists
967 -- `fn' does not exist already
968 local
969 external_name: ANY
970 fn_name: ANY
971 do
972 external_name := name.to_c
973 fn_name := fn.to_c
974 file_link ($external_name, $fn_name)
975 end
976
977 append (f: like Current) is
978 -- Append a copy of the contents of `f'.
979 require else
980 target_is_closed: is_closed
981 source_is_closed: f.is_closed
982 do
983 -- Open in append mode.
984 open_append
985 -- Open `f' in read mode.
986 f.open_read
987 -- Append contents of `f'.
988 file_append (file_pointer, f.file_pointer, f.count)
989 -- Close both files.
990 close
991 f.close
992 ensure then
993 new_count: count = old count + f.count
994 files_closed: f.is_closed and is_closed
995 end
996
997 put_integer, putint (i: INTEGER) is
998 -- Write `i' at current position.
999 deferred
1000 end
1001
1002 put_boolean, putbool (b: BOOLEAN) is
1003 -- Write `b' at current position.
1004 deferred
1005 end
1006
1007 put_real, putreal (r: REAL) is
1008 -- Write `r' at current position.
1009 deferred
1010 end
1011
1012 put_double, putdouble (d: DOUBLE) is
1013 -- Write `d' at current position.
1014 deferred
1015 end
1016
1017 put_string, putstring (s: STRING) is
1018 -- Write `s' at current position.
1019 local
1020 ext_s: ANY
1021 do
1022 if s.count /= 0 then
1023 ext_s := s.area
1024 file_ps (file_pointer, $ext_s, s.count)
1025 end
1026 end
1027
1028 put_managed_pointer (p: MANAGED_POINTER; start_pos, nb_bytes: INTEGER) is
1029 -- Put data of length `nb_bytes' pointed by `start_pos' index in `p' at
1030 -- current position.
1031 do
1032 file_ps (file_pointer, p.item + start_pos, nb_bytes)
1033 end
1034
1035 put_character, putchar (c: CHARACTER) is
1036 -- Write `c' at current position.
1037 do
1038 file_pc (file_pointer, c)
1039 end
1040
1041 put_new_line, new_line is
1042 -- Write a new line character at current position.
1043 do
1044 file_tnwl (file_pointer)
1045 end
1046
1047 stamp (time: INTEGER) is
1048 -- Stamp with `time' (for both access and modification).
1049 require
1050 file_exists: exists
1051 local
1052 external_name: ANY
1053 do
1054 external_name := name.to_c
1055 file_utime ($external_name, time, 2)
1056 ensure
1057 date_updated: date = time -- But race condition possible
1058 end
1059
1060 set_access (time: INTEGER) is
1061 -- Stamp with `time' (access only).
1062 require
1063 file_exists: exists
1064 local
1065 external_name: ANY
1066 do
1067 external_name := name.to_c
1068 file_utime ($external_name, time, 0)
1069 ensure
1070 acess_date_updated: access_date = time -- But race condition might occur
1071 date_unchanged: date = old date -- Modulo a race condition
1072 end
1073
1074 set_date (time: INTEGER) is
1075 -- Stamp with `time' (modification time only).
1076 require
1077 file_exists: exists
1078 local
1079 external_name: ANY
1080 do
1081 external_name := name.to_c
1082 file_utime ($external_name, time, 1)
1083 ensure
1084 access_date_unchanged: access_date = old access_date -- But race condition might occur
1085 date_updated: date = time -- Modulo a race condition
1086 end
1087
1088 change_name (new_name: STRING) is
1089 -- Change file name to `new_name'
1090 require
1091 new_name_not_void: new_name /= Void
1092 new_name_not_empty: not new_name.is_empty
1093 file_exists: exists
1094 local
1095 ext_old_name, ext_new_name: ANY
1096 do
1097 ext_old_name := name.to_c
1098 ext_new_name := new_name.to_c
1099 file_rename ($ext_old_name, $ext_new_name)
1100 name := new_name
1101 ensure
1102 name_changed: name.is_equal (new_name)
1103 end
1104
1105 add_permission (who, what: STRING) is
1106 -- Add read, write, execute or setuid permission
1107 -- for `who' ('u', 'g' or 'o') to `what'.
1108 require
1109 -- `who @ 1 in {u, g, o}'
1110 -- For every `i' in 1 .. `what'.`count', `what' @ `i' in {w, r, x, s, t}'
1111 who_is_not_void: who /= Void
1112 what_is_not_void: what /= Void
1113 file_descriptor_exists: exists
1114 local
1115 external_name, ext_who, ext_what: ANY
1116 do
1117 external_name := name.to_c
1118 ext_who := who.to_c
1119 ext_what := what.to_c
1120 file_perm ($external_name, $ext_who, $ext_what, 1)
1121 end
1122
1123 remove_permission (who, what: STRING) is
1124 -- Remove read, write, execute or setuid permission
1125 -- for `who' ('u', 'g' or 'o') to `what'.
1126 require
1127 -- `who @ 1 in {u, g, o}'
1128 -- For every `i' in 1 .. `what'.`count', `what' @ `i' in {w, r, x, s, t}'
1129 who_is_not_void: who /= Void
1130 what_is_not_void: what /= Void
1131 file_descriptor_exists: exists
1132 local
1133 external_name, ext_who, ext_what: ANY
1134 do
1135 external_name := name.to_c
1136 ext_who := who.to_c
1137 ext_what := what.to_c
1138 file_perm ($external_name, $ext_who, $ext_what, 0)
1139 end
1140
1141 change_mode (mask: INTEGER) is
1142 -- Replace mode by `mask'.
1143 require
1144 file_exists: exists
1145 local
1146 external_name: ANY
1147 do
1148 external_name := name.to_c
1149 file_chmod ($external_name, mask)
1150 end
1151
1152 change_owner (new_owner_id: INTEGER) is
1153 -- Change owner of file to `new_owner_id' found in
1154 -- system password file. On some systems this
1155 -- requires super-user privileges.
1156 require
1157 file_exists: exists
1158 local
1159 external_name: ANY
1160 do
1161 external_name := name.to_c
1162 file_chown ($external_name, new_owner_id)
1163 end
1164
1165 change_group (new_group_id: INTEGER) is
1166 -- Change group of file to `new_group_id' found in
1167 -- system password file.
1168 require
1169 file_exists: exists
1170 local
1171 external_name: ANY
1172 do
1173 external_name := name.to_c
1174 file_chgrp ($external_name, new_group_id)
1175 end
1176
1177 change_date: INTEGER is
1178 -- Time stamp of last change.
1179 require
1180 file_exists: exists
1181 do
1182 set_buffer
1183 Result := buffered_file_info.change_date
1184 end
1185
1186 touch is
1187 -- Update time stamp (for both access and modification).
1188 require
1189 file_exists: exists
1190 local
1191 external_name: ANY
1192 do
1193 external_name := name.to_c
1194 file_touch ($external_name)
1195 ensure
1196 date_changed: date /= old date -- Race condition nearly impossible
1197 end
1198
1199 basic_store (object: ANY) is
1200 -- Produce an external representation of the
1201 -- entire object structure reachable from `object'.
1202 -- Retrievable within current system only.
1203 do
1204 c_basic_store (descriptor, $object)
1205 end
1206
1207 general_store (object: ANY) is
1208 -- Produce an external representation of the
1209 -- entire object structure reachable from `object'.
1210 -- Retrievable from other systems for same platform
1211 -- (machine architecture).
1212 --| This feature may use a visible name of a class written
1213 --| in the `visible' clause of the Ace file. This makes it
1214 --| possible to overcome class name clashes.
1215 do
1216 c_general_store (descriptor, $object)
1217 end
1218
1219 independent_store (object: ANY) is
1220 -- Produce an external representation of the
1221 -- entire object structure reachable from `object'.
1222 -- Retrievable from other systems for the same or other
1223 -- platform (machine architecture).
1224 do
1225 c_independent_store (descriptor, $object)
1226 end
1227
1228 feature -- Removal
1229
1230 wipe_out is
1231 -- Remove all items.
1232 require else
1233 is_closed: is_closed
1234 do
1235 open_write
1236 close
1237 end
1238
1239 delete is
1240 -- Remove link with physical file.
1241 -- File does not physically disappear from the disk
1242 -- until no more processes reference it.
1243 -- I/O operations on it are still possible.
1244 -- A directory must be empty to be deleted.
1245 require
1246 exists: exists
1247 local
1248 external_name: ANY
1249 do
1250 external_name := name.to_c
1251 file_unlink ($external_name)
1252 end
1253
1254 reset (fn: STRING) is
1255 -- Change file name to `fn' and reset
1256 -- file descriptor and all information.
1257 require
1258 valid_file_name: fn /= Void
1259 do
1260 name := fn
1261 if mode /= Closed_file then
1262 close
1263 end
1264 last_integer := 0
1265 if last_string /= Void then
1266 last_string.wipe_out
1267 end
1268 last_real := 0.0
1269 last_character := '%U'
1270 last_double := 0.0
1271 ensure
1272 file_renamed: name = fn
1273 file_closed: is_closed
1274 end
1275
1276 feature -- Input
1277
1278 read_real, readreal is
1279 -- Read a new real.
1280 -- Make result available in `last_real'.
1281 require else
1282 is_readable: file_readable
1283 deferred
1284 end
1285
1286 read_double, readdouble is
1287 -- Read a new double.
1288 -- Make result available in `last_double'.
1289 require else
1290 is_readable: file_readable
1291 deferred
1292 end
1293
1294 read_character, readchar is
1295 -- Read a new character.
1296 -- Make result available in `last_character'.
1297 require else
1298 is_readable: file_readable
1299 do
1300 last_character := file_gc (file_pointer)
1301 end
1302
1303 read_integer, readint is
1304 -- Read a new integer.
1305 -- Make result available in `last_integer'.
1306 require else
1307 is_readable: file_readable
1308 deferred
1309 end
1310
1311 read_line, readline is
1312 -- Read a string until new line or end of file.
1313 -- Make result available in `last_string'.
1314 -- New line will be consumed but not part of `last_string'.
1315 require else
1316 is_readable: file_readable
1317 local
1318 str_cap: INTEGER
1319 read: INTEGER -- Amount of bytes already read
1320 str_area: ANY
1321 done: BOOLEAN
1322 do
1323 from
1324 if last_string = Void then
1325 create_last_string (0)
1326 end
1327 str_area := last_string.area
1328 str_cap := last_string.capacity
1329 until
1330 done
1331 loop
1332 read := read + file_gs (file_pointer, $str_area, str_cap, read)
1333 if read > str_cap then
1334 -- End of line not reached yet
1335 --|The string must be consistently set before
1336 --|resizing.
1337 last_string.set_count (str_cap)
1338 if str_cap < 2048 then
1339 last_string.grow (str_cap + 1024)
1340 else
1341 -- Increase capacity by `Growth_percentage' as
1342 -- defined in RESIZABLE.
1343 last_string.automatic_grow
1344 end
1345 str_cap := last_string.capacity
1346 read := read - 1 -- True amount of byte read
1347 str_area := last_string.area
1348 else
1349 last_string.set_count (read)
1350 done := True
1351 end
1352 end
1353 end
1354
1355 read_stream, readstream (nb_char: INTEGER) is
1356 -- Read a string of at most `nb_char' bound characters
1357 -- or until end of file.
1358 -- Make result available in `last_string'.
1359 require else
1360 is_readable: file_readable
1361 local
1362 new_count: INTEGER
1363 str_area: ANY
1364 do
1365 if last_string = Void then
1366 create_last_string (nb_char)
1367 else
1368 last_string.grow (nb_char)
1369 end
1370 str_area := last_string.area
1371 new_count := file_gss (file_pointer, $str_area, nb_char)
1372 last_string.set_count (new_count)
1373 end
1374
1375 read_to_managed_pointer (p: MANAGED_POINTER; start_pos, nb_bytes: INTEGER) is
1376 -- Read at most `nb_bytes' bound bytes and make result
1377 -- available in `p' at position `start_pos'.
1378 require else
1379 p_not_void: p /= Void
1380 p_large_enough: p.count >= nb_bytes + start_pos
1381 is_readable: file_readable
1382 do
1383 bytes_read := file_gss (file_pointer, p.item + start_pos, nb_bytes)
1384 end
1385
1386 read_word, readword is
1387 -- Read a string, excluding white space and stripping
1388 -- leading white space.
1389 -- Make result available in `last_string'.
1390 -- White space characters are: blank, new_line, tab,
1391 -- vertical tab, formfeed, end of file.
1392 require
1393 is_readable: file_readable
1394 local
1395 str_area: ANY
1396 str_cap: INTEGER
1397 read: INTEGER -- Amount of bytes already read
1398 do
1399 from
1400 if last_string = Void then
1401 create_last_string (0)
1402 end
1403 str_area := last_string.area
1404 str_cap := last_string.capacity
1405 until
1406 read > str_cap
1407 loop
1408 read := read +
1409 file_gw (file_pointer, $str_area, str_cap, read)
1410 if read > str_cap then
1411 -- End of word not reached yet.
1412 if str_cap < 2048 then
1413 last_string.grow (str_cap + 1024)
1414 else
1415 -- Increase capacity by `Growth_percentage' as
1416 -- defined in RESIZABLE.
1417 last_string.automatic_grow
1418 end
1419 str_area := last_string.area
1420 str_cap := last_string.capacity
1421 read := read - 1 -- True amount of byte read
1422 else
1423 last_string.set_count (read)
1424 read := str_cap + 1 -- End of loop
1425 end
1426 end
1427 separator := file_lh (file_pointer) -- Look ahead
1428 ensure
1429 last_string_not_void: last_string /= Void
1430 end
1431
1432 feature -- Convenience
1433
1434 copy_to (file: like Current) is
1435 -- Copy content of current from current cursor
1436 -- position to end of file into `file' from
1437 -- current cursor position of `file'.
1438 require
1439 file_not_void: file /= Void
1440 file_is_open_write: file.is_open_write
1441 current_is_open_read: is_open_read
1442 local
1443 l_modulo, l_read, nb: INTEGER
1444 l_pos: INTEGER
1445 l_old_last_string: STRING
1446 do
1447 from
1448 l_read := 0
1449 nb := count
1450 l_modulo := 51200
1451 l_old_last_string := last_string
1452 last_string := Void
1453 l_pos := position
1454 if l_pos /= 0 then
1455 go (0)
1456 end
1457 until
1458 l_read >= nb
1459 loop
1460 read_stream (l_modulo)
1461 file.put_string (last_string)
1462 l_read := l_read + l_modulo
1463 end
1464 -- Restore previous status of Current file.
1465 if l_pos /= 0 then
1466 go (l_pos)
1467 end
1468 last_string := l_old_last_string
1469 end
1470
1471 feature {NONE} -- Implementation
1472
1473 create_last_string (a_min_size: INTEGER) is
1474 -- Create new instance of `last_string' with a least `a_min_size'
1475 -- as capacity.
1476 require
1477 last_string_void: last_string = Void
1478 a_min_size_non_negative: a_min_size >= 0
1479 do
1480 create last_string.make (default_last_string_size.max (a_min_size))
1481 ensure
1482 last_string_not_void: last_string /= Void
1483 capacity_set: last_string.capacity >= a_min_size
1484 end
1485
1486 default_last_string_size: INTEGER is 256
1487 -- Default size for creating `last_string'
1488
1489 read_to_string (a_string: STRING; pos, nb: INTEGER): INTEGER is
1490 -- Fill `a_string', starting at position `pos' with at
1491 -- most `nb' characters read from current file.
1492 -- Return the number of characters actually read.
1493 require
1494 is_readable: file_readable
1495 not_end_of_file: not end_of_file
1496 a_string_not_void: a_string /= Void
1497 valid_position: a_string.valid_index (pos)
1498 nb_large_enough: nb > 0
1499 nb_small_enough: nb <= a_string.count - pos + 1
1500 deferred
1501 ensure
1502 nb_char_read_large_enough: Result >= 0
1503 nb_char_read_small_enough: Result <= nb
1504 character_read: not end_of_file implies Result > 0
1505 end
1506
1507 true_string: STRING is
1508 -- Character string "true"
1509 once
1510 Result := "True"
1511 end
1512
1513 false_string: STRING is
1514 -- Character string "false"
1515 once
1516 Result := "False"
1517 end
1518
1519 buffered_file_info: UNIX_FILE_INFO is
1520 -- Information about the file.
1521 once
1522 create Result.make
1523 end
1524
1525 set_buffer is
1526 -- Resynchronizes information on file
1527 require
1528 file_exists: exists
1529 do
1530 buffered_file_info.update (name)
1531 end
1532
1533 file_link (from_name, to_name: POINTER) is
1534 -- Link `to_name' to `from_name'
1535 external
1536 "C signature (char *, char *) use %"eif_file.h%""
1537 end
1538
1539 file_unlink (fname: POINTER) is
1540 -- Delete file `fname'.
1541 external
1542 "C signature (char *) use %"eif_file.h%""
1543 end
1544
1545 file_open (f_name: POINTER; how: INTEGER): POINTER is
1546 -- File pointer for file `f_name', in mode `how'.
1547 external
1548 "C signature (char *, int): EIF_POINTER use %"eif_file.h%""
1549 end
1550
1551 file_dopen (fd, how: INTEGER): POINTER is
1552 -- File pointer for file of descriptor `fd' in mode `how'
1553 -- (which must fit the way `fd' was obtained).
1554 external
1555 "C signature (int, int): EIF_POINTER use %"eif_file.h%""
1556 end
1557
1558 file_reopen (f_name: POINTER; how: INTEGER; file: POINTER): POINTER is
1559 -- File pointer to `file', reopened to have new name `f_name'
1560 -- in a mode specified by `how'.
1561 external
1562 "C signature (char *, int, FILE *): EIF_POINTER use %"eif_file.h%""
1563 end
1564
1565 file_close (file: POINTER) is
1566 -- Close `file'.
1567 external
1568 "C signature (FILE *) use %"eif_file.h%""
1569 end
1570
1571 file_flush (file: POINTER) is
1572 -- Flush `file'.
1573 external
1574 "C signature (FILE *) use %"eif_file.h%""
1575 end
1576
1577 file_fd (file: POINTER): INTEGER is
1578 -- Operating system's file descriptor
1579 external
1580 "C signature (FILE *): EIF_INTEGER use %"eif_file.h%""
1581 end
1582
1583 file_gc (file: POINTER): CHARACTER is
1584 -- Access the next character
1585 external
1586 "C signature (FILE *): EIF_CHARACTER use %"eif_file.h%""
1587 end
1588
1589 file_gs (file: POINTER; a_string: POINTER; length, begin: INTEGER): INTEGER is
1590 -- `a_string' updated with characters read from `file'
1591 -- until new line, with `begin' characters already read.
1592 -- If it does not fit, result is `length' - `begin' + 1.
1593 -- If it fits, result is number of characters read.
1594 external
1595 "C signature (FILE *, char *, EIF_INTEGER, EIF_INTEGER): EIF_INTEGER use %"eif_file.h%""
1596 end
1597
1598 file_gss (file: POINTER; a_string: POINTER; length: INTEGER): INTEGER is
1599 -- Read min (`length', remaining bytes in file) characters
1600 -- into `a_string'. If it does not fit, result is `length' + 1.
1601 -- Otherwise, result is the number of characters read.
1602 external
1603 "C signature (FILE *, char *, EIF_INTEGER): EIF_INTEGER use %"eif_file.h%""
1604 end
1605
1606 file_gw (file: POINTER; a_string: POINTER; length, begin: INTEGER): INTEGER is
1607 -- Read a string excluding white space and stripping
1608 -- leading white space from `file' into `a_string'.
1609 -- White space characters are: blank, new_line,
1610 -- tab, vertical tab, formfeed or end of file.
1611 -- If it does not fit, result is `length' - `begin' + 1,
1612 -- otherwise result is number of characters read.
1613 external
1614 "C signature (FILE *, char *, EIF_INTEGER, EIF_INTEGER): EIF_INTEGER use %"eif_file.h%""
1615 end
1616
1617 file_lh (file: POINTER): CHARACTER is
1618 -- Look ahead in `file' and find out the value of the next
1619 -- character. Do not read over character.
1620 external
1621 "C signature (FILE *): EIF_CHARACTER use %"eif_file.h%""
1622 end
1623
1624 file_size (file: POINTER): INTEGER is
1625 -- Size of `file'
1626 external
1627 "C signature (FILE *): EIF_INTEGER use %"eif_file.h%""
1628 alias
1629 "eif_file_size"
1630 end
1631
1632 file_tnil (file: POINTER) is
1633 -- Read upto next input line.
1634 external
1635 "C signature (FILE *) use %"eif_file.h%""
1636 end
1637
1638 file_tell (file: POINTER): INTEGER is
1639 -- Current cursor position in file.
1640 external
1641 "C signature (FILE *): EIF_INTEGER use %"eif_file.h%""
1642 end
1643
1644 file_touch (f_name: POINTER) is
1645 -- Touch file `f_name'.
1646 external
1647 "C signature (char *) use %"eif_file.h%""
1648 end
1649
1650 file_rename (old_name, new_name: POINTER) is
1651 -- Change file name from `old_name' to `new_name'.
1652 external
1653 "C signature (char *, char *) use %"eif_file.h%""
1654 end
1655
1656 file_perm (f_name, who, what: POINTER; flag: INTEGER) is
1657 -- Change permissions for `f_name' to `who' and `what'.
1658 -- `flag' = 1 -> add permissions,
1659 -- `flag' = 0 -> remove permissions.
1660 external
1661 "C signature (char *, char *, char *, int) use %"eif_file.h%""
1662 end
1663
1664 file_chmod (f_name: POINTER; mask: INTEGER) is
1665 -- Change mode of `f_name' to `mask'.
1666 external
1667 "C signature (char *, int) use %"eif_file.h%""
1668 end
1669
1670 file_chown (f_name: POINTER; new_owner: INTEGER) is
1671 -- Change owner of `f_name' to `new_owner'
1672 external
1673 "C signature (char *, int) use %"eif_file.h%""
1674 end
1675
1676 file_chgrp (f_name: POINTER; new_group: INTEGER) is
1677 -- Change group of `f_name' to `new_group'
1678 external
1679 "C signature (char *, int) use %"eif_file.h%""
1680 end
1681
1682 file_utime (f_name: POINTER; time, how: INTEGER) is
1683 -- Set access, modification time or both (`how' = 0,1,2) on
1684 -- `f_name', using `time' as time stamp.
1685 external
1686 "C signature (char *, int, int) use %"eif_file.h%""
1687 end
1688
1689 file_tnwl (file: POINTER) is
1690 -- Print a new-line to `file'.
1691 external
1692 "C signature (FILE *) use %"eif_file.h%""
1693 end
1694
1695 file_append (file, from_file: POINTER; length: INTEGER) is
1696 -- Append a copy of `from_file' to `file'
1697 external
1698 "C signature (FILE *, FILE *, EIF_INTEGER) use %"eif_file.h%""
1699 end
1700
1701 file_ps (file: POINTER; a_string: POINTER; length: INTEGER) is
1702 -- Print `a_string' to `file'.
1703 external
1704 "C signature (FILE *, char *, EIF_INTEGER) use %"eif_file.h%""
1705 end
1706
1707 file_pc (file: POINTER; c: CHARACTER) is
1708 -- Put `c' to end of `file'.
1709 external
1710 "C signature (FILE *, EIF_CHARACTER) use %"eif_file.h%""
1711 end
1712
1713 file_go (file: POINTER; abs_position: INTEGER) is
1714 -- Go to absolute `position', originated from start.
1715 external
1716 "C signature (FILE *, EIF_INTEGER) use %"eif_file.h%""
1717 end
1718
1719 file_recede (file: POINTER; abs_position: INTEGER) is
1720 -- Go to absolute `position', originated from end.
1721 external
1722 "C signature (FILE *, EIF_INTEGER) use %"eif_file.h%""
1723 end
1724
1725 file_move (file: POINTER; offset: INTEGER) is
1726 -- Move file pointer by `offset'.
1727 external
1728 "C signature (FILE *, EIF_INTEGER) use %"eif_file.h%""
1729 end
1730
1731 file_feof (file: POINTER): BOOLEAN is
1732 -- End of file?
1733 external
1734 "C signature (FILE *): EIF_BOOLEAN use %"eif_file.h%""
1735 end
1736
1737 file_exists (f_name: POINTER): BOOLEAN is
1738 -- Does `f_name' exist.
1739 external
1740 "C signature (char *): EIF_BOOLEAN use %"eif_file.h%""
1741 end
1742
1743 file_path_exists (f_name: POINTER): BOOLEAN is
1744 -- Does `f_name' exist.
1745 external
1746 "C signature (char *): EIF_BOOLEAN use %"eif_file.h%""
1747 end
1748
1749 file_access (f_name: POINTER; which: INTEGER): BOOLEAN is
1750 -- Perform access test `which' on `f_name' using real UID.
1751 external
1752 "C signature (char *, EIF_INTEGER): EIF_BOOLEAN use %"eif_file.h%""
1753 end
1754
1755 file_creatable (f_name: POINTER; n: INTEGER): BOOLEAN is
1756 -- Is `f_name' of count `n' creatable.
1757 external
1758 "C signature (char *, EIF_INTEGER): EIF_BOOLEAN use %"eif_file.h%""
1759 end
1760
1761 c_retrieved (file_handle: INTEGER): ANY is
1762 -- Object structured retrieved from file of pointer
1763 -- `file_ptr'
1764 external
1765 "C use %"eif_retrieve.h%""
1766 alias
1767 "eretrieve"
1768 end
1769
1770 c_basic_store (file_handle: INTEGER; object: POINTER) is
1771 -- Store object structure reachable form current object
1772 -- in file pointer `file_ptr'.
1773 external
1774 "C signature (EIF_INTEGER, EIF_REFERENCE) use %"eif_store.h%""
1775 alias
1776 "estore"
1777 end
1778
1779 c_general_store (file_handle: INTEGER; object: POINTER)is
1780 -- Store object structure reachable form current object
1781 -- in file pointer `file_ptr'.
1782 external
1783 "C signature (EIF_INTEGER, EIF_REFERENCE) use %"eif_store.h%""
1784 alias
1785 "eestore"
1786 end
1787
1788 c_independent_store (file_handle: INTEGER; object: POINTER) is
1789 -- Store object structure reachable form current object
1790 -- in file pointer `file_ptr'.
1791 external
1792 "C signature (EIF_INTEGER, EIF_REFERENCE) use %"eif_store.h%""
1793 alias
1794 "sstore"
1795 end
1796
1797 feature {NONE} -- Inapplicable
1798
1799 go_to (r: CURSOR) is
1800 -- Move to position marked `r'.
1801 do
1802 end
1803
1804 replace (v: like item) is
1805 -- Replace current item by `v'.
1806 require else
1807 is_writable: file_writable
1808 do
1809 ensure then
1810 item = v
1811 count = old count
1812 end
1813
1814 remove is
1815 -- Remove current item.
1816 do
1817 end
1818
1819 prune (v: like item) is
1820 -- Remove an occurrence of `v' if any.
1821 do
1822 ensure then
1823 count <= old count
1824 end
1825
1826 feature {FILE} -- Implementation
1827
1828 mode: INTEGER
1829 -- Input-output mode
1830
1831 Closed_file: INTEGER is 0
1832 Read_file: INTEGER is 1
1833 Write_file: INTEGER is 2
1834 Append_file: INTEGER is 3
1835 Read_Write_file: INTEGER is 4
1836 Append_Read_file: INTEGER is 5
1837
1838 set_read_mode is
1839 -- Define file mode as read.
1840 do
1841 mode := Read_file
1842 end
1843
1844 set_write_mode is
1845 -- Define file mode as write.
1846 do
1847 mode := Write_file
1848 end
1849
1850 platform_indicator: PLATFORM is
1851 -- Platform indicator
1852 once
1853 create Result
1854 end
1855
1856 invariant
1857
1858 valid_mode: Closed_file <= mode and mode <= Append_read_file
1859 name_exists: name /= Void
1860 name_not_empty: not name.is_empty
1861
1862 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23