Add separate command for documenation generation and add option for specifying output directory.

Author: MM45

src/ec.ml

@@ -393,6 +393,7 @@ let main () =
       eco         : bool;
       gccompact   : int option;
       gendoc      : bool;
+      outdirp     : string option;
     }
   end in
 
@@ -448,7 +449,8 @@ let main () =
         ; interactive = true
         ; eco         = false
         ; gccompact   = None
-        ; gendoc      = false }
+        ; gendoc      = false 
+        ; outdirp     = None }
 
     end
 
@@ -476,14 +478,54 @@ let main () =
         ; interactive = false
         ; eco         = cmpopts.cmpo_noeco
         ; gccompact   = cmpopts.cmpo_compact
-        ; gendoc      = cmpopts.cmpo_doc }
+        ; gendoc      = false
+        ; outdirp     = None }
 
       end
 
     | `Runtest _ ->
         (* Eagerly executed *)
         assert false
+    
+    | `GenDoc docopts -> begin
+        let name = docopts.doco_input in
 
+        begin try
+          let ext = Filename.extension name in
+          ignore (EcLoader.getkind ext : EcLoader.kind)
+        with EcLoader.BadExtension ext ->
+          Format.eprintf "do not know what to do with %s@." ext;
+          exit 1
+        end;
+
+        let prvoff =  {
+          prvo_maxjobs = None;
+          prvo_timeout = None;
+          prvo_cpufactor = None;
+          prvo_provers = None;
+          prvo_pragmas = [];
+          prvo_ppwidth = None;
+          prvo_checkall = false;
+          prvo_profile = false;
+          prvo_iterate = false;
+          prvo_why3server = None; } 
+        in
+
+        let terminal =
+          lazy (T.from_channel ~name (open_in name))
+        in
+
+        { prvopts     = prvoff
+        ; input       = Some name
+        ; terminal    = terminal
+        ; interactive = false
+        ; eco         = true
+        ; gccompact   = None
+        ; gendoc      = true
+        ; outdirp     = docopts.doco_outdirp }
+      end
+
+      
   in
 
   (match state.input with
@@ -679,7 +721,7 @@ let main () =
             if not state.eco then
               finalize_input state.input (EcCommands.current ());
             if state.gendoc then
-              EcDoc.generate_html state.input (EcCommands.current ());
+              EcDoc.generate_html ?outdirp:state.outdirp state.input (EcCommands.current ());
             exit 0
           end;
       with

src/ecDoc.ml

@@ -290,14 +290,25 @@ let emit_pages (dp : string) (th : string) (tstr : string) (gdoc : string list)
 
 (* -------------------------------------------------------------------- *)
 (* input = input name, scope contains all documentation items *)
-let generate_html (fname : string option) (scope : EcScope.scope) : unit =
+let generate_html ?(outdirp : string option) (fname : string option) (scope : EcScope.scope) : unit =
   match fname with
   | Some fn ->
       let kind =
         try  EcLoader.getkind (Filename.extension fn)
         with EcLoader.BadExtension _ -> assert false 
       in
-      let dp, fn = Filename.dirname fn, Filename.basename fn in
+      let dp =
+        match outdirp with
+        | None -> Filename.dirname fn
+        | Some outdirp -> 
+          try
+            if Sys.is_directory outdirp
+            then outdirp
+            else raise (Invalid_argument (Format.sprintf "%s is not an existing directory." outdirp))
+          with
+          | _ as ex -> Printf.eprintf "Exception: %s\n." (Printexc.to_string ex); raise ex
+      in
+      let fn = Filename.basename fn in
       let th = Filename.remove_extension fn in
       let tstr = thkind_str kind  ^ " " ^ th in
       begin

src/ecDoc.mli

@@ -1,2 +1,2 @@
 (* -------------------------------------------------------------------- *)
-val generate_html : string option -> EcScope.scope -> unit
+val generate_html : ?outdirp:string -> string option -> EcScope.scope -> unit

src/ecOptions.ml

@@ -9,6 +9,7 @@ type command = [
   | `Config
   | `Runtest of run_option
   | `Why3Config
+  | `GenDoc  of doc_option 
 ]
 
 and options = {
@@ -24,7 +25,6 @@ and cmp_option = {
   cmpo_tstats  : string option;
   cmpo_noeco   : bool;
   cmpo_script  : bool;
-  cmpo_doc     : bool;
 }
 
 and cli_option = {
@@ -41,6 +41,11 @@ and run_option = {
   runo_rawargs   : string list;
 }
 
+and doc_option = {
+  doco_input     : string;
+  doco_outdirp   : string option;
+}
+
 and prv_options = {
   prvo_maxjobs    : int option;
   prvo_timeout    : int option;
@@ -342,8 +347,7 @@ let specs = {
       `Spec  ("tstats" , `String, "Save timing statistics to <file>");
       `Spec  ("script" , `Flag  , "Computer-friendly output");
       `Spec  ("no-eco" , `Flag  , "Do not cache verification results");
-      `Spec  ("compact", `Int   , "<internal>");
-      `Spec  ("doc"    , `Flag  , "Generate documentation")]);
+      `Spec  ("compact", `Int   , "<internal>")]);
 
     ("cli", "Run EasyCrypt top-level", [
       `Group "loader";
@@ -361,6 +365,10 @@ let specs = {
     ]);
 
     ("why3config", "Configure why3", []);
+    
+    ("gendoc", "Generate documentation", [
+      `Spec ("odir", `String, "Output documentation files in <dir>")
+    ]);
   ];
 
   xp_groups = [
@@ -508,8 +516,7 @@ let cmp_options_of_values ini values input =
     cmpo_compact = get_int "compact" values;
     cmpo_tstats  = get_string "tstats" values;
     cmpo_noeco   = get_flag "no-eco" values;
-    cmpo_script  = get_flag "script" values;
-    cmpo_doc     = get_flag "doc" values;  }
+    cmpo_script  = get_flag "script" values; }
 
 let runtest_options_of_values ini values (input, scenarios) =
   { runo_input     = input;
@@ -519,6 +526,10 @@ let runtest_options_of_values ini values (input, scenarios) =
     runo_jobs      = get_int "jobs" values;
     runo_rawargs   = get_strings "raw-args" values; }
 
+let doc_options_of_values values input =
+  { doco_input     = input;
+    doco_outdirp   = get_string "odir" values; }
+
 (* -------------------------------------------------------------------- *)
 let parse getini argv =
   let (command, values, anons) = parse specs argv in
@@ -578,8 +589,20 @@ let parse getini argv =
 
         (cmd, ini, true)
 
-    | _ -> assert false
+    | "gendoc" -> 
+      begin
+        match anons with
+        | [input] ->
+          let ini = getini None in
+          let cmd = `GenDoc (doc_options_of_values values input) in
+            (cmd, ini, true)
 
+        | _ ->
+          raise (Arg.Bad "this command takes a single input file as argument")
+      end
+
+    | _ -> assert false
+    
   in {
     o_options = glb_options_of_values ~env ini values;
     o_command = command;

src/ecOptions.mli

@@ -5,6 +5,7 @@ type command = [
   | `Config
   | `Runtest of run_option
   | `Why3Config
+  | `GenDoc of doc_option
 ]
 
 and options = {
@@ -20,7 +21,6 @@ and cmp_option = {
   cmpo_tstats  : string option;
   cmpo_noeco   : bool;
   cmpo_script  : bool;
-  cmpo_doc     : bool;
 }
 
 and cli_option = {
@@ -37,6 +37,11 @@ and run_option = {
   runo_rawargs   : string list;
 }
 
+and doc_option = {
+  doco_input     : string;
+  doco_outdirp   : string option;  
+}
+
 and prv_options = {
   prvo_maxjobs    : int option;
   prvo_timeout    : int option;