blob: 8ba9ae10494c2faf53c690b463c97996ed6f599c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id$ *)
open Gallina_lexer
let vfiles = ref ([] : string list)
let option_moins = ref false
let option_stdout = ref false
let traite_fichier f =
try
let chan_in = open_in (f^".v") in
let buf = Lexing.from_channel chan_in in
if not !option_stdout then chan_out := open_out (f ^ ".g");
try
while true do Gallina_lexer.action buf done
with Fin_fichier -> begin
flush !chan_out;
close_in chan_in;
if not !option_stdout then close_out !chan_out
end
with Sys_error _ ->
()
let traite_stdin () =
try
let buf = Lexing.from_channel stdin in
try
while true do Gallina_lexer.action buf done
with Fin_fichier ->
flush !chan_out
with Sys_error _ ->
()
let gallina () =
let lg_command = Array.length Sys.argv in
if lg_command < 2 then begin
output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n";
flush stderr;
exit 1
end;
let treat = function
| "-" -> option_moins := true
| "-stdout" -> option_stdout := true
| "-nocomments" -> comments := false
| f ->
if Filename.check_suffix f ".v" then
vfiles := (Filename.chop_suffix f ".v") :: !vfiles
in
Array.iter treat Sys.argv;
if !option_moins then
traite_stdin ()
else
List.iter traite_fichier !vfiles
let _ = Printexc.catch gallina ()
|
