retablissement du toplevel

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

11 files changed, 1122 insertions, 0 deletions

diff --git a/toplevel/errors.ml b/toplevel/errors.ml
new file mode 100644
index 000000000..1de6348ec
--- /dev/null
+++ b/toplevel/errors.ml
@@ -0,0 +1,64 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Ast
+
+let print_loc loc =
+  if loc = dummy_loc then 
+    [< 'sTR"<unknown>" >]
+  else 
+    [< 'iNT (fst loc); 'sTR"-"; 'iNT (snd loc) >]
+
+let guill s = "\""^s^"\""
+
+let where s =
+  if !Options.debug then  [< 'sTR"in "; 'sTR s; 'sTR":"; 'sPC >] else [<>]
+
+(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
+
+let rec explain_exn_default = function
+  | Stream.Failure -> [< 'sTR"Error: uncaught Parse.Failure." >]
+  | Stream.Error txt -> hOV 0 [< 'sTR"Syntax error: "; 'sTR txt >]
+  | Token.Error txt -> hOV 0 [< 'sTR"Lexer error: "; 'sTR txt >]
+  | Sys_error msg -> hOV 0 [< 'sTR"OS error: " ; 'sTR msg >]
+  | UserError(s,pps) -> hOV 1 [< 'sTR"Error: "; where s; pps >]
+	
+  | Out_of_memory -> [< 'sTR"Out of memory" >]
+  | Stack_overflow -> [< 'sTR"Stack overflow" >]
+	  
+  | Ast.No_match s -> hOV 0 [< 'sTR"Ast matching error : "; 'sTR s >]
+	
+  | Anomaly (s,pps) -> hOV 1 [< 'sTR"System Anomaly: "; where s; pps >]
+	  
+  | Match_failure(filename,pos1,pos2) ->
+      hOV 1 [< 'sTR"Match failure in file " ;
+	       'sTR filename ; 'sTR " from char #" ;
+	       'iNT pos1 ; 'sTR " to #" ; 'iNT pos2 >]
+
+  | Not_found -> [< 'sTR"Search error." >]
+
+  | Failure s -> hOV 0 [< 'sTR "System Error (Failure): " ; 'sTR (guill s) >]
+
+  | Invalid_argument s -> hOV 0 [< 'sTR"Invalid argument: " ; 'sTR (guill s) >]
+
+  | Sys.Break -> hOV 0 [< 'fNL; 'sTR"User Interrupt." >]
+
+  | Stdpp.Exc_located (loc,exc) ->
+      hOV 0 [< if loc = Ast.dummy_loc then [<>]
+               else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
+               explain_exn_default exc >]
+	
+  | reraise ->
+      flush_all();
+      (try Printexc.print raise reraise with _ -> ());
+      flush_all();
+      [< 'sTR "Please report." >]
+
+let raise_if_debug e =
+  if !Options.debug then raise e
+
+let explain_exn_function = ref explain_exn_default
+
+let explain_exn e = !explain_exn_function e
diff --git a/toplevel/errors.mli b/toplevel/errors.mli
new file mode 100644
index 000000000..4f6a1a074
--- /dev/null
+++ b/toplevel/errors.mli
@@ -0,0 +1,17 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+(*i*)
+
+(* Error report. *)
+
+val print_loc : Coqast.loc -> std_ppcmds
+
+val explain_exn : exn -> std_ppcmds
+
+val explain_exn_function : (exn -> std_ppcmds) ref
+val explain_exn_default : exn -> std_ppcmds
+
+val raise_if_debug : exn -> unit
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
new file mode 100644
index 000000000..b96d57a7d
--- /dev/null
+++ b/toplevel/mltop.ml
@@ -0,0 +1,269 @@
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Libobject
+open Library
+open System
+open Vernacinterp
+
+(* Code to hook Coq into the ML toplevel -- depends on having the
+   objective-caml compiler mostly visible. The functions implemented here are:
+   \begin{itemize}
+   \item [dir_ml_load name]: Loads the ML module fname from the current ML 
+     path. 
+   \item [dir_ml_use]: Directive #use of Ocaml toplevel
+   \item [dir_ml_dir]: Directive #directory of Ocaml toplevel
+   \end{itemize}
+ 
+   How to build an ML module interface with these functions.
+   The idea is that the ML directory path is like the Coq directory
+   path.  So we can maintain the two in parallel.
+   In the same way, we can use the "ml_env" as a kind of ML
+   environment, which we freeze, unfreeze, and add things to just like
+   to the other environments.
+   Finally, we can create an object which is an ML module, and require
+   that the "caching" of the ML module cause the loading of the
+   associated ML file, if that file has not been yet loaded.  Of
+   course, the problem is how to record dependences between ML
+   modules.
+   (I do not know of a solution to this problem, other than to
+   put all the needed names into the ML Module object.) *)
+
+(* This path is where we look for .cmo *)
+let coq_mlpath_copy = ref []
+let keep_copy_mlpath s = coq_mlpath_copy := (glob s)::!coq_mlpath_copy
+
+(* If there is a toplevel under Coq *)
+type toplevel = { 
+  load_obj : string -> unit;
+  use_file : string -> unit;
+  add_dir  : string -> unit }
+
+(* Determines the behaviour of Coq with respect to ML files (compiled 
+   or not) *)
+type kind_load =
+  | WithTop of toplevel
+  | WithoutTop
+  | Native
+
+(* Must be always initialized *)
+let load = ref Native
+
+(* Sets and initializes the kind of loading *)
+let set kload = load := kload
+
+(* Resets load *)
+let remove ()= load :=N ative
+
+(* Tests if an Ocaml toplevel runs under Coq *)
+let is_ocaml_top () =
+  match !load with
+    | WithTop _ -> true
+    |_ -> false
+
+(* Tests if we can load ML files *)
+let enable_load () =
+  match !load with
+    | WithTop _ | WithoutTop -> true
+    |_ -> false
+
+(* Dynamic loading of .cmo *)
+let dir_ml_load s = 
+  match !load with
+    | WithTop t -> 
+	if is_in_path !coq_mlpath_copy s then
+          try t.load_obj s
+          with
+            | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u
+            | _ -> errorlabstrm "Mltop.load_object"
+                  [< 'sTR"Cannot link ml-object "; 'sTR s;
+		     'sTR" to Coq code." >]
+	else 
+	  errorlabstrm "Mltop.load_object"
+            [< 'sTR"File not found on loadpath : "; 'sTR s >]
+    | WithoutTop ->
+	if is_in_path !coq_mlpath_copy s then
+          let gname = where_in_path !coq_mlpath_copy s in
+          try
+            Dynlink.loadfile gname;
+	    Dynlink.add_interfaces 
+	      [(String.capitalize (Filename.chop_suffix
+				     (Filename.basename gname) ".cmo"))] 
+	      [Filename.dirname gname]
+	  with
+	    | Dynlink.Error(a) ->
+		errorlabstrm "Mltop.load_object"
+                  [< 'sTR (Dynlink.error_message a) >]
+	else errorlabstrm "Mltop.load_object"
+          [< 'sTR"File not found on loadpath : "; 'sTR s >]
+    | Native ->
+	errorlabstrm "Mltop.no_load_object"
+          [< 'sTR"Loading of ML object file forbidden in a native Coq" >]
+
+(* Dynamic interpretation of .ml *)
+let dir_ml_use s =
+  match !load with
+    | WithTop t -> t.use_file s
+    | _ -> warning "Cannot access the ML compiler"
+
+(* Adds a path to the ML paths *)
+let dir_ml_dir s =
+  match !load with
+    | WithTop t -> t.add_dir s; keep_copy_mlpath s
+    | WithoutTop -> keep_copy_mlpath s
+    | _ -> ()
+
+(* For Rec Add ML Path *)
+let rdir_ml_dir dir=
+  List.iter dir_ml_dir (alldir dir)
+
+(* convertit un nom quelconque en nom de fichier ou de module *) 
+let mod_of_name name =
+  let base =
+    if Filename.check_suffix name ".cmo" then
+      Filename.chop_suffix name ".cmo"
+    else 
+      name
+  in 
+  String.capitalize base
+
+let file_of_name name = make_suffix (String.uncapitalize name) ".cmo"
+
+(* TODO: supprimer ce hack, si possible *)
+(* Initialisation of ML modules that need the state (ex: tactics like
+ * natural, omega ...)
+ * Each module may add some inits (function of type unit -> unit).
+ * These inits are executed right after the initial state loading if the
+ * module is statically linked, or after the loading if it is required. *)
+
+let init_list = ref ([] : (unit -> unit) list)
+
+let add_init_with_state init_fun =
+  init_list := init_fun :: !init_list
+
+let init_with_state () =
+  List.iter (fun f -> f()) (List.rev !init_list); init_list := []
+
+
+(* known_loaded_module contains the names of the loaded ML modules
+ * (linked or loaded with load_object). It is used not to loaded a 
+ * module twice. It is NOT the list of ML modules Coq knows. *)
+
+type ml_module_object = { mnames : string list }
+
+let known_loaded_modules = ref ([] : string list)
+
+let add_known_module mname =
+  known_loaded_modules := add_set mname !known_loaded_modules
+
+let module_is_known mname = List.mem mname !known_loaded_modules
+
+let load_object mname fname=
+  dir_ml_load fname;
+  init_with_state();
+  add_known_module mname
+
+(* Summary of declared ML Modules *)
+
+let loaded_modules = ref ([] : string list)
+let get_loaded_modules () = !loaded_modules
+let add_loaded_module md =
+  loaded_modules := add_set md !loaded_modules
+
+let orig_loaded_modules = ref (get_loaded_modules ())
+let init_ml_modules () = loaded_modules := !orig_loaded_modules
+
+
+let unfreeze_ml_modules x =
+  List.iter
+    (fun name ->
+       let mname = mod_of_name name in
+       if not (module_is_known mname) then
+         if enable_load() then
+           let fname= file_of_name mname in
+           load_object mname fname                
+         else 
+	   errorlabstrm "Mltop.unfreeze_ml_modules"
+             [< 'sTR"Loading of ML object file forbidden in a native Coq" >];
+       add_loaded_module mname)
+    x
+
+let _ = 
+  Summary.declare_summary "ML-MODULES"
+    { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules()));
+      Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x);
+      Summary.init_function = (fun () -> init_ml_modules ()) }
+
+(* Same as restore_ml_modules, but verbosely *)
+
+let cache_ml_module_object {mnames=mnames} =
+  List.iter
+    (fun name ->
+       let mname = mod_of_name name in
+       if not (module_is_known mname) then
+         let fname= file_of_name mname in
+         begin try 
+	   mSG [< 'sTR"[Loading ML file " ; 'sTR fname ; 'sTR" ..." >];
+           load_object mname fname;
+           mSGNL [< 'sTR"done]" >]
+         with e -> 
+	   begin pPNL [< 'sTR"failed]" >]; raise e end
+	 end;
+         add_loaded_module mname)
+    mnames
+
+let specification_ml_module_object x = x
+					 
+let (inMLModule,outMLModule) =
+  declare_object ("ML-MODULE",
+                  { load_function = cache_ml_module_object;
+                    cache_function = (fun _ -> ());
+                    specification_function = specification_ml_module_object })
+
+let declare_ml_modules l =
+  add_anonymous_object (inMLModule {mnames=l})
+    
+let print_ml_path () =
+  let l = !coq_mlpath_copy in
+  pPNL [< 'sTR"ML Load Path:"; 'fNL; 'sTR"  ";
+          hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >]
+
+let _ = vinterp_add "DeclareMLModule"
+	  (fun l ->
+	     let sl = List.map 
+			(function (VARG_STRING s) -> s 
+			   | _ -> anomaly "DeclareMLModule : not a string") 
+			l
+	     in
+    	     fun () -> declare_ml_modules sl)
+	  
+let _ = vinterp_add "AddMLPath"
+	  (function 
+	     | [VARG_STRING s] ->
+		 (fun () -> dir_ml_dir (glob s))
+	     | _ -> anomaly "AddMLPath : not a string")
+
+let _ = vinterp_add "RecAddMLPath"
+	  (function 
+	     | [VARG_STRING s] ->
+		 (fun () -> rdir_ml_dir (glob s))
+	     | _ -> anomaly "RecAddMLPath : not a string")
+
+let _ = vinterp_add "PrintMLPath"
+	  (function 
+	     | [] -> (fun () -> print_ml_path ())
+	     | _ -> anomaly "PrintMLPath : does not expect any argument")
+
+	  (* Printing of loaded ML modules *)
+	  
+let print_ml_modules () =
+  let l = get_loaded_modules () in
+  pP [< 'sTR"Loaded ML Modules : " ;
+        hOV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >]
+
+let _ = vinterp_add "PrintMLModules"
+	  (function 
+	     | [] -> (fun () -> print_ml_modules ())
+	     | _ -> anomaly "PrintMLModules : does not expect an argument")
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
new file mode 100644
index 000000000..72f9d3aa8
--- /dev/null
+++ b/toplevel/mltop.mli
@@ -0,0 +1,59 @@
+
+(* $Id$ *)
+
+(* If there is a toplevel under Coq *)
+type toplevel = {
+  load_obj : string -> unit;
+  use_file : string -> unit;
+  add_dir : string -> unit }
+
+(* Determines the behaviour of Coq with respect to ML files (compiled 
+   or not) *) 
+type kind_load=
+  | WithTop of toplevel
+  | WithoutTop
+  | Native
+
+(*Sets and initializes the kind of loading*)
+val set : kind_load -> unit
+
+(*Resets the kind of loading*)
+val remove : unit -> unit
+
+(*Tests if an Ocaml toplevel runs under Coq*)
+val is_ocaml_top : unit -> bool
+
+(*Tests if we can load ML files*)
+val enable_load : unit -> bool
+
+(*Dynamic loading of .cmo*)
+val dir_ml_load : string -> unit
+
+(*Dynamic interpretation of .ml*)
+val dir_ml_use : string -> unit
+
+(*Adds a path to the ML paths*)
+val dir_ml_dir : string -> unit
+
+val add_init_with_state : (unit -> unit) -> unit
+val init_with_state : unit -> unit
+
+(* List of modules linked to the toplevel *)
+val add_known_module : string -> unit
+val module_is_known : string -> bool
+val load_object : string -> string -> unit
+
+(* Summary of Declared ML Modules *)
+val get_loaded_modules : unit -> string list
+val add_loaded_module : string -> unit
+val init_ml_modules : unit -> unit
+val unfreeze_ml_modules : string list -> unit
+
+type ml_module_object = { mnames: string list }
+val inMLModule : ml_module_object -> Libobject.obj
+val outMLModule : Libobject.obj -> ml_module_object
+
+val declare_ml_modules : string list -> unit
+val print_ml_path : unit -> unit
+
+val print_ml_modules : unit -> unit
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
new file mode 100644
index 000000000..7af6dcc89
--- /dev/null
+++ b/toplevel/protectedtoplevel.ml
@@ -0,0 +1,134 @@
+
+(* $Id$ *)
+
+open Pp
+open Vernac
+
+(* 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
+
+let output_results_nl stream =
+  let _ = 
+    Sys.signal Sys.sigint
+      (Sys.Signal_handle (fun _ -> 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 request_id =
+  [< 'fNL; 'sTR "message"; 'fNL; 'sTR "acknowledge"; 'fNL; 
+     'iNT request_id; 'fNL; 'sTR "***"; 'fNL >]
+
+(* 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
+
+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
+
+let rec parse_one_command input_channel =
+  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 snd_line = input_line input_channel in
+      begin 
+	try
+          global_request_id := int_of_string snd_line
+	with
+          | e -> failwith ("could not parse the request identifier |"^
+                           snd_line ^ "|") 
+      end;
+      let stream_tail =
+        Stream.from
+          (line_oriented_channel_to_option !end_marker input_channel) in
+      begin
+	try
+	  check_break();
+          rearm_break();
+          raw_do_vernac (Pcoq.Gram.parsable stream_tail);
+          output_results_nl(acknowledge_command !global_request_id);
+          rearm_break();
+        with
+          | e -> begin flush_until_end_of_stream stream_tail; raise e end
+      end;
+      flush_until_end_of_stream stream_tail
+    else
+      parse_one_command input_channel
+  end else
+    parse_one_command input_channel
+
+let protected_loop input_chan =
+  let rec explain_and_restart e =
+    output_results_nl(Errors.explain_exn e);
+    rearm_break();
+    looprec input_chan;
+  and looprec input_chan =
+    try 
+      while true do parse_one_command input_chan done
+    with
+      | Vernacinterp.Drop -> raise Vernacinterp.Drop
+      | Vernacinterp.Quit -> exit 0
+      | End_of_file -> exit 0
+      | DuringCommandInterp(loc, Vernacinterp.Quit) -> raise Vernacinterp.Quit
+      | DuringCommandInterp(loc, Vernacinterp.Drop) -> raise Vernacinterp.Drop
+      | DuringCommandInterp(loc, e) ->
+	  explain_and_restart e
+      | e -> explain_and_restart e 
+  in
+  mSGNL [<'sTR "Starting Centaur Specialized loop" >];
+  looprec input_chan
diff --git a/toplevel/protectedtoplevel.mli b/toplevel/protectedtoplevel.mli
new file mode 100644
index 000000000..c09fac3e0
--- /dev/null
+++ b/toplevel/protectedtoplevel.mli
@@ -0,0 +1,17 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+(*i*)
+
+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 acknowledge_command : int -> std_ppcmds
+val set_start_marker : string -> unit
+val set_end_marker : string -> unit
+val parse_one_command : in_channel -> unit
+val protected_loop : in_channel -> unit
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
new file mode 100644
index 000000000..dcad19bed
--- /dev/null
+++ b/toplevel/toplevel.ml
@@ -0,0 +1,298 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Options
+open Errors
+open Vernac
+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. *)
+
+type input_buffer = { 
+  mutable prompt : unit -> string;
+  mutable str : string; (* buffer of already read characters *)
+  mutable len : int;    (* number of chars in the buffer *)
+  mutable bols : int list; (* offsets in str of begining of lines *)
+  mutable tokens : Gram.parsable; (* stream of tokens *)
+  mutable start : int } (* stream count of the first char of the buffer *)
+
+(* Double the size of the buffer. *)
+
+let resize_buffer ibuf =
+  let nstr = String.create (2 * String.length ibuf.str + 1) in
+  String.blit ibuf.str 0 nstr 0 (String.length ibuf.str);
+  ibuf.str <- nstr
+
+(* Delete all irrelevent lines of the input buffer. Keep the last line
+   in the buffer (useful when there are several commands on the same line. *)
+
+let resynch_buffer ibuf =
+  match ibuf.bols with
+    | ll::_ ->
+        let new_len = ibuf.len - ll in
+        String.blit ibuf.str ll ibuf.str 0 new_len;
+        ibuf.len <- new_len;
+        ibuf.bols <- [];
+        ibuf.start <- ibuf.start + ll
+    | _ -> ()
+
+(* Read a char in an input channel, displaying a prompt af every
+   begining of line. *)
+
+let prompt_char ic ibuf count =
+  let bol = match ibuf.bols with
+    | ll::_ -> ibuf.len == ll
+    | [] -> ibuf.len == 0
+  in
+  if bol then mSGERR [< 'sTR (ibuf.prompt()) >];
+  try
+    let c = input_char ic in
+    if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
+    if ibuf.len == String.length ibuf.str then resize_buffer ibuf;
+    ibuf.str.[ibuf.len] <- c;
+    ibuf.len <- ibuf.len + 1;
+    Some c
+  with End_of_file -> 
+    None
+
+(* Reinitialize the char stream (after a Drop) *)
+
+let reset_input_buffer ic ibuf =
+  ibuf.str <- "";
+  ibuf.len <- 0;
+  ibuf.bols <- [];
+  ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf));
+  ibuf.start <- 0
+
+(* Functions to print underlined locations from an input buffer. *)
+
+(* Given a location, returns the list of locations of each line. The last
+   line is returned separately. It also checks the location bounds. *)
+
+let get_bols_of_loc ibuf (bp,ep) =
+  let add_line (b,e) lines =
+    if b < 0 or e < b then anomaly "Bad location";
+    match lines with
+      | ([],None) -> ([], Some (b,e))
+      | (fl,oe) -> ((b,e)::fl, oe) 
+  in
+  let rec lines_rec ba after = function
+    | []                  -> add_line (0,ba) after
+    | ll::_ when ll <= bp -> add_line (ll,ba) after
+    | ll::fl              ->
+        let nafter = if ll < ep then add_line (ll,ba) after else after in
+        lines_rec ll nafter fl 
+  in
+  let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in
+  (fl,out_some ll)
+
+let dotted_location (b,e) =
+  if e-b < 3 then 
+    ("", String.make (e-b) ' ')
+  else 
+    (String.make (e-b-1) '.', " ")
+
+let print_highlight_location ib (bp,ep) =
+  let bp = bp - ib.start 
+  and ep = ep - ib.start in
+  let highlight_lines =
+    match get_bols_of_loc ib (bp,ep) with
+      | ([],(bl,el)) ->  
+	  [< 'sTR"> "; 'sTR(String.sub ib.str bl (el-bl));
+             'sTR"> "; 'sTR(String.make (bp-bl) ' ');
+             'sTR(String.make (ep-bp) '^') >]
+      | ((b1,e1)::ml,(bn,en)) ->
+          let (d1,s1) = dotted_location (b1,bp) in
+          let (dn,sn) = dotted_location (ep,en) in
+          let l1 = [< 'sTR"> "; 'sTR d1; 'sTR s1;
+                      'sTR(String.sub ib.str bp (e1-bp)) >] in
+          let li =
+            prlist (fun (bi,ei) ->
+                      [< 'sTR"> "; 'sTR(String.sub ib.str bi (ei-bi)) >]) ml in
+          let ln = [< 'sTR"> "; 'sTR(String.sub ib.str bn (ep-bn));
+                      'sTR sn; 'sTR dn >] in 
+	  [< l1; li; ln >]
+  in 
+  [< 'sTR"Toplevel input, characters "; Errors.print_loc (bp,ep); 'fNL;
+     highlight_lines; 'fNL >]
+
+(* Functions to report located errors in a file. *)
+
+let print_location_in_file s fname (bp,ep) =
+  let errstrm = [< 'sTR"Error while reading "; 'sTR s; 'sTR" :"; 'fNL;
+                   'sTR"File "; 'sTR ("\""^fname^"\"") >] in
+  if (bp,ep) = Ast.dummy_loc
+  then 
+    [< errstrm; 'sTR", unknown location."; 'fNL >]
+  else
+    let ic = open_in fname in
+    let rec line_of_pos lin bol cnt =
+      if cnt < bp then
+        if input_char ic == '\n'
+        then line_of_pos (lin + 1) (cnt +1) (cnt+1)
+        else line_of_pos lin bol (cnt+1)
+      else (lin, bol)
+    in
+    try
+      let (line, bol) = line_of_pos 1 0 0 in
+      close_in ic;
+      [< errstrm; 'sTR", line "; 'iNT line;
+         'sTR", characters "; Errors.print_loc (bp-bol,ep-bol); 'fNL >]
+    with e -> (close_in ic; [< errstrm; 'sTR", invalid location."; 'fNL >])
+	
+let print_command_location ib dloc =
+  match dloc with
+    | Some (bp,ep) ->
+        [< 'sTR"Error during interpretation of command:"; 'fNL;
+           'sTR(String.sub ib.str (bp-ib.start) (ep-bp)); 'fNL >]
+    | None -> [<>]
+
+let valid_loc dloc (b,e) =
+  (b,e) <> Ast.dummy_loc
+  & match dloc with
+    | Some (bd,ed) -> bd<=b & e<=ed
+    | _ -> true
+	  
+let valid_buffer_loc ib dloc (b,e) =
+  valid_loc dloc (b,e) & b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
+    
+(* A buffer to store the current command read on stdin. It is
+ * initialized when a vernac command is immediately followed by "\n",
+ * or after a Drop. *)
+
+let top_buffer =
+  let pr() = 
+    (Pfedit.proof_prompt())^(emacs_str (String.make 1 (Char.chr 249)))
+  in
+  { prompt = pr;
+    str = "";
+    len = 0;
+    bols = [];
+    tokens = Gram.parsable [<>];
+    start = 0 }
+
+let set_prompt prompt =
+  top_buffer.prompt
+  <- (fun () -> (prompt ()) ^ (emacs_str (String.make 1 (Char.chr 249))))
+
+(* Removes and prints the location of the error. The following exceptions
+   need not be located. *)
+let rec is_pervasive_exn = function
+  | Out_of_memory | Stack_overflow | Sys.Break -> true
+  | Error_in_file (_,_,e) -> is_pervasive_exn e
+  | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
+  | DuringCommandInterp (_,e) -> is_pervasive_exn e
+  | _ -> false
+
+(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
+   May raise only the following exceptions: Drop and End_of_input,
+   meaning we get out of the Coq loop *)
+let print_toplevel_error exc =
+  let (dloc,exc) =
+    match exc with
+      | DuringCommandInterp (loc,ie) ->
+          if loc = Ast.dummy_loc then (None,ie) else (Some loc, ie)
+      | _ -> (None, exc) 
+  in
+  let (locstrm,exc) =
+    match exc with
+      | Stdpp.Exc_located (loc, ie) ->
+          if valid_buffer_loc top_buffer dloc loc then
+            (print_highlight_location top_buffer loc, ie)
+          else 
+	    (print_command_location top_buffer dloc, ie)
+      | Error_in_file (s, (fname, loc), ie) ->
+          (print_location_in_file s fname loc, ie)
+      | _ -> (print_command_location top_buffer dloc, exc)
+  in
+  match exc with
+    | End_of_input -> 
+	mSGERRNL [<>]; pp_flush(); exit 0
+    | Vernacinterp.Drop ->  (* Last chance *)
+        if Mltop.is_ocaml_top() then raise Vernacinterp.Drop;
+        [< 'sTR"There is no ML toplevel."; 'fNL >]
+    | Vernacinterp.ProtectedLoop ->
+	raise Vernacinterp.ProtectedLoop
+    | Vernacinterp.Quit -> 
+	raise Vernacinterp.Quit
+    | _ -> 
+	[< if is_pervasive_exn exc then [<>] else locstrm;
+           Errors.explain_exn exc >]
+
+(* Read the input stream until a dot is encountered *)
+let parse_to_dot =
+  let rec dot = parser
+    | [< '("", ".") >] -> ()
+    | [< '("EOI", "") >] -> raise End_of_input
+    | [< '_; s >] -> dot s
+  in 
+  Gram.Entry.of_parser "Coqtoplevel.dot" dot
+    
+(* We assume that when a lexer error occurs, at least one char was eaten *)
+let rec discard_to_dot () =
+  try 
+    Gram.Entry.parse parse_to_dot top_buffer.tokens
+  with Stdpp.Exc_located(_,Token.Error _) -> 
+    discard_to_dot()
+
+
+(* If the error occured while parsing, we read the input until a dot token
+ * in encountered.
+ *)
+let process_error = function
+  | DuringCommandInterp _ as e -> e
+  | e ->
+      if is_pervasive_exn e then 
+	e
+      else 
+        try 
+	  discard_to_dot (); e 
+	with
+          | End_of_input -> End_of_input
+          | de -> if is_pervasive_exn de then de else e
+
+(* do_vernac reads and executes a toplevel phrase, and print error
+   messages when an exception is raised, except for the following:
+     Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
+           Otherwise, exit.
+     End_of_input: Ctrl-D was typed in, we will quit *)
+let do_vernac () =
+  mSGERRNL [<>];
+  resynch_buffer top_buffer;
+  begin 
+    try 
+      raw_do_vernac top_buffer.tokens
+    with e -> mSGNL (print_toplevel_error (process_error e)) 
+  end;
+  flush_all()
+
+(* coq and go read vernacular expressions until Drop is entered.
+ * 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 =
+  Sys.catch_break true;
+  try
+    if b then begin
+      reset_input_buffer stdin top_buffer;
+      while true do do_vernac() done
+    end else
+      protected_loop stdin
+  with
+    | Vernacinterp.Drop -> ()
+    | Vernacinterp.ProtectedLoop -> coq_switch false
+    | End_of_input -> mSGERRNL [<>]; pp_flush(); exit 0
+    | Vernacinterp.Quit -> exit 0
+    | e ->
+	mSGERRNL [< 'sTR"Anomaly in the toplevel loop. Please report." >];
+	coq_switch b
+
+let loop () = coq_switch true
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
new file mode 100644
index 000000000..3d04fc625
--- /dev/null
+++ b/toplevel/toplevel.mli
@@ -0,0 +1,39 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Pcoq
+(*i*)
+
+(* The Coq toplevel loop. *)
+
+(* A buffer for the character read from a channel. We store the command
+ * entered to be able to report errors without pretty-printing. *)
+
+type input_buffer = { 
+  mutable prompt : unit -> string;
+  mutable str : string; (* buffer of already read characters *)
+  mutable len : int;    (* number of chars in the buffer *)
+  mutable bols : int list; (* offsets in str of begining of lines *)
+  mutable tokens : Gram.parsable; (* stream of tokens *)
+  mutable start : int } (* stream count of the first char of the buffer *)
+
+(* The input buffer of stdin *)
+
+val top_buffer : input_buffer
+val set_prompt : (unit -> string) -> unit
+
+(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
+  May raise only the following exceptions: Drop and End_of_input,
+  meaning we get out of the Coq loop *)
+
+val print_toplevel_error : exn -> std_ppcmds
+
+(* Parse and execute a vernac command *)
+
+val do_vernac : unit -> unit
+
+(* Main entry point of Coq: read and execute vernac commands *)
+
+val loop : unit -> unit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
new file mode 100644
index 000000000..d0a0c63ff
--- /dev/null
+++ b/toplevel/vernac.ml
@@ -0,0 +1,154 @@
+
+(* $Id$ *)
+
+(* Parsing of vernacular. *)
+
+open Pp
+open Util
+open System
+open Coqast
+open Vernacinterp
+
+(* The functions in this module may raise (unexplainable!) exceptions.
+   Use the module Coqtoplevel, which catches these exceptions
+   (the exceptions are explained only at the toplevel). *)
+
+exception DuringCommandInterp of Coqast.loc * exn
+
+(* Like Exc_located, but specifies the outermost file read, the filename
+   associated to the location of the error, and the error itself. *)
+
+exception Error_in_file of string * (string * Coqast.loc) * exn
+
+(* Specifies which file is read. The intermediate file names are
+   discarded here. The Drop exception becomes an error. We forget
+   if the error ocurred during interpretation or not *)
+
+let raise_with_file file exc =
+  let (cmdloc,re) =
+    match exc with
+      | DuringCommandInterp(loc,e) -> (loc,e)
+      | e -> (Ast.dummy_loc,e) 
+  in
+  let (inner,inex) =
+    match re with
+      | Error_in_file (_, (f,loc), e) when loc <> Ast.dummy_loc ->
+          ((f, loc), e)
+      | Stdpp.Exc_located (loc, e) when loc <> Ast.dummy_loc ->
+          ((file, loc), e)
+      | _ -> ((file,cmdloc), re)
+  in 
+  raise (Error_in_file (file, inner, disable_drop inex))
+
+let real_error = function
+  | Stdpp.Exc_located (_, e) -> e
+  | Error_in_file (_, _, e) -> e
+  | e -> e
+
+(* Opening and closing a channel. Open it twice when verbose: the first
+   channel is used to read the commands, and the second one to print them.
+   Note: we could use only one thanks to seek_in, but seeking on and on in
+   the file we parse seems a bit risky to me.  B.B.  *)
+
+let open_file_twice_if verbosely fname =
+  let longfname = find_file_in_path fname in
+  let in_chan = open_in longfname in
+  let verb_ch = if verbosely then Some (open_in longfname) else None in
+  let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
+  (in_chan, longfname, (po, verb_ch))
+
+let close_input in_chan (_,verb) =
+  try 
+    close_in in_chan;
+    match verb with
+      | Some verb_ch -> close_in verb_ch
+      | _ -> ()
+  with _ -> ()
+
+let verbose_phrase verbch loc =
+  match verbch with
+    | Some ch ->
+	let len = snd loc - fst loc in
+	let s = String.create len in
+        seek_in ch (fst loc);
+        really_input ch s 0 len;
+        message s;
+        pp_flush()
+    | _ -> ()
+
+exception End_of_input
+  
+let parse_phrase (po, verbch) =
+  match Pcoq.Gram.Entry.parse Pcoq.main_entry po with
+    | Some com -> verbose_phrase verbch (Ast.loc com); com
+    | None -> raise End_of_input
+
+(* vernac parses the given stream, executes interpfun on the syntax tree it
+ * parses, and is verbose on "primitives" commands if verbosely is true *)
+
+let just_parsing = ref false
+
+let rec vernac interpfun input =
+  let com = parse_phrase input in
+  try
+    match com with
+      | Node (_,"LoadFile",[Str(_, verbosely); Str(_,fname)]) ->
+          let verbosely = verbosely = "Verbose" in
+          raw_load_vernac_file verbosely (make_suffix fname ".v")
+            
+      | Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
+                               Str (_,mname); Str(_,fname)]) ->
+          let verbosely = verbosely = "Verbose" in
+          let only_spec = only_spec = "Specification" in
+          Lib.with_heavy_rollback (* to roll back in case of error *)
+            (raw_compile_module verbosely only_spec mname)
+            (make_suffix fname ".v")
+      | _ -> if not !just_parsing then interpfun com
+  with e -> 
+    raise (DuringCommandInterp (Ast.loc com, e))
+      
+and raw_load_vernac_file verbosely s =
+  let _ = read_vernac_file verbosely s in ()
+
+and raw_compile_module verbosely only_spec mname file =
+  Library.open_module mname;
+  let lfname = read_vernac_file verbosely file in
+  let base = Filename.chop_suffix lfname ".v" in
+  if Pfedit.refining () then
+    errorlabstrm "Vernac.raw_compile_module"
+      [< 'sTR"proof editing in progress" ; (Pfedit.msg_proofs false) >];
+  if only_spec then
+    failwith ".vi not yet implemented"
+  else 
+    Library.save_module_to mname base
+
+and read_vernac_file verbosely s =
+  let interpfun =
+    if verbosely then 
+      Vernacinterp.interp
+    else 
+      Options.silently Vernacinterp.interp 
+  in
+  let (in_chan, fname, input) = open_file_twice_if verbosely s in
+  try
+    (* we go out of the following infinite loop when a End_of_input is
+     * raised, which means that we raised the end of the file being loaded *)
+    while true do vernac interpfun input; pp_flush () done; fname
+  with e ->   (* whatever the exception *)
+    close_input in_chan input;    (* we must close the file first *)
+    match real_error e with
+      | End_of_input -> fname
+      | _ -> raise_with_file fname e
+
+(* raw_do_vernac : char Stream.t -> unit
+ * parses and executes one command of the vernacular char stream *)
+
+let raw_do_vernac po =
+  vernac (Lib.with_heavy_rollback Vernacinterp.interp) (po,None)
+
+(* Load a vernac file. Errors are annotated with file and location *)
+let load_vernac verb file =
+  try 
+    raw_load_vernac_file verb file
+  with e -> 
+    raise_with_file file e
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
new file mode 100644
index 000000000..401598781
--- /dev/null
+++ b/toplevel/vernac.mli
@@ -0,0 +1,28 @@
+
+(* $Id$ *)
+
+(* Parsing of vernacular. *)
+
+(* Like Exc_located, but specifies the outermost file read, the input buffer
+   associated to the location of the error, and the error itself. *)
+
+exception Error_in_file of string * (string * Coqast.loc) * exn
+
+(* Read a vernac command on the specified input (parse only).
+   Raises End_of_file if EOF (or Ctrl-D) is reached. *)
+
+val parse_phrase : Pcoq.Gram.parsable * in_channel option -> Coqast.t
+
+(* Reads and executes vernac commands from a stream.
+   The boolean just_parsing disables interpretation of commands. *)
+
+exception DuringCommandInterp of Coqast.loc * exn
+exception End_of_input
+
+val just_parsing : bool ref
+val raw_do_vernac : Pcoq.Gram.parsable -> unit
+
+(* Load a vernac file, verbosely or not. Errors are annotated with file
+   and location *)
+
+val load_vernac : bool -> string -> unit
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
new file mode 100644
index 000000000..8e6255d76
--- /dev/null
+++ b/toplevel/vernacinterp.mli
@@ -0,0 +1,43 @@
+
+open Names
+open Pp
+open Proof_trees
+ 
+exception Drop
+exception ProtectedLoop
+exception Quit
+
+val disable_drop : exn -> exn
+
+type vernac_arg = 
+  | VARG_VARGLIST of vernac_arg list
+  | VARG_STRING of string
+  | VARG_NUMBER of int
+  | VARG_NUMBERLIST of int list
+  | VARG_IDENTIFIER of identifier
+  | VCALL of string * vernac_arg list
+  | VARG_COMMAND of Coqast.t
+  | VARG_COMMANDLIST of Coqast.t list
+  | VARG_TACTIC of Coqast.t
+  | VARG_TACTIC_ARG of tactic_arg
+  | VARG_BINDER of identifier list * Coqast.t
+  | VARG_BINDERLIST of (identifier list * Coqast.t) list
+  | VARG_AST of Coqast.t
+  | VARG_ASTLIST of Coqast.t list
+  | VARG_UNIT
+  | VARG_DYN of Dyn.t   (* to put whatever you want *)
+
+
+val vinterp_add : string -> (vernac_arg list -> unit -> unit) -> unit
+val overwriting_vinterp_add : 
+  string -> (vernac_arg list -> unit -> unit) -> unit
+
+val vinterp_map : string -> vernac_arg list -> unit -> unit
+val vinterp_init : unit -> unit
+val cvt_varg : Coqast.t -> vernac_arg
+val call : string * vernac_arg list -> unit
+val interp : Coqast.t -> unit
+
+(* raises an user error telling that the vernac command was called
+   with bad arguments *)
+val bad_vernac_args : string -> 'a