From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 stm/vernac_classifier.ml | 41 ++++++++++++++++++-----------------------
 1 file changed, 18 insertions(+), 23 deletions(-)

(limited to 'stm/vernac_classifier.ml')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f68c8b32..21704779 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -16,8 +16,6 @@ open Vernacexpr
 
 let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
 
-let string_of_in_script b = if b then " (inside script)" else ""
-
 let string_of_parallel = function
   | `Yes (solve,abs) ->
        "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
@@ -34,7 +32,7 @@ let string_of_vernac_type = function
       "ProofStep " ^ string_of_parallel parallel ^
         Option.default "" proof_block_detection
   | VtProofMode s -> "ProofMode " ^ s
-  | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
+  | VtQuery -> "Query"
   | VtMeta -> "Meta "
 
 let string_of_vernac_when = function
@@ -44,25 +42,25 @@ let string_of_vernac_when = function
 let string_of_vernac_classification (t,w) =
   string_of_vernac_type t ^ " " ^ string_of_vernac_when w
 
-let classifiers = ref []
-let declare_vernac_classifier
-  (s : Vernacexpr.extend_name)
-  (f : Genarg.raw_generic_argument list -> unit -> vernac_classification)
-=
-  classifiers := !classifiers @ [s,f]
-
 let idents_of_name : Names.Name.t -> Names.Id.t list =
   function
   | Names.Anonymous -> []
   | Names.Name n -> [n]
 
+let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
+
+let options_affecting_stm_scheduling =
+  [ Vernacentries.universe_polymorphism_option_name;
+    stm_allow_nested_proofs_option_name ]
+
 let classify_vernac e =
   let static_classifier ~poly e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
     | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l))
-      when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
+      when CList.exists (CList.equal String.equal l)
+        options_affecting_stm_scheduling ->
        VtSideff [], VtNow
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
@@ -70,7 +68,7 @@ let classify_vernac e =
     | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
-    | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater
+    | VernacCheckMayEval _ -> VtQuery, VtLater
     (* ProofStep *)
     | VernacProof _ 
     | VernacFocus _ | VernacUnfocus
@@ -145,7 +143,7 @@ let classify_vernac e =
     | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
     | VernacChdir _ 
     | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
-    | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _
+    | VernacArguments _
     | VernacReserve _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
@@ -157,6 +155,7 @@ let classify_vernac e =
     | VernacDeclareClass _ | VernacDeclareInstances _
     | VernacRegister _
     | VernacNameSectionHypSet _
+    | VernacDeclareCustomEntry _
     | VernacComments _ -> VtSideff [], VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
@@ -183,30 +182,26 @@ let classify_vernac e =
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
     | VernacResetName _ | VernacResetInitial
-    | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
+    | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
     (* What are these? *)
-    | VernacToplevelControl _
     | VernacRestoreState _
     | VernacWriteState _ -> VtSideff [], VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
-        try List.assoc s !classifiers l ()
+        try Vernacentries.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let poly = List.fold_left (fun poly f ->
-          match f with
-          | VernacPolymorphic b -> b
-          | (VernacProgram | VernacLocal _) -> poly
-        ) poly f in
+      let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in
+      let poly = atts.Vernacinterp.polymorphic in
       static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
        static_control_classifier ~poly e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match static_control_classifier ~poly e with
-        | ( VtQuery _ | VtProofStep _ | VtSideff _
+        | ( VtQuery | VtProofStep _ | VtSideff _
           | VtProofMode _ | VtMeta), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
@@ -215,6 +210,6 @@ let classify_vernac e =
   in
   static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
 
-let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
+let classify_as_query = VtQuery, VtLater
 let classify_as_sideeff = VtSideff [], VtLater
 let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
-- 
cgit v1.2.3