1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * The HELM Project / The EU MoWGLI Project *)
6
(* * University of Bologna *)
7
(************************************************************************)
8
(* This file is distributed under the terms of the *)
9
(* GNU Lesser General Public License Version 2.1 *)
11
(* Copyright (C) 2000-2004, HELM Team. *)
12
(* http://helm.cs.unibo.it *)
13
(************************************************************************)
15
(* CONFIGURATION PARAMETERS *)
17
let verbose = ref false;;
20
let print_proof_tree, set_print_proof_tree =
21
let print_proof_tree = ref (fun _ _ _ _ _ _ -> None) in
22
(fun () -> !print_proof_tree),
26
curi sigma0 pf proof_tree_to_constr proof_tree_to_flattened_proof_tree
30
(f curi sigma0 pf proof_tree_to_constr
31
proof_tree_to_flattened_proof_tree constr_to_ids))
34
(* UTILITY FUNCTIONS *)
36
let print_if_verbose s = if !verbose then print_string s;;
38
(* Next exception is used only inside print_coq_object and tag_of_string_tag *)
39
exception Uninteresting;;
41
(* NOT USED anymore, we back to the V6 point of view with global parameters
43
(* Internally, for Coq V7, params of inductive types are associated *)
44
(* not to the whole block of mutual inductive (as it was in V6) but to *)
45
(* each member of the block; but externally, all params are required *)
46
(* to be the same; the following function checks that the parameters *)
47
(* of each inductive of a same block are all the same, then returns *)
48
(* this number; it fails otherwise *)
49
let extract_nparams pack =
50
let module D = Declarations in
51
let module U = Util in
52
let module S = Sign in
54
let {D.mind_nparams=nparams0} = pack.(0) in
55
let arity0 = pack.(0).D.mind_user_arity in
56
let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in
57
for i = 1 to Array.length pack - 1 do
58
let {D.mind_nparams=nparamsi} = pack.(i) in
59
let arityi = pack.(i).D.mind_user_arity in
60
let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in
61
if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block"
67
(* could_have_namesakes sp = true iff o is an object that could be cooked and *)
68
(* than that could exists in cooked form with the same name in a super *)
69
(* section of the actual section *)
70
let could_have_namesakes o sp = (* namesake = omonimo in italian *)
71
let module DK = Decl_kinds in
72
let module D = Declare in
73
let tag = Libobject.object_tag o in
74
print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
76
"CONSTANT" -> true (* constants/parameters are non global *)
77
| "INDUCTIVE" -> true (* mutual inductive types are never local *)
78
| "VARIABLE" -> false (* variables are local, so no namesakes *)
79
| _ -> false (* uninteresting thing that won't be printed*)
82
(* filter_params pvars hyps *)
83
(* filters out from pvars (which is a list of lists) all the variables *)
84
(* that does not belong to hyps (which is a simple list) *)
85
(* It returns a list of couples relative section path -- list of *)
87
let filter_params pvars hyps =
95
String.concat "/" (List.rev (List.map Names.string_of_id ids')) in
97
ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in
98
let tl' = aux ids' tl in
103
let cwd = Lib.cwd () in
104
let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
105
let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
106
aux (Names.repr_dirpath modulepath) (List.rev pvars)
109
type variables_type =
110
Definition of string * Term.constr * Term.types
111
| Assumption of string * Term.constr
114
(* The computation is very inefficient, but we can't do anything *)
115
(* better unless this function is reimplemented in the Declare *)
117
let search_variables () =
118
let module N = Names in
119
let cwd = Lib.cwd () in
120
let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
121
let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
125
| he::tl as modules ->
126
let one_section_variables =
127
let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in
128
let t = List.map N.string_of_id (Decls.last_section_hyps dirpath) in
131
one_section_variables @ aux tl
134
(Cic2acic.remove_module_dirpath_from_dirpath
135
~basedir:modulepath cwd)
138
(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *)
140
let rec join_dirs cwd =
146
with _ -> () (* Let's ignore the errors on mkdir *)
148
let newcwd = cwd ^ "/" ^ he in
149
join_dirs newcwd tail
152
let filename_of_path xml_library_root tag =
153
let module N = Names in
154
match xml_library_root with
155
None -> None (* stdout *)
156
| Some xml_library_root' ->
157
let tokens = Cic2acic.token_list_of_kernel_name tag in
158
Some (join_dirs xml_library_root' tokens)
161
let body_filename_of_filename =
163
Some f -> Some (f ^ ".body")
167
let types_filename_of_filename =
169
Some f -> Some (f ^ ".types")
173
let prooftree_filename_of_filename =
175
Some f -> Some (f ^ ".proof_tree")
179
let theory_filename xml_library_root =
180
let module N = Names in
181
match xml_library_root with
182
None -> None (* stdout *)
183
| Some xml_library_root' ->
184
let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in
185
(* theory from A/B/C/F.v goes into A/B/C/F.theory *)
186
let alltoks = List.rev toks in
187
Some (join_dirs xml_library_root' alltoks ^ ".theory")
189
let print_object uri obj sigma proof_tree_infos filename =
190
(* function to pretty print and compress an XML file *)
191
(*CSC: Unix.system "gzip ..." is an horrible non-portable solution. *)
192
let pp xml filename =
193
Xml.pp xml filename ;
200
let p = String.index_from s n '\'' in
201
String.sub s n (p - n) ^ "\\'" ^ escape s (p+1)
202
with Not_found -> String.sub s n (String.length s - n)
206
ignore (Unix.system ("gzip " ^ fn' ^ ".xml"))
208
let (annobj,_,constr_to_ids,_,ids_to_inner_sorts,ids_to_inner_types,_,_) =
209
Cic2acic.acic_object_of_cic_object sigma obj in
210
let (xml, xml') = Acic2Xml.print_object uri ids_to_inner_sorts annobj in
212
Acic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in
217
| Some xml' -> pp xml' (body_filename_of_filename filename)
219
pp xmltypes (types_filename_of_filename filename) ;
220
match proof_tree_infos with
222
| Some (sigma0,proof_tree,proof_tree_to_constr,
223
proof_tree_to_flattened_proof_tree) ->
226
uri sigma0 proof_tree proof_tree_to_constr
227
proof_tree_to_flattened_proof_tree constr_to_ids
229
match xmlprooftree with
231
| Some xmlprooftree ->
232
pp xmlprooftree (prooftree_filename_of_filename filename)
235
let string_list_of_named_context_list =
237
(function (n,_,_) -> Names.string_of_id n)
240
(* Function to collect the variables that occur in a term. *)
241
(* Used only for variables (since for constants and mutual *)
242
(* inductive types this information is already available. *)
244
let module T = Term in
246
match T.kind_of_term t with
247
T.Var id when not (List.mem id l) ->
248
let (_,bo,ty) = Global.lookup_named id in
251
Some bo' -> aux l bo'
260
| T.Cast (te,_, ty) -> aux (aux l te) ty
261
| T.Prod (_,s,t) -> aux (aux l s) t
262
| T.Lambda (_,s,t) -> aux (aux l s) t
263
| T.LetIn (_,s,_,t) -> aux (aux l s) t
264
| T.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl
266
let hyps = (Global.lookup_constant con).Declarations.const_hyps in
267
map_and_filter l hyps @ l
269
| T.Construct (ind,_) ->
270
let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in
271
map_and_filter l hyps @ l
272
| T.Case (_,t1,t2,b) ->
273
Array.fold_left (fun i x -> aux i x) (aux (aux l t1) t2) b
274
| T.Fix (_,(_,tys,bodies))
275
| T.CoFix (_,(_,tys,bodies)) ->
276
let r = Array.fold_left (fun i x -> aux i x) l tys in
277
Array.fold_left (fun i x -> aux i x) r bodies
278
and map_and_filter l =
281
| (n,_,_)::tl when not (List.mem n l) -> n::(map_and_filter l tl)
282
| _::tl -> map_and_filter l tl
287
(* Functions to construct an object *)
289
let mk_variable_obj id body typ =
290
let hyps,unsharedbody =
293
| Some bo -> find_hyps bo, Some (Unshare.unshare bo)
295
let hyps' = find_hyps typ @ hyps in
296
let hyps'' = List.map Names.string_of_id hyps' in
297
let variables = search_variables () in
298
let params = filter_params variables hyps'' in
300
(Names.string_of_id id, unsharedbody, Unshare.unshare typ, params)
303
(* Unsharing is not performed on the body, that must be already unshared. *)
304
(* The evar map and the type, instead, are unshared by this function. *)
305
let mk_current_proof_obj is_a_variable id bo ty evar_map env =
306
let unshared_ty = Unshare.unshare ty in
310
(n, {Evd.evar_concl = evar_concl ;
311
Evd.evar_hyps = evar_hyps}
313
(* We map the named context to a rel context and every Var to a Rel *)
314
let final_var_ids,context =
315
let rec aux var_ids =
319
let final_var_ids,tl' = aux (n::var_ids) tl in
320
let t' = Term.subst_vars var_ids t in
321
final_var_ids,(n, Acic.Decl (Unshare.unshare t'))::tl'
322
| (n,Some b,t)::tl ->
323
let final_var_ids,tl' = aux (n::var_ids) tl in
324
let b' = Term.subst_vars var_ids b in
325
(* t will not be exported to XML. Thus no unsharing performed *)
326
final_var_ids,(n, Acic.Def (Unshare.unshare b',t))::tl'
328
aux [] (List.rev (Environ.named_context_of_val evar_hyps))
330
(* We map the named context to a rel context and every Var to a Rel *)
331
(n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl))
332
) (Evarutil.non_instantiated evar_map)
334
let id' = Names.string_of_id id in
335
if metasenv = [] then
338
(Environ.global_vars_set env bo) (Environ.global_vars_set env ty) in
339
let hyps0 = Environ.keep_hyps env ids in
340
let hyps = string_list_of_named_context_list hyps0 in
341
(* Variables are the identifiers of the variables in scope *)
342
let variables = search_variables () in
343
let params = filter_params variables hyps in
344
if is_a_variable then
345
Acic.Variable (id',Some bo,unshared_ty,params)
347
Acic.Constant (id',Some bo,unshared_ty,params)
349
Acic.CurrentProof (id',metasenv,bo,unshared_ty)
352
let mk_constant_obj id bo ty variables hyps =
353
let hyps = string_list_of_named_context_list hyps in
354
let ty = Unshare.unshare ty in
355
let params = filter_params variables hyps in
358
Acic.Constant (Names.string_of_id id,None,ty,params)
361
(Names.string_of_id id, Some (Unshare.unshare (Declarations.force c)),
365
let mk_inductive_obj sp mib packs variables nparams hyps finite =
366
let module D = Declarations in
367
let hyps = string_list_of_named_context_list hyps in
368
let params = filter_params variables hyps in
369
(* let nparams = extract_nparams packs in *)
371
let tyno = ref (Array.length packs) in
375
let {D.mind_consnames=consnames ;
376
D.mind_typename=typename } = p
378
let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in
379
let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in
381
(Array.fold_right (fun (name,lc) i -> (name,lc)::i)
383
(fun j x ->(x,Unshare.unshare lc.(j))) consnames)
387
(typename,finite,Unshare.unshare arity,cons)::i
390
Acic.InductiveDefinition (tys,params,nparams)
393
(* The current channel for .theory files *)
394
let theory_buffer = Buffer.create 4000;;
396
let theory_output_string ?(do_not_quote = false) s =
397
(* prepare for coqdoc post-processing *)
398
let s = if do_not_quote then s else "(** #"^s^"\n#*)\n" in
400
Buffer.add_string theory_buffer s
403
let kind_of_global_goal = function
404
| Decl_kinds.Global, Decl_kinds.DefinitionBody _ -> "DEFINITION","InteractiveDefinition"
405
| Decl_kinds.Global, (Decl_kinds.Proof k) -> "THEOREM",Decl_kinds.string_of_theorem_kind k
406
| Decl_kinds.Local, _ -> assert false
408
let kind_of_inductive isrecord kn =
410
if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite
411
then if isrecord then "Record" else "Inductive"
415
let kind_of_variable id =
416
let module DK = Decl_kinds in
417
match Decls.variable_kind id with
418
| DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption"
419
| DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis"
420
| DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
421
| DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition"
422
| DK.IsProof _ -> "VARIABLE","LocalFact"
423
| _ -> Util.anomaly "Unsupported variable kind"
426
let kind_of_constant kn =
427
let module DK = Decl_kinds in
428
match Decls.constant_kind kn with
429
| DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
430
| DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
431
| DK.IsAssumption DK.Conjectural ->
432
Pp.warning "Conjecture not supported in dtd (used Declaration instead)";
433
"AXIOM","Declaration"
434
| DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
435
| DK.IsDefinition DK.Example ->
436
Pp.warning "Example not supported in dtd (used Definition instead)";
437
"DEFINITION","Definition"
438
| DK.IsDefinition DK.Coercion ->
439
Pp.warning "Coercion not supported in dtd (used Definition instead)";
440
"DEFINITION","Definition"
441
| DK.IsDefinition DK.SubClass ->
442
Pp.warning "SubClass not supported in dtd (used Definition instead)";
443
"DEFINITION","Definition"
444
| DK.IsDefinition DK.CanonicalStructure ->
445
Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)";
446
"DEFINITION","Definition"
447
| DK.IsDefinition DK.Fixpoint ->
448
Pp.warning "Fixpoint not supported in dtd (used Definition instead)";
449
"DEFINITION","Definition"
450
| DK.IsDefinition DK.CoFixpoint ->
451
Pp.warning "CoFixpoint not supported in dtd (used Definition instead)";
452
"DEFINITION","Definition"
453
| DK.IsDefinition DK.Scheme ->
454
Pp.warning "Scheme not supported in dtd (used Definition instead)";
455
"DEFINITION","Definition"
456
| DK.IsDefinition DK.StructureComponent ->
457
Pp.warning "StructureComponent not supported in dtd (used Definition instead)";
458
"DEFINITION","Definition"
459
| DK.IsDefinition DK.IdentityCoercion ->
460
Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)";
461
"DEFINITION","Definition"
462
| DK.IsDefinition DK.Instance ->
463
Pp.warning "Instance not supported in dtd (used Definition instead)";
464
"DEFINITION","Definition"
465
| DK.IsDefinition DK.Method ->
466
Pp.warning "Method not supported in dtd (used Definition instead)";
467
"DEFINITION","Definition"
468
| DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
469
"THEOREM",DK.string_of_theorem_kind thm
471
Pp.warning "Unsupported theorem kind (used Theorem instead)";
472
"THEOREM",DK.string_of_theorem_kind DK.Theorem
475
let kind_of_global r =
476
let module Ln = Libnames in
477
let module DK = Decl_kinds in
479
| Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
481
try let _ = Recordops.lookup_projections kn in true
482
with Not_found -> false in
483
kind_of_inductive isrecord (fst kn)
484
| Ln.VarRef id -> kind_of_variable id
485
| Ln.ConstRef kn -> kind_of_constant kn
488
let print_object_kind uri (xmltag,variation) =
490
Printf.sprintf "<ht:%s uri=\"%s\" as=\"%s\"/>\n" xmltag uri variation
492
theory_output_string s
496
(* where sp is the qualified identifier (section path) of a *)
497
(* definition/theorem, variable or inductive definition *)
498
(* and dest is either None (for stdout) or (Some filename) *)
499
(* pretty prints via Xml.pp the object whose identifier is id on dest *)
500
(* Note: it is printed only (and directly) the most cooked available *)
501
(* form of the definition (all the parameters are *)
502
(* lambda-abstracted, but the object can still refer to variables) *)
503
let print internal glob_ref kind xml_library_root =
504
let module D = Declarations in
505
let module De = Declare in
506
let module G = Global in
507
let module N = Names in
508
let module Nt = Nametab in
509
let module T = Term in
510
let module X = Xml in
511
let module Ln = Libnames in
512
(* Variables are the identifiers of the variables in scope *)
513
let variables = search_variables () in
517
(* this kn is fake since it is not provided by Coq *)
519
let (mod_path,dir_path) = Lib.current_prefix () in
520
N.make_kn mod_path dir_path (N.label_of_id id)
522
let (_,body,typ) = G.lookup_named id in
523
Cic2acic.Variable kn,mk_variable_obj id body typ
525
let id = N.id_of_label (N.con_label kn) in
526
let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
527
G.lookup_constant kn in
528
let typ = Typeops.type_of_constant_type (Global.env()) typ in
529
Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
530
| Ln.IndRef (kn,_) ->
531
let mib = G.lookup_mind kn in
532
let {D.mind_nparams=nparams;
533
D.mind_packets=packs ;
535
D.mind_finite=finite} = mib in
536
Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite
537
| Ln.ConstructRef _ ->
538
Util.error ("a single constructor cannot be printed in XML")
540
let fn = filename_of_path xml_library_root tag in
541
let uri = Cic2acic.uri_of_kernel_name tag in
542
if not internal then print_object_kind uri kind;
543
print_object uri obj Evd.empty None fn
546
let print_ref qid fn =
547
let ref = Nametab.global qid in
548
print false ref (kind_of_global ref) fn
551
(* where dest is either None (for stdout) or (Some filename) *)
552
(* pretty prints via Xml.pp the proof in progress on dest *)
553
let show_pftreestate internal fn (kind,pftst) id =
554
let pf = Tacmach.proof_of_pftreestate pftst in
555
let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in
556
let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree,
559
Proof2aproof.extract_open_pftreestate pftst in
560
let env = Global.env () in
562
mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in
565
Decl_kinds.Local, _ ->
567
"cic:/" ^ String.concat "/"
568
(Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable)
570
let kind_of_var = "VARIABLE","LocalFact" in
571
if not internal then print_object_kind uri kind_of_var;
573
| Decl_kinds.Global, _ ->
574
let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in
575
if not internal then print_object_kind uri (kind_of_global_goal kind);
578
print_object uri obj evar_map
579
(Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr,
580
proof_tree_to_flattened_proof_tree)) fn
584
let pftst = Pfedit.get_pftreestate () in
585
let (id,kind,_,_) = Pfedit.current_proof_statement () in
586
show_pftreestate false fn (kind,pftst) id
590
(* Let's register the callbacks *)
591
let xml_library_root =
593
Some (Sys.getenv "COQ_XML_LIBRARY_ROOT")
594
with Not_found -> None
597
let proof_to_export = ref None (* holds the proof-tree to export *)
601
Pfedit.set_xml_cook_proof
602
(function pftreestate -> proof_to_export := Some pftreestate)
606
Declare.set_xml_declare_variable
608
let id = Libnames.basename sp in
609
print false (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
610
proof_to_export := None)
614
Declare.set_xml_declare_constant
615
(function (internal,kn) ->
616
match !proof_to_export with
618
print internal (Libnames.ConstRef kn) (kind_of_constant kn)
620
| Some pftreestate ->
621
(* It is a proof. Let's export it starting from the proof-tree *)
622
(* I saved in the Pfedit.set_xml_cook_proof callback. *)
623
let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in
624
show_pftreestate internal fn pftreestate
625
(Names.id_of_label (Names.con_label kn)) ;
626
proof_to_export := None)
630
Declare.set_xml_declare_inductive
631
(function (isrecord,(sp,kn)) ->
632
print false (Libnames.IndRef (kn,0)) (kind_of_inductive isrecord kn)
637
Vernac.set_xml_start_library
639
Buffer.reset theory_buffer;
640
theory_output_string "<?xml version=\"1.0\" encoding=\"latin1\"?>\n";
641
theory_output_string ("<!DOCTYPE html [\n" ^
642
"<!ENTITY % xhtml-lat1.ent SYSTEM \"http://helm.cs.unibo.it/dtd/xhtml-lat1.ent\">\n" ^
643
"<!ENTITY % xhtml-special.ent SYSTEM \"http://helm.cs.unibo.it/dtd/xhtml-special.ent\">\n" ^
644
"<!ENTITY % xhtml-symbol.ent SYSTEM \"http://helm.cs.unibo.it/dtd/xhtml-symbol.ent\">\n\n" ^
645
"%xhtml-lat1.ent;\n" ^
646
"%xhtml-special.ent;\n" ^
647
"%xhtml-symbol.ent;\n" ^
649
theory_output_string "<html xmlns=\"http://www.w3.org/1999/xhtml\" xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\" xmlns:helm=\"http://www.cs.unibo.it/helm\">\n";
650
theory_output_string "<head></head>\n<body>\n")
654
Vernac.set_xml_end_library
656
theory_output_string "</body>\n</html>\n";
657
let ofn = theory_filename xml_library_root in
661
Buffer.output_buffer stdout theory_buffer ;
663
let ch = open_out (fn ^ ".v") in
664
Buffer.output_buffer ch theory_buffer ;
669
let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in
670
let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
671
let dir = Option.get xml_library_root in
673
if Sys.command cmd <> 0 then
674
Util.anomaly ("Error executing \"" ^ cmd ^ "\"")
676
command (coqdoc^options^" -d "^dir^" "^fn^".v");
677
let dot = if fn.[0]='/' then "." else "" in
678
command ("mv "^dir^"/"^dot^"*.html "^fn^".xml ");
679
command ("rm "^fn^".v");
680
print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n"))
684
let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;;
686
let uri_of_dirpath dir =
687
"/" ^ String.concat "/"
688
(List.map Names.string_of_id (List.rev (Names.repr_dirpath dir)))
692
Lib.set_xml_open_section
694
let s = "cic:" ^ uri_of_dirpath (Lib.cwd ()) in
695
theory_output_string ("<ht:SECTION uri=\""^s^"\">"))
699
Lib.set_xml_close_section
700
(fun _ -> theory_output_string "</ht:SECTION>")
704
Library.set_xml_require
705
(fun d -> theory_output_string
706
(Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
707
(uri_of_dirpath d) (Names.string_of_dirpath d)))
added
removed
contrib/xml/xmlcommand.ml
