why3doc: links to theories

parent 70f184d4
......@@ -147,7 +147,7 @@ why3.conf
/src/ide/xml.ml
# /src/why3doc/
/src/why3doc/to_html.ml
/src/why3doc/doc_lexer.ml
# /src/util/
/src/util/rc.ml
......
......@@ -966,9 +966,9 @@ install_no_local::
# why3doc
#########
WHY3DOCGENERATED = src/why3doc/to_html.ml
WHY3DOCGENERATED = src/why3doc/doc_lexer.ml
WHY3DOC_FILES = doc_html to_html doc_main
WHY3DOC_FILES = doc_html doc_def doc_lexer doc_main
WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES))
......
......@@ -20,20 +20,23 @@
open Ident
let glob = Hashtbl.create 5003
let flag = Debug.register_flag "glob"
let () = Debug.unset_flag flag (* make sure it is unset by default *)
let add id = match id.id_loc with
| None -> ()
| Some loc ->
let f, l, c, _ = Loc.get loc in
Format.eprintf "ADD GLOB: id=%s at %s/%d/%d@." id.id_string f l c;
Hashtbl.add glob (f, l, c) id
let dummy_id = id_register (id_fresh "dummy")
let def _id =
assert false (*TODO*)
let glob = Hashtbl.create 5003
(* could be improved with nested hash tables *)
let use _loc _id =
assert false (*TODO*)
let with_loc f = function
| None -> ()
| Some loc when loc = Loc.dummy_position -> ()
| Some loc -> f loc
let locate ~fname ~line ~column = Hashtbl.find glob (fname, line, column)
let use loc id =
let f, l, c, _ = Loc.get loc in
(* Format.eprintf "GLOB USE: id=%s at %s/%d/%d@." id.id_string f l c; *)
Hashtbl.add glob (f, l, c) id
let locate pos =
Hashtbl.find glob pos
......@@ -20,10 +20,13 @@
open Ident
val def: ident -> unit
(** [def id] registers the definition point for [id] *)
val flag: Debug.flag
val dummy_id: ident
val use: Loc.position -> ident -> unit
(** [add loc id] registers that [id] was used at position [loc] *)
val locate: fname:string -> line:int -> column:int -> ident
val locate: string * int * int -> ident
(** [locate pos] returns the ident used at position [pos], if any,
or raises [Not_found] *)
......@@ -171,19 +171,25 @@ let rec dty uc env = function
let ts = ts_tuple (List.length tyl) in
tyapp ts (List.map (dty uc env) tyl)
let find_ns find p ns =
let find_ns get_id find p ns =
let loc = qloc p in
let sl = string_list_of_qualid [] p in
try find ns sl
try
let r = find ns sl in
if Debug.test_flag Glob.flag then Glob.use loc (get_id r);
r
with Not_found -> error ~loc (UnboundSymbol sl)
let find_prop_ns = find_ns ns_find_pr
let get_id_prop p = p.pr_name
let find_prop_ns = find_ns get_id_prop ns_find_pr
let find_prop p uc = find_prop_ns p (get_namespace uc)
let find_tysymbol_ns = find_ns ns_find_ts
let get_id_ts ts = ts.ts_name
let find_tysymbol_ns = find_ns get_id_ts ns_find_ts
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)
let find_lsymbol_ns = find_ns ns_find_ls
let get_id_ls ls = ls.ls_name
let find_lsymbol_ns = find_ns get_id_ls ns_find_ls
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)
let find_fsymbol_ns q ns =
......@@ -197,7 +203,8 @@ let find_psymbol_ns q ns =
let find_fsymbol q uc = find_fsymbol_ns q (get_namespace uc)
let find_psymbol q uc = find_psymbol_ns q (get_namespace uc)
let find_namespace_ns = find_ns ns_find_ns
let get_dummy_id _ = Glob.dummy_id
let find_namespace_ns = find_ns get_dummy_id ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)
let specialize_lsymbol p uc =
......@@ -1170,6 +1177,7 @@ let add_use_clone env lenv th (loc, use, subst) =
let use_or_clone th =
let q, id = split_qualid use.use_theory in
let t = find_theory env lenv q id in
if Debug.test_flag Glob.flag then Glob.use (qloc use.use_theory) t.th_name;
match subst with
| None -> use_export th t
| Some s -> clone_export th t (type_inst th t s)
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2012 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Why3
open Ident
let loadpath = ref []
let set_loadpath l = loadpath := l
let output_dir = ref None
let set_output_dir d = output_dir := d
let output_file fname =
let f = Filename.basename fname in
let base = match !output_dir with
| None -> f
| Some dir -> Filename.concat dir f
in
base ^ ".html"
type tag = string
type file = {
tags: (int * int, tag) Hashtbl.t; (* line, column -> tag *)
}
let files = Hashtbl.create 17
let add_file fname =
Hashtbl.add files fname { tags = Hashtbl.create 17 }
let add_ident id = match id.id_loc with
| None ->
()
| Some loc ->
let f, l, c, _ = Loc.get loc in
try
let f = Hashtbl.find files f in
let t = id.id_string ^ "_" ^ string_of_int l in (* TODO: improve? *)
Hashtbl.add f.tags (l, c) t
with Not_found ->
()
let is_def (fn, l, c) =
let f = Hashtbl.find files fn in
Hashtbl.find f.tags (l, c)
let locate id = match id.id_loc with
| None ->
raise Not_found
| Some loc ->
let fn, l, c, _ = Loc.get loc in
output_file fn, is_def (fn, l, c)
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2012 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Why3
open Ident
(* records definition locations *)
val set_loadpath: string list -> unit
val set_output_dir: string option -> unit
val output_file: string -> string
val add_file: string -> unit
val add_ident: ident -> unit
type tag = string
val is_def: string * int * int -> tag
(* if [loc] is a definition point, returns the corresponding tag,
otrherwise raises [Not_found] *)
val locate: ident -> string * tag
(* or raises [Not_found] *)
......@@ -23,8 +23,14 @@
{
open Format
open Lexing
open Why3
let newline fmt () = fprintf fmt "\n"
let newline lexbuf fmt =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum };
fprintf fmt "\n"
let make_table l =
let ht = Hashtbl.create 97 in
......@@ -35,19 +41,23 @@
[ "theory"; "end";
"type"; "constant"; "function"; "predicate"; "inductive";
"clone"; "use";
"import"; "export"; "axiom"; "goal"; "lemma";]
"import"; "export"; "axiom"; "goal"; "lemma"; ]
let is_keyword2 = make_table
[ "match"; "with"; "let"; "in"; "if"; "then"; "else";
"forall"; "exists";
(* programs *)
"as"; "assert"; "begin";
"do"; "done"; "downto"; "else";
"exception"; "val"; "for"; "fun";
"if"; "in";
"module"; "mutable";
"rec"; "then"; "to";
"try"; "while"; "invariant"; "variant"; "raise"; "label";
]
"try"; "while"; "invariant"; "variant"; "raise"; "label"; ]
let get_loc lb =
let p = Lexing.lexeme_start_p lb in
p.pos_fname, p.pos_lnum, p.pos_cnum - p.pos_bol
}
......@@ -66,13 +76,26 @@ rule scan fmt = parse
else if is_keyword2 s then
fprintf fmt "<font class=\"keyword2\">%s</font>" s
else begin
(* let loc = get_loc lexbuf in *)
fprintf fmt "%s" s
let (* f,l,c as *) loc = get_loc lexbuf in
(* Format.eprintf " IDENT %s/%d/%d@." f l c; *)
(* is this a def point? *)
try
let t = Doc_def.is_def loc in
fprintf fmt "<a name=\"%s\">%s</a>" t s
with Not_found ->
(* is this a use point? *)
try
let id = Glob.locate loc in
let fn, t = Doc_def.locate id in
fprintf fmt "<a href=\"%s#%s\">%s</a>" fn t s
with Not_found ->
(* otherwise, just print it *)
fprintf fmt "%s" s
end;
scan fmt lexbuf }
| "<" { fprintf fmt "&lt;"; scan fmt lexbuf }
| "&" { fprintf fmt "&amp;"; scan fmt lexbuf }
| "\n" { newline fmt (); scan fmt lexbuf }
| "\n" { newline lexbuf fmt; scan fmt lexbuf }
| '"' { fprintf fmt "\""; string fmt lexbuf; scan fmt lexbuf }
| "'\"'"
| _ as s { fprintf fmt "%s" s; scan fmt lexbuf }
......@@ -81,7 +104,7 @@ and comment fmt = parse
| "(*" { fprintf fmt "(*"; comment fmt lexbuf; comment fmt lexbuf }
| "*)" { fprintf fmt "*)" }
| eof { () }
| "\n" { newline fmt (); comment fmt lexbuf }
| "\n" { newline lexbuf fmt; comment fmt lexbuf }
| '"' { fprintf fmt "\""; string fmt lexbuf; comment fmt lexbuf }
| "<" { fprintf fmt "&lt;"; comment fmt lexbuf }
| "&" { fprintf fmt "&amp;"; comment fmt lexbuf }
......@@ -89,6 +112,7 @@ and comment fmt = parse
| _ as s { fprintf fmt "%s" s; comment fmt lexbuf }
and string fmt = parse
| "\n" { newline lexbuf fmt; string fmt lexbuf }
| '"' { fprintf fmt "\"" }
| "<" { fprintf fmt "&lt;"; string fmt lexbuf }
| "&" { fprintf fmt "&amp;"; string fmt lexbuf }
......@@ -101,16 +125,14 @@ and string fmt = parse
(* input *)
let cin = open_in fname in
let lb = Lexing.from_channel cin in
lb.Lexing.lex_curr_p <-
{ lb.Lexing.lex_curr_p with Lexing.pos_fname = fname };
(* output *)
fprintf fmt "<pre>@\n";
scan fmt lb;
fprintf fmt "</pre>@\n";
close_in cin
(*
let () =
Queue.iter do_file opt_queue
*)
}
(*
......
......@@ -23,6 +23,8 @@ open Why3
open Util
open Theory
let () = Debug.set_flag Glob.flag
(* command line parsing *)
let usage_msg = sprintf
......@@ -48,7 +50,9 @@ let () =
Arg.parse option_list add_opt_file usage_msg;
let config = Whyconf.read_config None in
let main = Whyconf.get_main config in
opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main)
opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
Doc_def.set_loadpath !opt_loadpath;
Doc_def.set_output_dir !opt_output
let css =
let css_fname = match !opt_output with
......@@ -60,24 +64,21 @@ let css =
let do_file env fname =
let m = Env.read_file env fname in
let add _s _th = () (* Glob.def th.th_name *) in
let add _s th = Doc_def.add_ident th.th_name in
Mstr.iter add m
let print_file fname =
let f = Filename.basename fname in
let base = match !opt_output with
| None -> f
| Some dir -> Filename.concat dir f
in
let fhtml = base ^ ".html" in
let fhtml = Doc_def.output_file fname in
let c = open_out fhtml in
let fmt = formatter_of_out_channel c in
let f = Filename.basename fname in
Doc_html.print_header fmt ~title:f ~css ();
To_html.do_file fmt fname;
Doc_lexer.do_file fmt fname;
Doc_html.print_footer fmt ();
close_out c
let () =
Queue.iter Doc_def.add_file opt_queue;
try
let env = Env.create_env !opt_loadpath in
Queue.iter (do_file env) opt_queue;
......
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