restructuration des printers: proofs passe avant parsing

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

1 files changed, 12 insertions, 47 deletions

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index c6a442761..239b45fab 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -19,49 +19,26 @@ open Unix
 (* 1. Core objects *)
 let ocamlobjs = ["unix.cma"]
 let dynobjs = ["dynlink.cma"]
-let camlp4objs = [(*"odyl.cma"; "camlp4.cma";*) "gramlib.cma"]
-let configobjs = ["coq_config.cmo"]
-let libobjs = ocamlobjs @ camlp4objs @ configobjs
+let camlp4objs = ["gramlib.cma"]
+let libobjs = ocamlobjs @ camlp4objs
 
 let spaces = Str.regexp "[ \t\n]+"
-let split_cmo l = Str.split spaces l
+let split_list l = Str.split spaces l
 
-let lib = split_cmo Tolink.lib 
-let kernel = split_cmo Tolink.kernel
-let library = split_cmo Tolink.library 
-let pretyping = split_cmo Tolink.pretyping 
-let interp = split_cmo Tolink.interp
-let parsing = split_cmo Tolink.parsing 
-let proofs = split_cmo Tolink.proofs 
-let tactics = split_cmo Tolink.tactics 
-let toplevel = split_cmo Tolink.toplevel 
-let highparsing = split_cmo Tolink.highparsing 
-let highparsingnew = split_cmo Tolink.highparsingnew
-let ide = split_cmo Tolink.ide 
+let ide = split_list Tolink.ide 
 
-let core_objs = 
-  libobjs @ lib @ kernel @ library @ pretyping @ interp @ parsing @ 
-  proofs @ tactics
+let core_objs = split_list Tolink.core_objs
+let core_libs = split_list Tolink.core_libs
 
-let core_libs = 
-  libobjs @ [ "lib/lib.cma" ; "kernel/kernel.cma" ; "library/library.cma" ;
-  "pretyping/pretyping.cma" ; "interp/interp.cma" ; "parsing/parsing.cma" ;
-  "proofs/proofs.cma" ; "tactics/tactics.cma" ]
-
-(* 3. Files only in coqsearchisos (if option -searchisos is used) *)
-let coqsearch = ["version_searchisos.cmo"; "cmd_searchisos_line.cmo"]
-
-(* 4. Toplevel objects *)
-let camlp4objs =
+(* 3. Toplevel objects *)
+let camlp4topobjs =
   ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"; "q_util.cmo"; "q_coqast.cmo" ]
-let topobjs = camlp4objs
+let topobjs = camlp4topobjs
 
 let gramobjs = []
 let notopobjs = gramobjs
 
-(* 5. High-level tactics objects *)
-let hightactics = 
- (split_cmo Tolink.hightactics) @ (split_cmo Tolink.contrib) 
+(* 4. High-level tactics objects *)
 
 (* environment *)
 let src_coqtop = ref Coq_config.coqtop
@@ -102,7 +79,6 @@ let module_of_file name =
 (* Build the list of files to link and the list of modules names *)
 let files_to_link userfiles =
   let dyn_objs = if not !opt then dynobjs else [] in
-  let command_objs = if !searchisos then coqsearch else [] in
   let toplevel_objs =
     if !top then topobjs else if !opt then notopobjs else [] in
   let ide_objs = if !coqide then 
@@ -114,17 +90,8 @@ let files_to_link userfiles =
      "ide/ide.cma" ]
   else [] 
   in
-  let objs = 
-    core_objs @ dyn_objs @ toplevel @ highparsing @ highparsingnew @ 
-    command_objs @ hightactics @ toplevel_objs @ ide_objs
-  and libs =
-    core_libs @ dyn_objs @ 
-    [ "toplevel/toplevel.cma" ; "parsing/highparsing.cma" ;
-      "parsing/highparsingnew.cma" ] @ 
-    command_objs @ [ "tactics/hightactics.cma" ; "contrib/contrib.cma" ] @
-    toplevel_objs @ 
-    ide_libs      
-  in
+  let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs
+  and libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in
   let objstolink,libstolink =
     if !opt then 
       ((List.map native_suffix objs) @ userfiles,
@@ -183,8 +150,6 @@ let parse_args () =
     | "-opt" :: rem -> opt := true ; parse (op,fl) rem
     | "-full" :: rem -> full := true ; parse (op,fl) rem
     | "-top" :: rem -> top := true ; parse (op,fl) rem
-    | "-searchisos" :: rem ->
-        searchisos := true; parse (op,fl) rem
     | "-ide" :: rem ->
         coqide := true; parse (op,fl) rem
     | "-v8" :: rem -> parse (op,fl) rem