Flag ide_slave moved into Flags module

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

3 files changed, 7 insertions, 4 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index c6b1cdd7d..d931ad987 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -34,6 +34,8 @@ let term_quality = ref false
 
 let xml_export = ref false
 
+let ide_slave = ref false
+
 type load_proofs = Force | Lazy | Dont
 
 let load_proofs = ref Lazy
diff --git a/lib/flags.mli b/lib/flags.mli
index 797ee3875..8ff9deeaa 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -20,6 +20,8 @@ val term_quality : bool ref
 
 val xml_export : bool ref
 
+val ide_slave : bool ref
+
 type load_proofs = Force | Lazy | Dont
 val load_proofs : load_proofs ref
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7abb0180f..9ec843441 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -184,7 +184,6 @@ let usage () =
 
 let warning s = msg_warning (strbrk s)
 
-let ide_slave = ref false
 let filter_opts = ref false
 
 let verb_compat_ntn = ref false
@@ -339,7 +338,7 @@ let parse_args arglist =
     | "-v7" :: rem -> error "This version of Coq does not support v7 syntax"
     | "-v8" :: rem -> parse rem
 
-    | "-ideslave" :: rem -> ide_slave := true; parse rem
+    | "-ideslave" :: rem -> Flags.ide_slave := true; parse rem
 
     | "-filteropts" :: rem -> filter_opts := true; parse rem
 
@@ -372,7 +371,7 @@ let init arglist =
       let foreign_args = parse_args arglist in
       if !filter_opts then
         (print_string (String.concat "\n" foreign_args); exit 0);
-      if !ide_slave then begin
+      if !Flags.ide_slave then begin
         Flags.make_silent true;
         Ide_slave.init_stdout ()
       end;
@@ -421,7 +420,7 @@ let start () =
   let () = if Dumpglob.dump () then
     let () = if_verbose warning "Dumpglob cannot be used in interactive mode." in
     Dumpglob.noglob () in
-  if !ide_slave then
+  if !Flags.ide_slave then
     Ide_slave.loop ()
   else
     Toplevel.loop();