[stm] Break stm/toplevel dependency loop.

Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.

This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.

As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.

Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.

1 files changed, 77 insertions, 0 deletions

diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
new file mode 100644
index 000000000..f26ef460d
--- /dev/null
+++ b/vernac/vernacinterp.ml
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Pp
+open CErrors
+
+type deprecation = bool
+type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
+
+(* Table of vernac entries *)
+let vernac_tab =
+  (Hashtbl.create 51 :
+    (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t)
+
+let vinterp_add depr s f =
+  try
+    Hashtbl.add vernac_tab s (depr, f)
+  with Failure _ ->
+    user_err ~hdr:"vinterp_add"
+      (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
+
+let overwriting_vinterp_add s f =
+  begin
+    try
+      let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s
+    with Not_found -> ()
+  end;
+  Hashtbl.add vernac_tab s (false, f)
+
+let vinterp_map s =
+  try
+    Hashtbl.find vernac_tab s
+  with Failure _ | Not_found ->
+    user_err ~hdr:"Vernac Interpreter"
+      (str"Cannot find vernac command " ++ str (fst s) ++ str".")
+
+let vinterp_init () = Hashtbl.clear vernac_tab
+
+let warn_deprecated_command =
+  let open CWarnings in
+  create ~name:"deprecated-command" ~category:"deprecated"
+         (fun pr -> str "Deprecated vernacular command: " ++ pr)
+
+(* Interpretation of a vernac command *)
+
+let call ?locality (opn,converted_args) =
+  let loc = ref "Looking up command" in
+  try
+    let depr, callback = vinterp_map opn in
+    let () = if depr then
+      let rules = Egramml.get_extend_vernac_rule opn in
+      let pr_gram = function
+      | Egramml.GramTerminal s -> str s
+      | Egramml.GramNonTerminal _ -> str "_"
+      in
+      let pr = pr_sequence pr_gram rules in
+      warn_deprecated_command pr;
+    in
+    loc:= "Checking arguments";
+    let hunk = callback converted_args in
+    loc:= "Executing command";
+    Locality.LocalityFixme.set locality;
+    hunk();
+    Locality.LocalityFixme.assert_consumed()
+  with
+    | Drop -> raise Drop
+    | reraise ->
+        let reraise = CErrors.push reraise in
+        if !Flags.debug then
+	  Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc);
+        iraise reraise