Migration of ProtectedToplevel and Line_oriented_parser into new contrib Interface

 the ProtectedLoop feature was used only by CoqInterface.
 Idem for stuff in Line_oriented_parser

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12573 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 18 deletions

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 ()