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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 91477 - (hide annotations)
Sun Jan 14 09:47:13 2007 UTC (13 years, 1 month ago) by ericb
File size: 42468 byte(s)
Synchronized with ISE 6.0.65740
1 manus_eiffel 91424 indexing
2     description:
3     "Sequential files, viewed as persistent sequences of characters"
4 manus_eiffel 91434 library: "Free implementation of ELKS library"
5 ericb 91466 copyright: "Copyright (c) 1986-2006, Eiffel Software and others"
6 manus_eiffel 91434 license: "Eiffel Forum License v2 (see forum.txt)"
7 manus_eiffel 91424 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 ericb 91466 -- ASCII code of character following last word read
173 manus_eiffel 91424
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 ericb 91477 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 manus_eiffel 91424 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 ericb 91466 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 manus_eiffel 91424 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 ericb 91477 new_name_not_empty: not new_name.is_empty
1093 manus_eiffel 91424 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 ericb 91475
1207 manus_eiffel 91424 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 ericb 91466 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 ericb 91477 bytes_read := file_gss (file_pointer, p.item + start_pos, nb_bytes)
1384 ericb 91466 end
1385    
1386 manus_eiffel 91424 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 ericb 91475 ensure
1429     last_string_not_void: last_string /= Void
1430 manus_eiffel 91424 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 ericb 91466 "C signature (char *, char *) use %"eif_file.h%""
1537 manus_eiffel 91424 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 ericb 91466 "C signature (char *, int, FILE *): EIF_POINTER use %"eif_file.h%""
1563 manus_eiffel 91424 end
1564    
1565     file_close (file: POINTER) is
1566     -- Close `file'.
1567     external
1568 ericb 91466 "C signature (FILE *) use %"eif_file.h%""
1569 manus_eiffel 91424 end
1570    
1571     file_flush (file: POINTER) is
1572     -- Flush `file'.
1573     external
1574 ericb 91466 "C signature (FILE *) use %"eif_file.h%""
1575 manus_eiffel 91424 end
1576    
1577     file_fd (file: POINTER): INTEGER is
1578     -- Operating system's file descriptor
1579     external
1580 ericb 91466 "C signature (FILE *): EIF_INTEGER use %"eif_file.h%""
1581 manus_eiffel 91424 end
1582    
1583     file_gc (file: POINTER): CHARACTER is
1584     -- Access the next character
1585     external
1586 ericb 91466 "C signature (FILE *): EIF_CHARACTER use %"eif_file.h%""
1587 manus_eiffel 91424 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 ericb 91466 "C signature (FILE *, char *, EIF_INTEGER, EIF_INTEGER): EIF_INTEGER use %"eif_file.h%""
1596 manus_eiffel 91424 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 ericb 91466 "C signature (FILE *, char *, EIF_INTEGER): EIF_INTEGER use %"eif_file.h%""
1604 manus_eiffel 91424 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 ericb 91466 "C signature (FILE *, char *, EIF_INTEGER, EIF_INTEGER): EIF_INTEGER use %"eif_file.h%""
1615 manus_eiffel 91424 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 ericb 91466 "C signature (FILE *): EIF_CHARACTER use %"eif_file.h%""
1622 manus_eiffel 91424 end
1623    
1624     file_size (file: POINTER): INTEGER is
1625     -- Size of `file'
1626     external
1627 ericb 91466 "C signature (FILE *): EIF_INTEGER use %"eif_file.h%""
1628     alias
1629     "eif_file_size"
1630 manus_eiffel 91424 end
1631    
1632     file_tnil (file: POINTER) is
1633     -- Read upto next input line.
1634     external
1635 ericb 91466 "C signature (FILE *) use %"eif_file.h%""
1636 manus_eiffel 91424 end
1637    
1638     file_tell (file: POINTER): INTEGER is
1639     -- Current cursor position in file.
1640     external
1641 ericb 91466 "C signature (FILE *): EIF_INTEGER use %"eif_file.h%""
1642 manus_eiffel 91424 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 ericb 91466 "C signature (FILE *) use %"eif_file.h%""
1693 manus_eiffel 91424 end
1694    
1695     file_append (file, from_file: POINTER; length: INTEGER) is
1696     -- Append a copy of `from_file' to `file'
1697     external
1698 ericb 91466 "C signature (FILE *, FILE *, EIF_INTEGER) use %"eif_file.h%""
1699 manus_eiffel 91424 end
1700    
1701     file_ps (file: POINTER; a_string: POINTER; length: INTEGER) is
1702     -- Print `a_string' to `file'.
1703     external
1704 ericb 91466 "C signature (FILE *, char *, EIF_INTEGER) use %"eif_file.h%""
1705 manus_eiffel 91424 end
1706    
1707     file_pc (file: POINTER; c: CHARACTER) is
1708     -- Put `c' to end of `file'.
1709     external
1710 ericb 91466 "C signature (FILE *, EIF_CHARACTER) use %"eif_file.h%""
1711 manus_eiffel 91424 end
1712    
1713     file_go (file: POINTER; abs_position: INTEGER) is
1714     -- Go to absolute `position', originated from start.
1715     external
1716 ericb 91466 "C signature (FILE *, EIF_INTEGER) use %"eif_file.h%""
1717 manus_eiffel 91424 end
1718    
1719     file_recede (file: POINTER; abs_position: INTEGER) is
1720     -- Go to absolute `position', originated from end.
1721     external
1722 ericb 91466 "C signature (FILE *, EIF_INTEGER) use %"eif_file.h%""
1723 manus_eiffel 91424 end
1724    
1725     file_move (file: POINTER; offset: INTEGER) is
1726     -- Move file pointer by `offset'.
1727     external
1728 ericb 91466 "C signature (FILE *, EIF_INTEGER) use %"eif_file.h%""
1729 manus_eiffel 91424 end
1730    
1731     file_feof (file: POINTER): BOOLEAN is
1732     -- End of file?
1733     external
1734 ericb 91466 "C signature (FILE *): EIF_BOOLEAN use %"eif_file.h%""
1735 manus_eiffel 91424 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 ericb 91466 "C use %"eif_retrieve.h%""
1766 manus_eiffel 91424 alias
1767     "eretrieve"
1768     end
1769 ericb 91475
1770 manus_eiffel 91424 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 ericb 91475
1779 manus_eiffel 91424 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 ericb 91475
1788 manus_eiffel 91424 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 ericb 91475
1850 ericb 91466 platform_indicator: PLATFORM is
1851     -- Platform indicator
1852     once
1853     create Result
1854     end
1855 manus_eiffel 91424
1856     invariant
1857 ericb 91466
1858 manus_eiffel 91424 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 manus_eiffel 91438 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23