summaryrefslogtreecommitdiff
path: root/toplevel/protectedtoplevel.ml
blob: caf323053d5a0b6055b06d8ca165d826cd4d62ff (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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
(************************************************************************)
(*  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: protectedtoplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)

open Pp
open Line_oriented_parser
open Vernac
open Vernacexpr

(* The toplevel parsing loop we propose here is more robust to printing
   errors.  The philosophy is that all commands should be individually wrapped
   in predefined markers.  If there is a parsing error, everything down to
   the closing marker will be discarded.  Also there is always an aknowledge
   message associated to a wrapped command. *)


(* It is also possible to have break signals sent by other programs.  However,
   there are some operations that should not be interrupted, especially, those
   operations that are outputing data.
*)

let break_happened = ref false

(* Before outputing any data, output_results makes sure that no interrupt 
   is going to disturb the process. *)
let output_results_nl stream =
    let _ = Sys.signal Sys.sigint
       (Sys.Signal_handle(fun i -> break_happened := true;()))
  in
  msgnl stream

let rearm_break () =
  let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun _ -> raise Sys.Break)) in 
    ()

let check_break () =
  if !break_happened then begin
    break_happened := false;
    raise Sys.Break
  end

(* All commands are acknowledged. *)

let global_request_id = ref 013

let acknowledge_command_ref =
   ref(fun request_id command_count opt_exn
      -> (fnl () ++ str "acknowledge command number " ++
           int request_id ++ fnl () ++ 
         str "successfully executed " ++ int command_count ++ fnl () ++
           str "error message" ++ fnl () ++
         (match opt_exn with
           Some e -> Cerrors.explain_exn e
         | None -> (mt ())) ++ fnl () ++
         str "E-n-d---M-e-s-s-a-g-e" ++ fnl ()))

let set_acknowledge_command f =
  acknowledge_command_ref := f

let acknowledge_command request_id = !acknowledge_command_ref request_id

(* The markers are chosen to be likely to be different from any existing text. *)

let start_marker = ref "protected_loop_start_command"
let end_marker = ref "protected_loop_end_command"
let start_length = ref (String.length !start_marker)
let start_marker_buffer = ref (String.make !start_length ' ')

let set_start_marker s =
  start_marker := s;
  start_length := String.length s;
  start_marker_buffer := String.make !start_length ' '
    
let set_end_marker s =
  end_marker := s

exception E_with_rank of int * exn

let rec parse_one_command_group input_channel =
  let count = ref 0 in
  let this_line = input_line input_channel in
  if (String.length this_line) >= !start_length then begin
    String.blit this_line 0 !start_marker_buffer 0 !start_length;
    if !start_marker_buffer = !start_marker then
      let req_id_line = input_line input_channel in
      	begin 
	  (try
            global_request_id := int_of_string req_id_line
	  with
            | e -> failwith ("could not parse the request identifier |"^
                             req_id_line ^ "|")) ;
	  let count_line = input_line input_channel in
	    begin
	      (try
		count := int_of_string count_line
	      with
		| e -> failwith("could not parse the count|" ^ count_line
				^ "|"));
	      let stream_tail =
	      	Stream.from
		  (line_oriented_channel_to_option
		     !end_marker input_channel) in
	      	begin
		  check_break();
		  rearm_break();
		  let rec execute_n_commands rank =
		    if rank = !count then
		      None
		    else
		      let first_cmd_status =
                      	try 
			  raw_do_vernac
			    (Pcoq.Gram.parsable stream_tail);
		      	None
		      	with e -> Some(rank,e) in
		      	match first_cmd_status with
			    None ->
			      execute_n_commands (rank + 1)
			  | v -> v in
		  let r = execute_n_commands 0 in
		    (match r with
			 None ->
			   output_results_nl 
			     (acknowledge_command
			      	!global_request_id !count None)
		       | Some(rank, e) ->
			   (match e with 
                    	     | DuringCommandInterp(a,e1)
			     | Stdpp.Exc_located (a,DuringSyntaxChecking e1) ->
				  output_results_nl
				    (acknowledge_command
				       !global_request_id rank (Some e1))
			      | e -> 
				  output_results_nl
				    (acknowledge_command
				       !global_request_id rank (Some e))));
		    rearm_break();
		    flush_until_end_of_stream stream_tail
	      	end
	    end
	end
    else
      parse_one_command_group input_channel
  end else
    parse_one_command_group input_channel

let protected_loop input_chan =
  let rec explain_and_restart e =
    begin
      output_results_nl(Cerrors.explain_exn e);
      rearm_break();
      looprec input_chan;
    end
  and looprec input_chan =
    try 
      while true do parse_one_command_group input_chan done
    with
      | Vernacexpr.Drop -> raise Vernacexpr.Drop
      | Vernacexpr.Quit -> exit 0
      | End_of_file -> exit 0
      | DuringCommandInterp(loc, Vernacexpr.Quit) -> raise Vernacexpr.Quit
      | DuringCommandInterp(loc, Vernacexpr.Drop) -> raise Vernacexpr.Drop
      | DuringCommandInterp(loc, e)
      | Stdpp.Exc_located (loc,DuringSyntaxChecking e) ->
	  explain_and_restart e
      | e -> explain_and_restart e in
    begin
      msgnl (str "Starting Centaur Specialized loop");
      looprec input_chan
    end