2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 type uri_generator = string -> string
16 (* interface functions ******************************************************)
18 let indexes = ref false (* show de Bruijn indexes *)
20 let expand = ref false (* always expand global definitions *)
22 let si = ref false (* use sort inclusion *)
24 let unquote = ref false (* do not quote identifiers when lexing *)
26 let icm = ref 0 (* complexity measure of relocated terms *)
28 let cover = ref "" (* initial uri segment *)
30 let mk_uri = ref (fun _ _ -> C.err : bool -> string -> uri_generator)
36 expand := false; si := false; cover := ""; indexes := false; icm := 0;
37 mk_uri := fun _ _ -> C.err