aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml')
-rw-r--r--plugins/xml/xmlcommand.ml23
1 files changed, 9 insertions, 14 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index ddc4725c3..6145548b2 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -441,12 +441,7 @@ let proof_to_export = ref None (* holds the proof-tree to export *)
;;
let _ =
- Pfedit.set_xml_cook_proof
- (function pftreestate -> proof_to_export := Some pftreestate)
-;;
-
-let _ =
- Declare.set_xml_declare_variable
+ Hook.set Declare.xml_declare_variable
(function (sp,kn) ->
let id = Libnames.basename sp in
print Declare.UserVerbose (Globnames.VarRef id) (kind_of_variable id) xml_library_root ;
@@ -454,7 +449,7 @@ let _ =
;;
let _ =
- Declare.set_xml_declare_constant
+ Hook.set Declare.xml_declare_constant
(function (internal,kn) ->
match !proof_to_export with
None ->
@@ -470,7 +465,7 @@ let _ =
;;
let _ =
- Declare.set_xml_declare_inductive
+ Hook.set Declare.xml_declare_inductive
(function (isrecord,(sp,kn)) ->
print Declare.UserVerbose (Globnames.IndRef (Names.mind_of_kn kn,0))
(kind_of_inductive isrecord (Names.mind_of_kn kn))
@@ -478,7 +473,7 @@ let _ =
;;
let _ =
- Vernac.set_xml_start_library
+ Hook.set Vernac.xml_start_library
(function () ->
Buffer.reset theory_buffer;
theory_output_string "<?xml version=\"1.0\" encoding=\"latin1\"?>\n";
@@ -495,7 +490,7 @@ let _ =
;;
let _ =
- Vernac.set_xml_end_library
+ Hook.set Vernac.xml_end_library
(function () ->
theory_output_string "</body>\n</html>\n";
let ofn = theory_filename xml_library_root in
@@ -525,7 +520,7 @@ let _ =
ofn)
;;
-let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;;
+let _ = Hook.set Lexer.xml_output_comment (theory_output_string ~do_not_quote:true) ;;
let uri_of_dirpath dir =
"/" ^ String.concat "/"
@@ -533,19 +528,19 @@ let uri_of_dirpath dir =
;;
let _ =
- Lib.set_xml_open_section
+ Hook.set Lib.xml_open_section
(fun _ ->
let s = "cic:" ^ uri_of_dirpath (Lib.cwd ()) in
theory_output_string ("<ht:SECTION uri=\""^s^"\">"))
;;
let _ =
- Lib.set_xml_close_section
+ Hook.set Lib.xml_close_section
(fun _ -> theory_output_string "</ht:SECTION>")
;;
let _ =
- Library.set_xml_require
+ Hook.set Library.xml_require
(fun d -> theory_output_string
(Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
(uri_of_dirpath d) (Names.DirPath.to_string d)))