Commit 6165ac52 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove line numbers from theory anchors (fixes #98).

Since the same name cannot be reused for several theories in a single
file, the line-number suffix can be scrapped. This makes it easier to
reference a given theory from a human-written documentation.

The final underscore is kept to avoid ambiguities.
parent 90d80242
......@@ -29,11 +29,11 @@ let add loc idk =
let k = key loc in
if not (Hashtbl.mem glob k) then Hashtbl.add glob k idk
let def id =
Opt.iter (fun loc -> add loc (id, Def)) id.id_loc
let def ~kind id =
Opt.iter (fun loc -> add loc (id, Def, kind)) id.id_loc
let use loc id =
add loc (id, Use)
let use ~kind loc id =
add loc (id, Use, kind)
let find loc =
Hashtbl.find glob (key loc)
......
......@@ -15,14 +15,14 @@ val flag: Debug.flag
val dummy_id: ident
val def: ident -> unit
val def: kind:string -> ident -> unit
(** [def id] registers that [id] is defined at position [id.id_loc] *)
val use: Loc.position -> ident -> unit
val use: kind:string -> Loc.position -> ident -> unit
(** [use loc id] registers that [id] is used at position [loc] *)
type def_use = Def | Use
val find: Loc.position -> ident * def_use
(** [find pos] returns the ident used/defined at position [pos], if any,
or raises [Not_found] *)
val find: Loc.position -> ident * def_use * string
(** [find pos] returns the ident at position [pos], if any, as well as its
used/defined status and its kind, or raises [Not_found] *)
......@@ -55,7 +55,7 @@ let find_qualid get_id find ns q =
let sl = string_list_of_qualid q in
let r = try find ns sl with Not_found ->
Loc.error ~loc:(qloc q) (UnboundSymbol q) in
if Debug.test_flag Glob.flag then Glob.use (qloc_last q) (get_id r);
if Debug.test_flag Glob.flag then Glob.use ~kind:"" (qloc_last q) (get_id r);
r
let find_prop_ns ns q = find_qualid (fun pr -> pr.pr_name) ns_find_pr ns q
......@@ -927,7 +927,7 @@ open Pdecl
open Pmodule
let add_pdecl ~vc muc d =
if Debug.test_flag Glob.flag then Sid.iter Glob.def d.pd_news;
if Debug.test_flag Glob.flag then Sid.iter (Glob.def ~kind:"") d.pd_news;
add_pdecl ~vc muc d
let add_decl muc d = add_pdecl ~vc:false muc (create_pure_decl d)
......@@ -1189,7 +1189,8 @@ let find_module env file q =
| Qident {id_str = nm} ->
(try Mstr.find nm file with Not_found -> read_module env [] nm)
| Qdot (p, {id_str = nm}) -> read_module env (string_list_of_qualid p) nm in
if Debug.test_flag Glob.flag then Glob.use (qloc_last q) m.mod_theory.th_name;
if Debug.test_flag Glob.flag then
Glob.use ~kind:"theory" (qloc_last q) m.mod_theory.th_name;
m
let type_inst ({muc_theory = tuc} as muc) ({mod_theory = t} as m) s =
......@@ -1345,7 +1346,8 @@ let close_module loc =
let slice = Stack.top state in
if Debug.test_noflag debug_parse_only then begin
let m = Loc.try1 ~loc close_module (Opt.get slice.muc) in
if Debug.test_flag Glob.flag then Glob.def m.mod_theory.th_name;
if Debug.test_flag Glob.flag then
Glob.def ~kind:"theory" m.mod_theory.th_name;
slice.file <- Mstr.add m.mod_theory.th_name.id_string m slice.file;
end;
slice.muc <- None
......
......@@ -52,8 +52,12 @@ let pp_tag_escape =
let c = Char.code c in
Format.fprintf fmt "%%%c%c" hex.[c / 16] hex.[c mod 16]) s
let pp_tag fmt s l =
Format.fprintf fmt "%a_%d" pp_tag_escape s l
let pp_tag ~kind fmt s l =
if kind = "theory" then
(* no need to disambiguate by line number for theories *)
Format.fprintf fmt "%a_" pp_tag_escape s
else
Format.fprintf fmt "%a_%d" pp_tag_escape s l
let local_files = Hashtbl.create 17
let add_local_file fn = Hashtbl.add local_files (Filename.chop_extension fn) ()
......@@ -68,17 +72,17 @@ let pp_url fmt lp =
| _ ->
Format.fprintf fmt "%s.html" fn
let pp_anchor fmt id =
let pp_anchor ~kind 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
let _, l, _, _ = Loc.get loc in (pp_tag ~kind) fmt id.id_string l
let pp_locate fmt id =
let pp_locate ~kind fmt id =
match id.id_loc with
| None -> raise Not_found
| Some _loc ->
let lp, _, _ =
try Pmodule.restore_path id with Not_found -> Theory.restore_path id
in
Format.fprintf fmt "%a#%a" pp_url lp pp_anchor id
Format.fprintf fmt "%a#%a" pp_url lp (pp_anchor ~kind) id
......@@ -21,8 +21,8 @@ val set_stdlib_url: string -> unit
val output_file: string -> string
val pp_anchor: Format.formatter -> ident -> unit
val pp_anchor: kind:string -> Format.formatter -> ident -> unit
(* raises [Not_found] if ident has no location *)
val pp_locate: Format.formatter -> ident -> unit
val pp_locate: kind:string -> Format.formatter -> ident -> unit
(* raises [Not_found] if ident has no location *)
......@@ -59,17 +59,17 @@
Loc.user_position f l (s + 1) (e - 1)
else loc in
try
let id, def = Glob.find loc in
let id, def, kind = 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
(Doc_def.pp_anchor ~kind) id Pp.html_string s
| Glob.Use ->
fprintf fmt "<a href=\"%a\">%a</a>"
Doc_def.pp_locate id Pp.html_string s
(Doc_def.pp_locate ~kind) id Pp.html_string s
with Not_found ->
(* otherwise, just print it *)
Pp.html_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