diff options
| -rw-r--r-- | ide/coq.ml | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | toplevel/line_oriented_parser.ml | 29 | ||||
| -rw-r--r-- | toplevel/line_oriented_parser.mli | 13 | ||||
| -rw-r--r-- | toplevel/protectedtoplevel.ml | 176 | ||||
| -rw-r--r-- | toplevel/protectedtoplevel.mli | 26 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 23 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacinterp.ml | 1 |
10 files changed, 5 insertions, 269 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index ea3400f2e..67cf70a3b 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -520,8 +520,6 @@ let print_toplevel_error exc = in match exc with | End_of_input -> str "Please report: End of input",None - | Vernacexpr.ProtectedLoop -> - str "ProtectedLoop not allowed by coqide!",None | Vernacexpr.Drop -> str "Drop is not allowed by coqide!",None | Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None | _ -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 89d06d2dd..cb7507d9c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -586,7 +586,6 @@ GEXTEND Gram (* Toplevel control *) | IDENT "Drop" -> VernacToplevelControl Drop - | IDENT "ProtectedLoop" -> VernacToplevelControl ProtectedLoop | IDENT "Quit" -> VernacToplevelControl Quit | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; diff --git a/toplevel/line_oriented_parser.ml b/toplevel/line_oriented_parser.ml deleted file mode 100644 index a9dcff3e7..000000000 --- a/toplevel/line_oriented_parser.ml +++ /dev/null @@ -1,29 +0,0 @@ -(************************************************************************) -(* 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$ *) - -let line_oriented_channel_to_option stop_string input_channel = - let count = ref 0 in - let buff = ref "" in - let current_length = ref 0 in - fun i -> - if (i - !count) >= !current_length then begin - count := !count + !current_length + 1; - buff := input_line input_channel; - if !buff = stop_string then - None - else begin - current_length := String.length !buff; - Some '\n' - end - end else - Some (String.get !buff (i - !count)) - -let flush_until_end_of_stream char_stream = - Stream.iter (function _ -> ()) char_stream diff --git a/toplevel/line_oriented_parser.mli b/toplevel/line_oriented_parser.mli deleted file mode 100644 index 8ad0b2fde..000000000 --- a/toplevel/line_oriented_parser.mli +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) - -(*i $Id$ i*) - -val line_oriented_channel_to_option: string -> in_channel -> int -> char option - -val flush_until_end_of_stream : 'a Stream.t -> unit diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml deleted file mode 100644 index 7abb68eea..000000000 --- a/toplevel/protectedtoplevel.ml +++ /dev/null @@ -1,176 +0,0 @@ -(************************************************************************) -(* 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 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) - | DuringSyntaxChecking(a,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) - | DuringSyntaxChecking(loc, e) -> - explain_and_restart e - | e -> explain_and_restart e in - begin - msgnl (str "Starting Centaur Specialized loop"); - looprec input_chan - end diff --git a/toplevel/protectedtoplevel.mli b/toplevel/protectedtoplevel.mli deleted file mode 100644 index 8be663966..000000000 --- a/toplevel/protectedtoplevel.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) - -(*i $Id$ i*) - -(*i*) -open Pp -(*i*) - -(* A protected toplevel (used in Pcoq). *) - -val break_happened : bool ref -val global_request_id : int ref -val output_results_nl : std_ppcmds -> unit -val rearm_break : unit -> unit -val check_break : unit -> unit -val set_acknowledge_command : (int -> int -> exn option -> std_ppcmds) -> unit -val set_start_marker : string -> unit -val set_end_marker : string -> unit -val parse_one_command_group : in_channel -> unit -val protected_loop : in_channel -> unit diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index b57b9c1eb..baa63bc35 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -15,7 +15,6 @@ open Cerrors open Vernac open Vernacexpr open Pcoq -open Protectedtoplevel (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -307,8 +306,6 @@ let print_toplevel_error exc = | Vernacexpr.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise Vernacexpr.Drop; (str"Error: There is no ML toplevel." ++ fnl ()) - | Vernacexpr.ProtectedLoop -> - raise Vernacexpr.ProtectedLoop | Vernacexpr.Quit -> raise Vernacexpr.Quit | _ -> @@ -369,30 +366,20 @@ let do_vernac () = * Ctrl-C will raise the exception Break instead of aborting Coq. * Here we catch the exceptions terminating the Coq loop, and decide * if we really must quit. - * The boolean value is used to choose between a protected loop, which - * we think is more suited for communication with other programs, or - * plain communication. *) + *) -let rec coq_switch b = +let rec loop () = Sys.catch_break true; (* ensure we have a command separator object (DOT) so that the first command can be reseted. *) Lib.mark_end_of_command(); try - if b then begin - reset_input_buffer stdin top_buffer; - while true do do_vernac() done - end else - protected_loop stdin + reset_input_buffer stdin top_buffer; + while true do do_vernac() done with | Vernacexpr.Drop -> () - | Vernacexpr.ProtectedLoop -> - Lib.declare_initial_state(); - coq_switch false | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 | Vernacexpr.Quit -> exit 0 | e -> msgerrnl (str"Anomaly. Please report."); - coq_switch b - -let loop () = coq_switch true + loop () diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index daca81757..4c229d168 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -18,8 +18,6 @@ Mltop Vernacentries Whelp Vernac -Line_oriented_parser -Protectedtoplevel Toplevel Usage Coqinit diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 74974c9d1..d0ee9d39c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -18,7 +18,6 @@ open Decl_kinds open Ppextend (* Toplevel control exceptions *) -exception ProtectedLoop exception Drop exception Quit diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 211d20d39..0924e519b 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -62,7 +62,6 @@ let call (opn,converted_args) = hunk() with | Drop -> raise Drop - | ProtectedLoop -> raise ProtectedLoop | e -> if !Flags.debug then msgnl (str"Vernac Interpreter " ++ str !loc); |