why3html : use jstree to display a nice tree

Fix il/li tag

Makefile.in

@@ -220,6 +220,7 @@ install_no_local::
 	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
 	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
 	cp -f share/images/*.png $(DATADIR)/why3/images
+	cp -rf share/javascript $(DATADIR)/why3/javascript
 	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
 	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang
 

share/javascript/themes/default/style.css

+/*
+ * jsTree default theme 1.0
+ * Supported features: dots/no-dots, icons/no-icons, focused, loading
+ * Supported plugins: ui (hovered, clicked), checkbox, contextmenu, search
+ */
+
+.jstree-default li, 
+.jstree-default ins { background-image:url("d.png"); background-repeat:no-repeat; background-color:transparent; }
+.jstree-default li { background-position:-90px 0; background-repeat:repeat-y; }
+.jstree-default li.jstree-last { background:transparent; }
+.jstree-default .jstree-open > ins { background-position:-72px 0; }
+.jstree-default .jstree-closed > ins { background-position:-54px 0; }
+.jstree-default .jstree-leaf > ins { background-position:-36px 0; }
+
+.jstree-default .jstree-hovered { background:#e7f4f9; border:1px solid #d8f0fa; padding:0 2px 0 1px; }
+.jstree-default .jstree-clicked { background:#beebff; border:1px solid #99defd; padding:0 2px 0 1px; }
+.jstree-default a .jstree-icon { background-position:-56px -19px; }
+.jstree-default a.jstree-loading .jstree-icon { background:url("throbber.gif") center center no-repeat !important; }
+
+.jstree-default.jstree-focused { background:#ffffee; }
+
+.jstree-default .jstree-no-dots li, 
+.jstree-default .jstree-no-dots .jstree-leaf > ins { background:transparent; }
+.jstree-default .jstree-no-dots .jstree-open > ins { background-position:-18px 0; }
+.jstree-default .jstree-no-dots .jstree-closed > ins { background-position:0 0; }
+
+.jstree-default .jstree-no-icons a .jstree-icon { display:none; }
+
+.jstree-default .jstree-search { font-style:italic; }
+
+.jstree-default .jstree-no-icons .jstree-checkbox { display:inline-block; }
+.jstree-default .jstree-no-checkboxes .jstree-checkbox { display:none !important; }
+.jstree-default .jstree-checked > a > .jstree-checkbox { background-position:-38px -19px; }
+.jstree-default .jstree-unchecked > a > .jstree-checkbox { background-position:-2px -19px; }
+.jstree-default .jstree-undetermined > a > .jstree-checkbox { background-position:-20px -19px; }
+.jstree-default .jstree-checked > a > .jstree-checkbox:hover { background-position:-38px -37px; }
+.jstree-default .jstree-unchecked > a > .jstree-checkbox:hover { background-position:-2px -37px; }
+.jstree-default .jstree-undetermined > a > .jstree-checkbox:hover { background-position:-20px -37px; }
+
+#vakata-dragged.jstree-default ins { background:transparent !important; }
+#vakata-dragged.jstree-default .jstree-ok { background:url("d.png") -2px -53px no-repeat !important; }
+#vakata-dragged.jstree-default .jstree-invalid { background:url("d.png") -18px -53px no-repeat !important; }
+#jstree-marker.jstree-default { background:url("d.png") -41px -57px no-repeat !important; text-indent:-100px; }
+
+.jstree-default a.jstree-search { color:aqua; }
+.jstree-default .jstree-locked a { color:silver; cursor:default; }
+
+#vakata-contextmenu.jstree-default-context, 
+#vakata-contextmenu.jstree-default-context li ul { background:#f0f0f0; border:1px solid #979797; -moz-box-shadow: 1px 1px 2px #999; -webkit-box-shadow: 1px 1px 2px #999; box-shadow: 1px 1px 2px #999; }
+#vakata-contextmenu.jstree-default-context li { }
+#vakata-contextmenu.jstree-default-context a { color:black; }
+#vakata-contextmenu.jstree-default-context a:hover, 
+#vakata-contextmenu.jstree-default-context .vakata-hover > a { padding:0 5px; background:#e8eff7; border:1px solid #aecff7; color:black; -moz-border-radius:2px; -webkit-border-radius:2px; border-radius:2px; }
+#vakata-contextmenu.jstree-default-context li.jstree-contextmenu-disabled a, 
+#vakata-contextmenu.jstree-default-context li.jstree-contextmenu-disabled a:hover { color:silver; background:transparent; border:0; padding:1px 4px; }
+#vakata-contextmenu.jstree-default-context li.vakata-separator { background:white; border-top:1px solid #e0e0e0; margin:0; }
+#vakata-contextmenu.jstree-default-context li ul { margin-left:-4px; }
+
+/* IE6 BEGIN */
+.jstree-default li, 
+.jstree-default ins,
+#vakata-dragged.jstree-default .jstree-invalid, 
+#vakata-dragged.jstree-default .jstree-ok, 
+#jstree-marker.jstree-default { _background-image:url("d.gif"); }
+.jstree-default .jstree-open ins { _background-position:-72px 0; }
+.jstree-default .jstree-closed ins { _background-position:-54px 0; }
+.jstree-default .jstree-leaf ins { _background-position:-36px 0; }
+.jstree-default a ins.jstree-icon { _background-position:-56px -19px; }
+#vakata-contextmenu.jstree-default-context ins { _display:none; }
+#vakata-contextmenu.jstree-default-context li { _zoom:1; }
+.jstree-default .jstree-undetermined a .jstree-checkbox { _background-position:-20px -19px; }
+.jstree-default .jstree-checked a .jstree-checkbox { _background-position:-38px -19px; }
+.jstree-default .jstree-unchecked a .jstree-checkbox { _background-position:-2px -19px; }
+/* IE6 END */
\ No newline at end of file

src/ide/html_session.ml

@@ -28,6 +28,16 @@ let allow_obsolete = ref true
 let opt_config = ref None
 let opt_context = ref false
 
+type style =
+  | Simple
+  | Jstree
+
+let opt_style = ref Jstree
+
+let set_opt_style = function
+  | "simple" -> opt_style := Simple
+  | "jstree" -> opt_style := Jstree
+  | _ -> assert false
 
 let spec = Arg.align [
   ("-I",
@@ -50,6 +60,9 @@ let spec = Arg.align [
   " 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'."
 ]
 
 
@@ -91,60 +104,80 @@ let env = read_config ~includes !opt_config
 
 open Util
 
-let print_prover fmt = function
-  | Detected_prover pd -> fprintf fmt "%s" pd.prover_name
-  | Undetected_prover s -> fprintf fmt "%s" s
-
-let print_proof_status fmt = function
-  | Undone -> fprintf fmt "Undone"
-  | Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr
-  | InternalFailure exn ->
-    fprintf fmt "Failure : %a"Exn_printer.exn_printer exn
-
-let print_proof_attempt fmt pa =
-  fprintf fmt "<il>%a : %a</il>"
-    print_prover pa.prover
-    print_proof_status pa.proof_state
-
-let rec print_transf fmt tr =
-  fprintf fmt "<il>%s : <ul>%a</ul></il>"
-    tr.transf_name
-    (Pp.print_list Pp.newline print_goal) tr.subgoals
-
-and print_goal fmt g =
-  fprintf fmt "<il>%s : <ul>%a%a</ul></il>"
-    g.goal_name
-    (Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
-       Pp.nothing print_proof_attempt)
-    g.external_proofs
-    (Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
-       Pp.nothing print_transf)
-    g.transformations
-
-let print_theory fmt th =
-  fprintf fmt "<il>%s : <ul>%a</ul></il>"
-    th.theory_name
-    (Pp.print_list Pp.newline print_goal) th.goals
-
-let print_file fmt f =
-  fprintf fmt "<il>%s : <ul>%a</ul></il>"
-    f.file_name
-    (Pp.print_list Pp.newline print_theory) f.theories
-
-let print_session fmt s =
-  fprintf fmt "<p><ul>%a</ul></p>"
-    (Pp.print_list Pp.newline print_file) s
 
 type context =
-    ((formatter -> Session_ro.session -> unit)
-     -> Session_ro.session -> unit, formatter, unit) format
+    (string ->
+     (formatter -> Session_ro.session -> unit) -> Session_ro.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_project_dir ~allow_obsolete ~env session_path 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
+  else print_session basename fmt session;
+  pp_print_flush fmt ();
+  if output_dir <> "-" then close_out cout
+
+
+module Simple =
+struct
+
+  let print_prover fmt = function
+    | Detected_prover pd -> fprintf fmt "%s" pd.prover_name
+    | Undetected_prover s -> fprintf fmt "%s" s
+
+  let print_proof_status fmt = function
+    | Undone -> fprintf fmt "Undone"
+    | Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr
+    | InternalFailure exn ->
+      fprintf fmt "Failure : %a"Exn_printer.exn_printer exn
 
-let simple_context : context = "<!DOCTYPE html
+  let print_proof_attempt fmt pa =
+    fprintf fmt "<li>%a : %a</li>"
+      print_prover pa.prover
+      print_proof_status pa.proof_state
+
+  let rec print_transf fmt tr =
+    fprintf fmt "<li>%s : <ul>%a</ul></li>"
+      tr.transf_name
+      (Pp.print_list Pp.newline print_goal) tr.subgoals
+
+  and print_goal fmt g =
+    fprintf fmt "<li>%s : <ul>%a%a</ul></li>"
+      g.goal_name
+      (Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
+         Pp.nothing print_proof_attempt)
+      g.external_proofs
+      (Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
+         Pp.nothing print_transf)
+      g.transformations
+
+  let print_theory fmt th =
+    fprintf fmt "<li>%s : <ul>%a</ul></li>"
+      th.theory_name
+      (Pp.print_list Pp.newline print_goal) th.goals
+
+  let print_file fmt f =
+    fprintf fmt "<li>%s : <ul>%a</ul></li>"
+      f.file_name
+      (Pp.print_list Pp.newline print_theory) f.theories
+
+  let print_session _name fmt s =
+    fprintf fmt "<ul>%a</ul>"
+      (Pp.print_list Pp.newline print_file) s
+
+
+  let context : context = "<!DOCTYPE html
 PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
 \"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
 <html xmlns=\"http://www.w3.org/1999/xhtml\">
 <head>
-<title>A template for why3html</title>
+<title>Why3 session of %s</title>
 </head>
 <body>
 %a
@@ -152,18 +185,142 @@ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
 </html>
 "
 
-let run_file f =
-  let session_path = get_project_dir f in
-  let session = read_project_dir ~allow_obsolete ~env session_path in
-  let cout = if output_dir = "-" then stdout else
-      let basename = Filename.basename session_path in
-      open_out (Filename.concat output_dir (basename^".html")) in
-  let fmt = formatter_of_out_channel cout in
-  if !opt_context
-  then fprintf fmt simple_context print_session session
-  else print_session fmt session;
-  pp_print_flush fmt ();
-  if output_dir <> "-" then close_out cout
+  let run_files () =
+  Queue.iter (run_file context print_session) files
 
+end
 
-let () = Queue.iter run_file files
+module Jstree =
+struct
+
+  let print_prover fmt = function
+    | Detected_prover pd -> fprintf fmt "%s" pd.prover_name
+    | Undetected_prover s -> fprintf fmt "%s" s
+
+  let print_proof_status fmt = function
+    | Undone -> fprintf fmt "Undone"
+    | Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr
+    | InternalFailure exn ->
+      fprintf fmt "Failure : %a"Exn_printer.exn_printer exn
+
+  let print_proof_attempt fmt pa =
+    fprintf fmt "@[<hov><li rel='prover' ><a href='#'>%a : %a</a></li>@]"
+      print_prover pa.prover
+      print_proof_status pa.proof_state
+
+  let rec print_transf fmt tr =
+    fprintf fmt
+      "@[<hov><li rel='transf'><a href='#'>%s</a>@,<ul>%a</ul></li>@]"
+      tr.transf_name
+      (Pp.print_list Pp.newline print_goal) tr.subgoals
+
+  and print_goal fmt g =
+    fprintf fmt
+      "@[<hov><li rel='goal'><a href='#'>%s</a>@,<ul>%a%a</ul></li>@]"
+      g.goal_name
+      (Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
+         Pp.nothing print_proof_attempt)
+      g.external_proofs
+      (Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
+         Pp.nothing print_transf)
+      g.transformations
+
+  let print_theory fmt th =
+    fprintf fmt
+      "@[<hov><li rel='theory'><a href='#'>%s</a>@,<ul>%a</ul></li>@]"
+      th.theory_name
+      (Pp.print_list Pp.newline print_goal) th.goals
+
+  let print_file fmt f =
+    fprintf fmt "@[<hov><li rel='file'><a href='#'>%s</a>@,<ul>%a</ul></li>@]"
+      f.file_name
+      (Pp.print_list Pp.newline print_theory) f.theories
+
+  let print_session_aux name fmt s =
+    fprintf fmt "@[<hov><ul><a href='#'>%s</a>@,%a</ul>@]"
+      name
+      (Pp.print_list Pp.newline print_file) s
+
+
+  let print_session name fmt s =
+    fprintf fmt
+      "<a href='#' onclick=\"$('#%s_session').jstree('open_all');\">
+expand all
+</a> <a href='#' onclick=\"$('#%s_session').jstree('close_all');\">
+close all
+</a>
+<div id=\"%s_session\" class=\"session\">
+%a
+</div>
+<script type=\"text/javascript\" class=\"source\">
+$(function () {
+  $(\"#%s_session\").jstree({ 
+      \"types\" : {
+	   \"types\" : {
+	   \"file\" : {
+		\"icon\" : { \"image\" : \"images/folder16.png\"},
+		      },
+	   \"theory\" : {
+		\"icon\" : { \"image\" : \"images/folder16.png\"},
+		      },
+	   \"goal\" : {
+		\"icon\" : { \"image\" : \"images/file16.png\"},
+		      },
+	   \"prover\" : {
+		\"icon\" : { \"image\" : \"images/wizard16.png\"},
+		      },
+	   \"transf\" : {
+		\"icon\" : { \"image\" : \"images/configure16.png\"},
+		      },
+                        }
+                },
+      \"plugins\" : [\"themes\",\"html_data\",\"types\"]
+        });
+});
+</script>
+"
+  name name name (print_session_aux name) s name
+
+
+  let context : context = "<!DOCTYPE html
+PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
+\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
+<html xmlns=\"http://www.w3.org/1999/xhtml\">
+<head>
+    <meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />
+    <title>Why3 session of %s</title>
+    <script type=\"text/javascript\" src=\"javascript/jquery.js\"></script>
+    <script type=\"text/javascript\" src=\"javascript/jquery.jstree.js\">
+    </script>
+</head>
+<body>
+%a
+</body>
+</html>
+"
+
+  let run_files () =
+    Queue.iter (run_file context print_session) files;
+    if !opt_context then
+      let data_dir = Whyconf.datadir (Whyconf.get_main env.config) in
+      (** copy images *)
+      let img_dir_src = Filename.concat data_dir "images" in
+      let img_dir_dst = Filename.concat output_dir "images" in
+      if not (Sys.file_exists img_dir_dst) then Unix.mkdir img_dir_dst 0o755;
+      List.iter (fun img_name ->
+        let from = Filename.concat img_dir_src img_name in
+        let to_  = Filename.concat img_dir_dst img_name in
+        Sysutil.copy_file from to_)
+        ["folder16.png";"file16.png";"wizard16.png";"configure16.png"];
+      (** copy javascript *)
+      let js_dir_src = Filename.concat data_dir "javascript" in
+      let js_dir_dst = Filename.concat output_dir "javascript" in
+      Sysutil.copy_dir js_dir_src js_dir_dst
+
+end
+
+
+let () =
+  match !opt_style with
+    | Simple -> Simple.run_files ()
+    | Jstree -> Jstree.run_files ()

