Applying Emilio's suggestion to simplify type of eval_expr.

This is not fully satisfactory though since we would not like to have
"eval_expr" depending on a parsing/lexing/comments state... but it
does because of eval_expr possibly printing the vernac expression
given to it.

3 files changed, 8 insertions, 8 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 71e1f9593d..08c3fe2053 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -299,7 +299,7 @@ let do_vernac () =
   resynch_buffer top_buffer;
   try
     let input = (top_buffer.tokens, None) in
-    Vernac.eval_expr input (read_sentence input)
+    Vernac.eval_expr top_buffer.tokens (read_sentence input)
   with
     | End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f03f31178c..ee5827b92b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -141,7 +141,7 @@ let pr_new_syntax_in_context loc ocom =
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
-let pr_new_syntax (po,_) loc ocom =
+let pr_new_syntax po loc ocom =
   (* Reinstall the context of parsing which includes the bindings of comments to locations *)
   Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom
 
@@ -173,7 +173,7 @@ let print_cmd_header loc com =
   Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
   Format.pp_print_flush !Pp_control.std_ft ()
 
-let rec vernac_com input checknav (loc,com) =
+let rec vernac_com po checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
@@ -199,7 +199,7 @@ let rec vernac_com input checknav (loc,com) =
   in
     try
       checknav loc com;
-      if do_beautify () then pr_new_syntax input loc (Some com);
+      if do_beautify () then pr_new_syntax po loc (Some com);
       (* XXX: This is not 100% correct if called from an IDE context *)
       if !Flags.time then print_cmd_header loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
@@ -223,7 +223,7 @@ and read_vernac_file verbosely s =
     while true do
       let loc_ast = parse_sentence input in
       CWarnings.set_current_loc (fst loc_ast);
-      vernac_com input checknav loc_ast;
+      vernac_com (fst input) checknav loc_ast;
     done
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
@@ -232,7 +232,7 @@ and read_vernac_file verbosely s =
     match e with
       | End_of_input ->
           if do_beautify () then
-            pr_new_syntax input (Loc.make_loc (max_int,max_int)) None
+            pr_new_syntax (fst input) (Loc.make_loc (max_int,max_int)) None
       | reraise ->
 	 iraise (disable_drop e, info)
 
@@ -247,7 +247,7 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr input loc_ast = vernac_com input checknav loc_ast
+let eval_expr po loc_ast = vernac_com po checknav loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 2fd86ddc22..52216bbfd6 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -21,7 +21,7 @@ exception End_of_input
 
 val just_parsing : bool ref
 
-val eval_expr : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -> unit
+val eval_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit
 
 (** Set XML hooks *)
 val xml_start_library : (unit -> unit) Hook.t