Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from de coqdoc (compatibilité)

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

2 files changed, 50 insertions, 38 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d802770f0..fccfb1bf3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -252,7 +252,7 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
 let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
   let ntn,args = contract_notation ntn args in
   let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-    if !Flags.dump then Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df;
+    if Dumpglob.dump () then Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df;
     let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
       subst_aconstr_in_rawconstr loc intern subst ([],env) c
 
@@ -334,10 +334,10 @@ let check_no_explicitation l =
 let intern_qualid loc qid intern env args =
   try match Nametab.extended_locate qid with
   | TrueGlobal ref ->
-      Dumpglob.add_glob loc ref;
+      if Dumpglob.dump() then Dumpglob.add_glob loc ref;
       RRef (loc, ref), args
   | SyntacticDef sp ->
-      Dumpglob.add_glob_kn loc sp;
+      if Dumpglob.dump() then Dumpglob.add_glob_kn loc sp;
       let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
       let nids = List.length ids in
       if List.length args < nids then error_not_enough_arguments loc;
@@ -567,7 +567,7 @@ let find_constructor ref f aliases pats scopes =
 	    let v = Environ.constant_value (Global.env()) cst in
 	    unf (global_of_constr v)
         | ConstructRef cstr -> 
-	    Dumpglob.add_glob loc r; 
+	    if Dumpglob.dump() then Dumpglob.add_glob loc r; 
 	    cstr, [], pats
         | _ -> raise Not_found
       in unf r
@@ -618,7 +618,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
       let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-      if !Flags.dump then Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
+      if Dumpglob.dump () then Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
       let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes 
 	c
@@ -627,7 +627,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
       let a = alias_of aliases in
       let (c,df) = Notation.interp_prim_token_cases_pattern loc p a 
 	(tmp_scope,scopes) in
-      if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df;
+      if Dumpglob.dump () then Dumpglob.dump_notation_location (fst (unloc loc)) df;
       (ids,[subst,c])
   | CPatDelimiters (loc, key, e) ->
       intern_pat (find_delimiters_scope loc key::scopes) aliases None e
@@ -687,7 +687,7 @@ let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function
   | Anonymous -> env 
   | Name id -> 
       check_hidden_implicit_parameters id lvar;
-      Dumpglob.dump_binding loc id;
+      if Dumpglob.dump() then Dumpglob.dump_binding loc id;
       (Idset.add id ids,tmpsc,scopes)
 
 let intern_typeclass_binders intern_type lvar env bl =
@@ -887,7 +887,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         intern_notation intern env loc ntn args
     | CPrim (loc, p) ->
 	let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
-	if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df;
+	if Dumpglob.dump () then Dumpglob.dump_notation_location (fst (unloc loc)) df;
 	c
     | CDelimiters (loc, key, e) ->
 	intern (ids,None,find_delimiters_scope loc key::scopes) e
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 84117fafa..b8121af86 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -16,7 +16,7 @@ let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> h
 let glob_file = ref Pervasives.stdout
 
 let open_glob_file f =
-  glob_file := Pervasives.open_out(f ^ ".glob")
+  glob_file := Pervasives.open_out f
   
 let close_glob_file () =
   Pervasives.close_out !glob_file
@@ -24,10 +24,29 @@ let close_glob_file () =
 let dump_string s = 
   Pervasives.output_string !glob_file s
 
+type glob_output_t = 
+    | None
+    | StdOut
+    | MultFiles
+    | File of string
+
+let glob_output = ref MultFiles
+
+let dump () = !glob_output != None
+
+let noglob () = glob_output := None
+
+let dump_to_stdout () = glob_output := StdOut
+
+let multi_dump () = !glob_output = MultFiles
+
+let dump_into_file f = glob_output := File f; open_glob_file f
+
+let previous_state = ref MultFiles
+let pause () = previous_state := !glob_output
+let continue () = glob_output := !previous_state
 
 
-(**********************************************************************)
-(* Dump of globalization (to be used by coqdoc)                       *)
 let token_number = ref 0
 let last_pos = ref 0
 
@@ -117,25 +136,21 @@ let add_glob_gen loc sp lib_dp ty =
     dump_ref loc filepath modpath ident ty
 
 let add_glob loc ref = 
-  let sp = Nametab.sp_of_global ref in
-  let lib_dp = Lib.library_part ref in
-  let ty = type_of_global_ref ref in
-    add_glob_gen loc sp lib_dp ty
+  if loc <> Util.dummy_loc then
+    let sp = Nametab.sp_of_global ref in
+    let lib_dp = Lib.library_part ref in
+    let ty = type_of_global_ref ref in
+      add_glob_gen loc sp lib_dp ty
       
-let add_glob loc ref =
-  if !Flags.dump && loc <> Util.dummy_loc then add_glob loc ref
-
 let mp_of_kn kn = 
   let mp,sec,l = Names.repr_kn kn in 
     Names.MPdot (mp,l) 
 
 let add_glob_kn loc kn =
-  let sp = Nametab.sp_of_syntactic_definition kn in
-  let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
-    add_glob_gen loc sp lib_dp "syndef"
-
-let add_glob_kn loc ref =
-  if !Flags.dump && loc <> Util.dummy_loc then add_glob_kn loc ref
+  if loc <> Util.dummy_loc then
+    let sp = Nametab.sp_of_syntactic_definition kn in
+    let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
+      add_glob_gen loc sp lib_dp "syndef"
 
 let add_local loc id = ()
 (*   let mod_dp,id = repr_path sp in *)
@@ -189,23 +204,20 @@ let dump_local_binder b sec ty =
   | Topconstr.LocalRawDef _ -> ()
 
 let dump_modref loc mp ty =
-  if !Flags.dump then
-    let (dp, l) = Lib.split_modpath mp in
-    let fp = Names.string_of_dirpath dp in
-    let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in
-      dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
-			    (fst (Util.unloc loc)) fp mp "<>" ty)
+  let (dp, l) = Lib.split_modpath mp in
+  let fp = Names.string_of_dirpath dp in
+  let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in
+    dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
+		    (fst (Util.unloc loc)) fp mp "<>" ty)
 
 let dump_moddef loc mp ty =
-  if !Flags.dump then
-    let (dp, l) = Lib.split_modpath mp in
-    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
-      dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
+  let (dp, l) = Lib.split_modpath mp in
+  let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+    dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
 
 let dump_libref loc dp ty =
-  if !Flags.dump then
-    dump_string (Printf.sprintf "R%d %s <> <> %s\n" 
-			     (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
+  dump_string (Printf.sprintf "R%d %s <> <> %s\n" 
+		  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
 
 let dump_notation_location pos ((path,df),sc) =
   let rec next growing =
@@ -218,7 +230,7 @@ let dump_notation_location pos ((path,df),sc) =
   let loc = next (pos >= !last_pos) in
     last_pos := pos;
     let path = Names.string_of_dirpath path in
-    let _sc = match sc with Some sc -> " "^sc | None -> "" in
+    let _sc = match sc with Some sc -> " "^sc | _ -> "" in
       dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)