why3html : allow to display the edited files (for example .v)

share/javascript/session.css

@@ -4,4 +4,13 @@
 
 .notverified{
     color: red;
-}
\ No newline at end of file
+}
+
+#edited{
+   right:0px;
+   top: 20px;
+   position: fixed;
+   z-index: 50;
+   width: 50%;
+   height: 600px;
+}

share/javascript/session.js

+function showedited(s){
+    var iframe = document.getElementById("edited");
+    var addr = "edited/"+s;
+    iframe.src = addr;
+    $("#edited").show()
+}
\ No newline at end of file

src/ide/html_session.ml

@@ -39,6 +39,15 @@ let set_opt_style = function
   | "jstree" -> opt_style := Jstree
   | _ -> assert false
 
+let opt_pp = ref []
+
+let set_opt_pp_in,set_opt_pp_cmd,set_opt_pp_out =
+  let suf = ref "" in
+  let cmd = ref "" in
+  (fun s -> suf := s),
+  (fun s -> cmd := s),
+  (fun s -> opt_pp := (!suf,(!cmd,s))::!opt_pp)
+
 let spec = Arg.align [
   ("-I",
    Arg.String (fun s -> includes := s :: !includes),
@@ -62,7 +71,19 @@ let spec = Arg.align [
     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'."
+    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 ()->
+    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'"
 ]
 
 
@@ -84,6 +105,10 @@ let () =
     exit 0
   end
 
+(* let () = *)
+(*   List.iter (fun (in_,(cmd,out)) -> *)
+(*     printf "in : %s, cmd : %s, out : %s@." in_ cmd out) !opt_pp *)
+
 let output_dir =
   match !output_dir with
     | "" -> printf
@@ -95,6 +120,8 @@ let output_dir =
       exit 1
     | _ -> !output_dir
 
+let edited_dst = Filename.concat output_dir "edited"
+
 let allow_obsolete = !allow_obsolete
 let includes = List.rev !includes
 
@@ -210,10 +237,53 @@ struct
       fprintf fmt "<span class='notverified'>Failure : %a</span>"
         Exn_printer.exn_printer exn
 
+  let cmd_regexp = Str.regexp "%\\(.\\)"
+
+  let pp_run input cmd output =
+    let replace s = match Str.matched_group 1 s with
+      | "%" -> "%"
+      | "i" -> input
+      | "o" -> output
+      | _ -> failwith "unknown format specifier, use %%i, %%o"
+    in
+    let cmd = Str.global_substitute cmd_regexp replace cmd in
+    let c = Sys.command cmd in
+    if c <> 0 then
+      eprintf "[Error] '%s' stopped abnormaly : code %i" cmd c
+
+  let find_pp edited =
+    let basename = Filename.basename edited in
+    try
+      let suff,(cmd,suff_out) =
+        List.find (fun (s,_) -> ends_with basename s) !opt_pp in
+      let base =
+        String.sub basename 0 (String.length basename - String.length suff) in
+      let base_dst = (base^suff_out) in
+      if !opt_context then
+        pp_run edited cmd (Filename.concat edited_dst base_dst);
+      base_dst
+    with Not_found ->
+      eprintf "Default %s@." basename;
+      (** default printer *)
+      let base = try Filename.chop_extension basename with _ -> basename in
+      let base_dst = base^".txt" in
+      if !opt_context then
+        Sysutil.copy_file edited (Filename.concat edited_dst base_dst);
+      base_dst
+
   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
+    match pa.edited_as with
+      | None ->
+        fprintf fmt "@[<hov><li rel='prover' ><a href='#'>%a : %a</a></li>@]"
+          print_prover pa.prover
+          print_proof_status pa.proof_state
+      | Some f ->
+        let output = find_pp f in
+        fprintf fmt "@[<hov><li rel='prover' ><a href='#' \
+onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
+          output
+          print_prover pa.prover
+          print_proof_status pa.proof_state
 
   let rec print_transf fmt tr =
     fprintf fmt
@@ -308,16 +378,28 @@ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
     <link rel=\"stylesheet\" type=\"text/css\"
      href=\"javascript/session.css\" />
     <script type=\"text/javascript\" src=\"javascript/jquery.js\"></script>
-    <script type=\"text/javascript\" src=\"javascript/jquery.jstree.js\">
-    </script>
+    <script type=\"text/javascript\" src=\"javascript/jquery.jstree.js\">\
+</script>
+    <script type=\"text/javascript\" src=\"javascript/session.js\">\
+</script>
 </head>
 <body>
 %a
+<iframe src=\"\"  id='edited'>
+<p>Your browser does not support iframes.</p>
+</iframe>
+<script type=\"text/javascript\" class=\"source\">
+$(function () {
+  $('#edited').hide()
+})
+</script>
 </body>
 </html>
 "
 
   let run_files () =
+    if !opt_context then
+      if not (Sys.file_exists edited_dst) then Unix.mkdir edited_dst 0o755;
     Queue.iter (run_file context print_session) files;
     if !opt_context then
       let data_dir = Whyconf.datadir (Whyconf.get_main env.config) in

src/ide/session_ro.ml

@@ -98,11 +98,11 @@ struct
 end
 
 
-module Read_project (O : Session.OBSERVER) =
+module Read_project (O : Session.OBSERVER)
+  (P : sig val project_dir : string end) =
 struct
   module M = Session.Make(Observer_dumb)
 
-
   let read_prover_option = function
     | M.Detected_prover pd -> Detected_prover
       { prover_name = pd.Session.prover_name;
@@ -120,7 +120,7 @@ struct
   let read_edited_as prover ea =
     match prover, ea with
       | (_, "") | (M.Detected_prover {Session.interactive = false},_) -> None
-      | _ -> Some ea
+      | _ -> Some (Filename.concat P.project_dir ea)
 
   let rec read_trans key transf acc =
     Mstr.add key
@@ -161,19 +161,20 @@ struct
       theories = List.map read_theory file.M.theories;
       file_verified = file.M.file_verified}
 
-  let read_project_dir ~allow_obsolete ~env project_dir =
+  let read_project_dir ~allow_obsolete ~env =
     let init _ _ = () in
     let notify _ = () in
     let _found_obs = M.open_session ~allow_obsolete
-        ~env:env.env ~config:env.config ~init ~notify project_dir
+        ~env:env.env ~config:env.config ~init ~notify P.project_dir
     in
     List.map read_file (M.get_all_files ())
 
 end
 
 let read_project_dir ~allow_obsolete ~env project_dir =
-  let module Rp = Read_project(Observer_dumb) in
-  Rp.read_project_dir ~allow_obsolete ~env project_dir
+  let module Rp = Read_project(Observer_dumb)
+        (struct let project_dir = project_dir end)in
+  Rp.read_project_dir ~allow_obsolete ~env
 
 
 open Format

src/util/util.ml

@@ -191,6 +191,14 @@ let split_string_rev s c =
       | Invalid_argument _ -> ""::acc in
   aux [] 0
 
+let ends_with s suf =
+  let rec aux s suf suflen offset i =
+    i >= suflen || (s.[i + offset] = suf.[i]
+                   && aux s suf suflen offset (i+1)) in
+  let slen = String.length s in
+  let suflen = String.length suf in
+  slen >= suflen && aux s suf suflen (slen - suflen) 0
+
 (** usefule function on char *)
 let is_uppercase c = 'A' <= c && c <= 'Z'
 

src/util/util.mli

@@ -135,6 +135,9 @@ val ttrue : 'a -> bool
 (* useful function on string *)
 val split_string_rev : string -> char -> string list
 
+val ends_with : string -> string -> bool
+(** test if a string ends with another *)
+
 (* useful function on char *)
 val is_uppercase : char -> bool