src/ide/session_ro.mli

@@ -73,7 +73,9 @@ and proof_attempt = private
   }
     (** a proof attempt for a given goal *)
 
-type env
+type env =
+  { env : Env.env;
+    config : Whyconf.config}
 
 val read_config : ?includes:string list -> string option -> env
 (** [read_config ~includes conf_path] read the configuration located in

src/util/sysutil.ml

@@ -120,6 +120,18 @@ let copy_file from to_ =
     output cout buff 0 !n
   done
 
+let rec copy_dir from to_ =
+  if not (Sys.file_exists to_) then Unix.mkdir to_ 0o755;
+  let files = Sys.readdir from in
+  let copy fname =
+    let src = Filename.concat from fname in
+    let dst = Filename.concat to_ fname in
+    if Sys.is_directory src
+    then copy_dir src dst
+    else copy_file src dst in
+  Array.iter copy files
+
+
 (* return the absolute path of a given file name.
    this code has been designed to be architecture-independant so
    be very careful if you modify this *)
@@ -183,5 +195,6 @@ let absolutize_filename dirname f =
 (*
 let p1 = relativize_filename "/bin/bash" "src/f.why"
 
-let p1 = relativize_filename "test" "/home/cmarche/recherche/why3/src/ide/f.why"
+let p1 = relativize_filename "test"
+  "/home/cmarche/recherche/why3/src/ide/f.why"
 *)

src/util/sysutil.mli

@@ -62,6 +62,12 @@ val call_asynchronous : (unit -> 'a) -> (unit -> 'a)
 val copy_file : string -> string -> unit
 (** [copy_file from to] copy the file from [from] to [to] *)
 
+val copy_dir : string -> string -> unit
+(** [copy_dir from to] copy the directory recursively from [from] to [to],
+    currently the directory must contains only directories and common files
+*)
+
+
 val path_of_file : string -> string list
 (** [path_of_file filename] return the absolute path of [filename] *)