Removing -filterops "hack" from coqtop.

This is now the "coqidetop" binary which specifically know how to
collect extra arguments.

3 files changed, 15 insertions, 50 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index d05bf6378a..5e3a82dcb9 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -78,18 +78,13 @@ type coqargs_pre = {
   inputstate  : string option;
 }
 
-type coqargs_base_query =
+type coqargs_query =
   | PrintTags | PrintWhere | PrintConfig
   | PrintVersion | PrintMachineReadableVersion
   | PrintHelp of (unit -> unit)
 
-type coqargs_queries = {
-  queries : coqargs_base_query list;
-  filteropts : string list option;
-}
-
 type coqargs_main =
-  | Queries of coqargs_queries
+  | Queries of coqargs_query list
   | Run
 
 type coqargs_post = {
@@ -147,10 +142,7 @@ let default_pre = {
   inputstate   = None;
 }
 
-let default_queries = {
-  queries = [];
-  filteropts = None;
-}
+let default_queries = []
 
 let default_post = {
   memory_stat  = false;
@@ -204,22 +196,10 @@ let set_color opts = function
   | _ ->
     error_wrong_arg ("Error: on/off/auto expected after option color")
 
-let add_query { queries; filteropts } q =
-  { queries = queries@[q]; filteropts }
-
 let set_query opts q =
   { opts with main = match opts.main with
-  | Run -> Queries (add_query default_queries q)
-  | Queries queries -> Queries (add_query queries q)
-  }
-
-let add_filteropts { queries } =
-  { queries; filteropts = Some [] }
-
-let set_filteropts opts =
-  { opts with main = match opts.main with
-  | Run -> Queries (add_filteropts default_queries)
-  | Queries queries -> Queries (add_filteropts queries)
+  | Run -> Queries (default_queries@[q])
+  | Queries queries -> Queries (queries@[q])
   }
 
 let warn_deprecated_inputstate =
@@ -553,7 +533,6 @@ let parse_args ~help ~init arglist : t * string list =
                   { oval with config = { oval.config with diffs_set = true }}
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
-    |"-filteropts" -> set_filteropts oval
     |"-impredicative-set" ->
       set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval
     |"-allow-sprop" -> set_logic (fun o -> { o with allow_sprop = true }) oval
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 3cbb0b109f..d1873bcb58 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -53,18 +53,13 @@ type coqargs_pre = {
   inputstate  : string option;
 }
 
-type coqargs_base_query =
+type coqargs_query =
   | PrintTags | PrintWhere | PrintConfig
   | PrintVersion | PrintMachineReadableVersion
   | PrintHelp of (unit -> unit)
 
-type coqargs_queries = {
-  queries : coqargs_base_query list;
-  filteropts : string list option;
-}
-
 type coqargs_main =
-  | Queries of coqargs_queries
+  | Queries of coqargs_query list
   | Run
 
 type coqargs_post = {
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 770698bee8..95f9d9ef77 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -155,22 +155,13 @@ let print_style_tags opts =
   let () = List.iter iter tags in
   flush_all ()
 
-let print_queries opts q =
-  let print_query = function
-    | PrintVersion -> Usage.version ()
-    | PrintMachineReadableVersion -> Usage.machine_readable_version ()
-    | PrintWhere -> print_endline (Envars.coqlib ())
-    | PrintHelp f -> f ()
-    | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs
-    | PrintTags -> print_style_tags opts.config in
-  List.iter print_query q.queries;
-  match q.filteropts with
-  | Some extras ->
-    if q.queries <> [] && extras <> [] then
-      error_wrong_arg "Queries are exclusive of other arguments"
-    else
-      print_string (String.concat "\n" extras)
-  | None -> ()
+let print_query opts = function
+  | PrintVersion -> Usage.version ()
+  | PrintMachineReadableVersion -> Usage.machine_readable_version ()
+  | PrintWhere -> print_endline (Envars.coqlib ())
+  | PrintHelp f -> f ()
+  | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs
+  | PrintTags -> print_style_tags opts.config
 
 (** GC tweaking *)
 
@@ -268,7 +259,7 @@ let init_toplevel custom =
   let () = init_setup opts.config.coqlib in
   (* Querying or running? *)
   match opts.main with
-  | Queries q -> print_queries opts q; exit 0
+  | Queries q -> List.iter (print_query opts) q; exit 0
   | Run ->
     let customstate = init_execution opts (custom.init customopts) in
     opts, customopts, customstate