Commit 4befe168 authored by MARCHE Claude's avatar MARCHE Claude Committed by MARCHE Claude

fix bug of why3doc

parent 29add8d3
......@@ -63,11 +63,17 @@ let pp_url fmt lp =
| _ ->
Format.fprintf fmt "%s.html" fn
let pp_anchor fmt id = match id.id_loc with
let pp_anchor fmt id =
match id.id_loc with
| None -> raise Not_found
| Some loc -> let _, l, _, _ = Loc.get loc in pp_tag fmt id.id_string l
| Some loc ->
let _, l, _, _ = Loc.get loc in pp_tag fmt id.id_string l
let pp_locate fmt id =
let lp, _, _ =
try Mlw_module.restore_path id with Not_found -> Theory.restore_path id in
Format.fprintf fmt "%a#%a" pp_url lp pp_anchor id
match id.id_loc with
| None -> raise Not_found
| Some _loc ->
let lp, _, _ =
try Mlw_module.restore_path id with Not_found -> Theory.restore_path id
in
Format.fprintf fmt "%a#%a" pp_url lp pp_anchor id
......@@ -22,6 +22,7 @@ val set_stdlib_url: string -> unit
val output_file: string -> string
val pp_anchor: Format.formatter -> ident -> unit
(* raises [Not_found] if ident has no location *)
val pp_locate: Format.formatter -> ident -> unit
(* or raises [Not_found] *)
(* raises [Not_found] if ident has no location *)
......@@ -63,13 +63,17 @@
(* Format.eprintf " IDENT %s/%d/%d@." f l c; *)
(* is this a def point? *)
try
match Glob.find loc with
| id, Glob.Def ->
fprintf fmt "<a name=\"%a\">%a</a>"
Doc_def.pp_anchor id Pp.html_string s
| id, Glob.Use ->
fprintf fmt "<a href=\"%a\">%a</a>"
Doc_def.pp_locate id Pp.html_string s
let id, def = Glob.find loc in
match id.Ident.id_loc with
| None -> raise Not_found
| Some _ ->
match def with
| Glob.Def ->
fprintf fmt "<a name=\"%a\">%a</a>"
Doc_def.pp_anchor id Pp.html_string s
| Glob.Use ->
fprintf fmt "<a href=\"%a\">%a</a>"
Doc_def.pp_locate id Pp.html_string s
with Not_found ->
(* otherwise, just print it *)
pp_print_string fmt s
......
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