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 type kernel = Crg | Brg | Bag
18 (* interface functions ******************************************************)
24 let si = ref false (* use sort inclusion *)
26 let cover = ref "" (* initial uri segment *)
28 let cc = ref false (* activate conversion constraints *)
30 let expand = ref false (* always expand global definitions *)
32 let indexes = ref false (* show de Bruijn indexes *)
34 let icm = ref 0 (* complexity measure of relocated terms *)
36 let unquote = ref false (* do not quote identifiers when lexing *)
38 let debug_parser = ref false (* output parser debug information *)
40 let debug_lexer = ref false (* output lexer debug information *)
43 let id = match !kernel with
48 let si = if !si then "-si" else "" in
52 String.concat "/" ["ld:"; kernel_id (); !cover ]
55 let bu = get_baseuri () in
56 fun s -> bu ^ "/" ^ s ^ ".ld"
59 xdir := ""; kernel := Brg; si := false; cover := "";
60 expand := false; indexes := false; icm := 0; unquote := false;
61 debug_parser := false; debug_lexer := false