why3doc: new option --stdlib-url to add links for files found in load path

parent 1d18fce0
...@@ -1189,7 +1189,7 @@ STDLIBS = bool comparison relations \ ...@@ -1189,7 +1189,7 @@ STDLIBS = bool comparison relations \
option list map set bag graph option list map set bag graph
# function ? sum ? tptp ? # function ? sum ? tptp ?
STDMODS = ref array arith hashtbl impset pqueue queue random stack string STDMODS = ref array arith hashtbl impset pqueue queue random stack string
STDLIBFILES = $(addsuffix .why, $(addprefix theories/, $(STDLIBS))) STDLIBFILES = $(addsuffix .why, $(addprefix theories/, $(STDLIBS)))
STDMODFILES = $(addsuffix .mlw, $(addprefix modules/, $(STDMODS))) STDMODFILES = $(addsuffix .mlw, $(addprefix modules/, $(STDMODS)))
......
...@@ -146,7 +146,8 @@ See manual Section xx ...@@ -146,7 +146,8 @@ See manual Section xx
- add tag 0.72 to the git repository (do not forget to push it) - add tag 0.72 to the git repository (do not forget to push it)
* put on the web page * put on the web page
- why3-0.72.tar.gz - why3-0.72.tar.gz
- standard library online, using why3doc (make stdlibdoc), to http://why3.lri.fr/stdlib/ - standard library online, using why3doc (make stdlibdoc),
to http://why3.lri.fr/stdlib/
- API doc, produced using ocamldoc (make apidoc), to http://why3.lri.fr/api/ - API doc, produced using ocamldoc (make apidoc), to http://why3.lri.fr/api/
Note: check that URL of API doc is correct in doc/api.tex line 9. Note: check that URL of API doc is correct in doc/api.tex line 9.
- update the main HTML page (sources are in why3-papers/www) - update the main HTML page (sources are in why3-papers/www)
......
...@@ -839,6 +839,8 @@ identifier use to its definition. ...@@ -839,6 +839,8 @@ identifier use to its definition.
\item Option \texttt{-o \textsl{<dir>}} defines the directory where to \item Option \texttt{-o \textsl{<dir>}} defines the directory where to
output the HTML files output the HTML files
\item Option \verb|--output| is the same as \verb|-o| \item Option \verb|--output| is the same as \verb|-o|
\item Option \verb|--stdlib-url|~\textsl{url} sets a URL for files
found in load path, so that links to definitions can be added
\end{itemize} \end{itemize}
\paragraph{Typesetting textual comments} \paragraph{Typesetting textual comments}
......
...@@ -24,6 +24,11 @@ open Ident ...@@ -24,6 +24,11 @@ open Ident
let loadpath = ref [] let loadpath = ref []
let set_loadpath l = loadpath := l let set_loadpath l = loadpath := l
let is_in_path fname =
List.mem (Filename.dirname fname) !loadpath
let stdlib_url = ref None
let set_stdlib_url u = stdlib_url := Some u
let output_dir = ref None let output_dir = ref None
let set_output_dir d = output_dir := d let set_output_dir d = output_dir := d
...@@ -36,36 +41,57 @@ let output_file fname = ...@@ -36,36 +41,57 @@ let output_file fname =
in in
base ^ ".html" base ^ ".html"
type url = string
type tag = string type tag = string
type file_kind = Local | Loadpath | Unknown
type file = { type file = {
tags: (int * int, tag) Hashtbl.t; (* line, column -> tag *) tags: (int * int, tag) Hashtbl.t; (* line, column -> tag *)
kind: file_kind;
} }
let files = Hashtbl.create 17 let files = Hashtbl.create 17
let add_file fname = let add_file fname =
Hashtbl.add files fname { tags = Hashtbl.create 17 } Hashtbl.add files fname { tags = Hashtbl.create 17; kind = Local }
let get_file fname =
try
Hashtbl.find files fname
with Not_found ->
let k = if is_in_path fname then Loadpath else Unknown in
let f = { tags = Hashtbl.create 17; kind = k } in
Hashtbl.add files fname f;
f
let make_tag s l =
s ^ "_" ^ string_of_int l (* TODO: improve? *)
let add_ident id = match id.id_loc with let add_ident id = match id.id_loc with
| None -> | None ->
() ()
| Some loc -> | Some loc ->
let f, l, c, _ = Loc.get loc in let f, l, c, _ = Loc.get loc in
try let f = get_file f in
let f = Hashtbl.find files f in let t = make_tag id.id_string l in
let t = id.id_string ^ "_" ^ string_of_int l in (* TODO: improve? *) Hashtbl.add f.tags (l, c) t
Hashtbl.add f.tags (l, c) t
with Not_found ->
()
let is_def (fn, l, c) = let is_def (fn, l, c) =
let f = Hashtbl.find files fn in let f = get_file fn in
Hashtbl.find f.tags (l, c) Hashtbl.find f.tags (l, c)
let make_url fn =
let url = Filename.basename fn ^ ".html" in
match (get_file fn).kind, !stdlib_url with
| Local, _ -> url
| Loadpath, Some www -> www ^ "/" ^ url
| _ -> raise Not_found
let locate id = match id.id_loc with let locate id = match id.id_loc with
| None -> | None ->
raise Not_found raise Not_found
| Some loc -> | Some loc ->
let fn, l, c, _ = Loc.get loc in let fn, l, _, _ = Loc.get loc in
(Filename.basename fn ^ ".html"), is_def (fn, l, c) make_url fn, make_tag id.id_string l
...@@ -26,6 +26,7 @@ open Ident ...@@ -26,6 +26,7 @@ open Ident
val set_loadpath: string list -> unit val set_loadpath: string list -> unit
val set_output_dir: string option -> unit val set_output_dir: string option -> unit
val set_stdlib_url: string -> unit
val output_file: string -> string val output_file: string -> string
...@@ -39,6 +40,8 @@ val is_def: string * int * int -> tag ...@@ -39,6 +40,8 @@ val is_def: string * int * int -> tag
(* if [loc] is a definition point, returns the corresponding tag, (* if [loc] is a definition point, returns the corresponding tag,
otrherwise raises [Not_found] *) otrherwise raises [Not_found] *)
val locate: ident -> string * tag type url = string
val locate: ident -> url * tag
(* or raises [Not_found] *) (* or raises [Not_found] *)
...@@ -42,6 +42,8 @@ let option_list = Arg.align [ ...@@ -42,6 +42,8 @@ let option_list = Arg.align [
"<dir> Print files in <dir>"; "<dir> Print files in <dir>";
"--output", Arg.String (fun s -> opt_output := Some s), "--output", Arg.String (fun s -> opt_output := Some s),
" same as -o"; " same as -o";
"--stdlib-url", Arg.String Doc_def.set_stdlib_url,
"<url> Add links to <url> for files found on loadpath";
] ]
let add_opt_file x = Queue.add x opt_queue let add_opt_file x = Queue.add x opt_queue
...@@ -56,8 +58,7 @@ let () = ...@@ -56,8 +58,7 @@ let () =
let css = let css =
let css_fname = "style.css" in let css_fname = "style.css" in
let css_full_fname = let css_full_fname = match !opt_output with
match !opt_output with
| None -> css_fname | None -> css_fname
| Some dir -> Filename.concat dir css_fname | Some dir -> Filename.concat dir css_fname
in in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment