Delineating a API for Coq inside toplevel/vernac.ml

Coq use case are mostly thoses :
- parsing a char stream to get a vernac expr
- evaluating a vernac expr with backtracking
- turning a knob with a vernac expr, no backtracking
- loading an entire file
- compiling an entire file
- backtracking (no clean API for this yet)
- peeking Coq state info (no clean API for this yet)

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

2 files changed, 26 insertions, 25 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6d4ecf7740..0bdb68f495 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -89,7 +89,7 @@ let verbose_phrase verbch loc =
 
 exception End_of_input
 
-let parse_phrase (po, verbch) =
+let parse_sentence (po, verbch) =
   match Pcoq.Gram.Entry.parse Pcoq.main_entry po with
     | Some (loc,_ as com) -> verbose_phrase verbch loc; com
     | None -> raise End_of_input
@@ -193,22 +193,21 @@ let rec vernac_com interpfun (loc,com) =
       Format.set_formatter_out_channel stdout;
       raise (DuringCommandInterp (loc, e))
 
-and vernac interpfun input =
-  vernac_com interpfun (parse_phrase input)
-
 and read_vernac_file verbosely s =
   Flags.make_warn verbosely;
   let interpfun =
-    if verbosely then
-      Vernacentries.interp
-    else
-      Flags.silently Vernacentries.interp
+    if verbosely then Vernacentries.interp
+    else Flags.silently Vernacentries.interp
   in
-  let (in_chan, fname, input) = open_file_twice_if verbosely s 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
+    while true do
+      vernac_com interpfun (parse_sentence input);
+      pp_flush ()
+    done
   with e ->   (* whatever the exception *)
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
@@ -217,17 +216,23 @@ and read_vernac_file verbosely s =
           if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname e
 
-(* raw_do_vernac : char Stream.t -> unit
- * parses and executes one command of the vernacular char stream.
- * Marks the end of the command in the lib_stk with a new label to
- * make vernac undoing easier. Also freeze state to speed up
- * backtracking. *)
 
-let raw_do_vernac po =
-  vernac (States.with_heavy_rollback Vernacentries.interp) (po,None);
+(* eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
+ * execute one vernacular command. Marks the end of the command in the lib_stk
+ * with a new label to make vernac undoing easier. Also freeze state to speed up
+ * backtracking. *)
+let eval_expr last =
+  vernac_com (States.with_heavy_rollback Vernacentries.interp) last;
   Lib.add_frozen_state();
   Lib.mark_end_of_command()
 
+let eval_ctrl ast =
+  vernac_com Vernacentries.interp (Util.dummy_loc,ast)
+
+(* raw_do_vernac : Pcoq.Gram.parsable -> unit
+ * vernac_step . parse_sentence *)
+let raw_do_vernac po = eval_expr (parse_sentence (po,None))
+
 (* XML output hooks *)
 let xml_start_library = ref (fun _ -> ())
 let xml_end_library = ref (fun _ -> ())
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 4dff36e53e..747c02afe3 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -13,8 +13,8 @@
 (* 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 ->
-  Util.loc * Vernacexpr.vernac_expr
+val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
+ Util.loc * Vernacexpr.vernac_expr
 
 (* Reads and executes vernac commands from a stream.
    The boolean [just_parsing] disables interpretation of commands. *)
@@ -23,6 +23,8 @@ exception DuringCommandInterp of Util.loc * exn
 exception End_of_input
 
 val just_parsing : bool ref
+val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
+val eval_ctrl : Vernacexpr.vernac_expr -> unit
 val raw_do_vernac : Pcoq.Gram.parsable -> unit
 
 (* Set XML hooks *)
@@ -38,9 +40,3 @@ val load_vernac : bool -> string -> unit
 (* Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
 
 val compile : bool -> string -> unit
-
-(* Interpret a vernac AST *)
-
-val vernac_com :
-  (Vernacexpr.vernac_expr -> unit) ->
-  Util.loc * Vernacexpr.vernac_expr -> unit