restored html output with style simple, style jstree missing

ROADMAP

@@ -90,7 +90,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
 == New Features to annouce ==
 
 * Coq Realizations
-* tool why3session with -latex, -html, -stats, etc
+* tool why3session with commands latex, html, stats, etc
 * tool why3doc
 * Support for several versions of the same prover
 * Improved IDE:

src/why3session/why3session_html.ml

@@ -19,20 +19,14 @@
 
 open Format
 open Why3
-module C = Whyconf
+open Why3session_lib
 
-let files = Queue.create ()
-let opt_version = ref false
 let output_dir = ref ""
-let allow_obsolete = ref true
-let opt_config = ref None
 let opt_context = ref false
 
-type style =
-  | Simple
-  | Jstree
+type style = Simple | Jstree
 
-let opt_style = ref Jstree
+let opt_style = ref Simple
 
 let set_opt_style = function
   | "simple" -> opt_style := Simple
@@ -48,44 +42,30 @@ let set_opt_pp_in,set_opt_pp_cmd,set_opt_pp_out =
   (fun s -> cmd := s),
   (fun s -> opt_pp := (!suf,(!cmd,s))::!opt_pp)
 
-let spec = Arg.align [
-  ("-v",
-   Arg.Set opt_version,
-   " Print version information") ;
+let spec =
   ("-o",
    Arg.Set_string output_dir,
-   " The directory to output the files ('-' for stdout)");
-  ("--strict",
-   Arg.Clear allow_obsolete,
-   " Forbid obsolete session");
-  "-C", Arg.String (fun s -> opt_config := Some s),
-      "<file> Read configuration from <file>";
-  "--config", Arg.String (fun s -> opt_config := Some s),
-      " Same as -C";
-  "--context", Arg.Set opt_context,
-  " Add context around the generated code in order to allow direct \
+   " The directory to output the files ('-' for stdout)") ::
+  ("--context", Arg.Set opt_context,
+   " Add context around the generated code in order to allow direct \
     visualisation (header, css, ...). It also add in the directory \
-    all the needed external file. It can't be set with stdout output";
-  "--style", Arg.Symbol (["simple";"jstree"], set_opt_style),
-  " Set the style to use. 'simple' use only 'ul' and 'il' tag. 'jstree' use \
-    the 'jstree' plugin of the javascript library 'jquery'.";
-  "--add_pp", Arg.Tuple
+    all the needed external file. It can't be set with stdout output") ::
+  ("--style", Arg.Symbol (["simple";"jstree"], set_opt_style),
+   " Set the style to use. 'simple' use only 'ul' and 'il' tag. 'jstree' use \
+    the 'jstree' plugin of the javascript library 'jquery'.") ::
+  ("--add_pp", Arg.Tuple
     [Arg.String set_opt_pp_in;
      Arg.String set_opt_pp_cmd;
      Arg.String set_opt_pp_out],
   "<suffix> <cmd> <out_suffix> \
 Add for the given prefix the given pretty-printer, \
 the new file as the given out_suffix. cmd must contain '%i' which will be \
-replace by the input file and '%o' which will be replaced by the output file.";
-    "--coqdoc",
-  Arg.Unit (fun ()->
+replace by the input file and '%o' which will be replaced by the output file.") ::
+  ("--coqdoc",
+   Arg.Unit (fun ()->
     opt_pp := (".v",("coqdoc --no-index --html -o %o %i",".html"))::!opt_pp),
-  " same as '--add_pp .v \"coqdoc --no-index --html -o %o %i\" .html'";
-    Debug.Opt.desc_debug_list;
-    Debug.Opt.desc_debug_all;
-    Debug.Opt.desc_debug;
-]
-
+  " same as '--add_pp .v \"coqdoc --no-index --html -o %o %i\" .html'") ::
+  simple_spec
 
 (*
 let version_msg = sprintf
@@ -117,22 +97,22 @@ let () =
   if  Debug.Opt.option_list () then exit 0
 *)
 
+(*
 let output_dir =
   match !output_dir with
- (*
-   | "" -> 
+   | "" ->
       printf "Error: output_dir must be set@.";
       exit 1
     | "-" when !opt_context ->
       printf
         "Error: context and stdout output can't be set at the same time@.";
       exit 1
- *)
     | _ -> !output_dir
 
 let edited_dst = Filename.concat output_dir "edited"
 
 let whyconf = Whyconf.read_config !opt_config
+  *)
 
 open Session
 open Util
@@ -142,12 +122,17 @@ type context =
      (formatter -> notask session -> unit) -> notask session
      -> unit, formatter, unit) format
 
-let run_file (context : context) print_session f =
-  let session_path = get_project_dir f in
-  let basename = Filename.basename session_path in
-  let session = read_session session_path in
-  let cout = if output_dir = "-" then stdout else
-      open_out (Filename.concat output_dir (basename^".html")) in
+let run_file (context : context) print_session fname =
+  let project_dir = Session.get_project_dir fname in
+  let session = Session.read_session project_dir in
+  let output_dir =
+    if !output_dir = "" then project_dir else !output_dir
+  in
+  let basename = Filename.basename project_dir in
+  let cout =
+    if output_dir = "-" then stdout else
+      open_out (Filename.concat output_dir (basename^".html"))
+  in
   let fmt = formatter_of_out_channel cout in
   if !opt_context
   then fprintf fmt context basename (print_session basename) session
@@ -216,11 +201,12 @@ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
 </html>
 "
 
-  let run_files () =
-  Queue.iter (run_file context print_session) files
+  let run_one = run_file context print_session
 
 end
 
+(*
+
 module Jstree =
 struct
 
@@ -343,7 +329,7 @@ close all
 </div>
 <script type=\"text/javascript\" class=\"source\">
 $(function () {
-  $(\"#%s_session\").jstree({ 
+  $(\"#%s_session\").jstree({
       \"types\" : {
 	   \"types\" : {
 	   \"file\" : {
@@ -421,16 +407,16 @@ $(function () {
       Sysutil.copy_dir js_dir_src js_dir_dst
 
 end
+*)
 
 
-(*
-let () =
+let run_one fname =
   match !opt_style with
-    | Simple -> Simple.run_files ()
-    | Jstree -> Jstree.run_files ()
-*)
-
-let run_one _fname = ()
+    | Simple -> Simple.run_one fname
+    | Jstree ->
+      eprintf "style jstree not yet available@.";
+      exit 1
+      (* Jstree.run_files () *)
 
 open Why3session_lib
 
@@ -446,3 +432,10 @@ let cmd =
     cmd_name = "html";
     cmd_run  = run;
   }
+
+
+(*
+Local Variables:
+compile-command: "unset LANG; make -C ../.. bin/why3session.byte"
+End:
+*)