aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
-rw-r--r--lib/system.ml50
-rw-r--r--lib/system.mli4
-rw-r--r--library/declare.ml11
-rw-r--r--library/declare.mli5
-rw-r--r--library/lib.ml6
-rw-r--r--library/lib.mli4
-rw-r--r--library/library.ml4
-rw-r--r--library/library.mli3
-rw-r--r--man/coqide.16
-rw-r--r--man/coqtop.16
-rw-r--r--parsing/g_xml.ml4287
-rw-r--r--parsing/lexer.ml46
-rw-r--r--parsing/lexer.mli2
-rw-r--r--test-suite/Makefile20
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--toplevel/usage.ml3
-rw-r--r--toplevel/vernac.ml6
-rw-r--r--toplevel/vernac.mli4
20 files changed, 2 insertions, 431 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 790acfef5..5d8cdc30f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -76,8 +76,6 @@ let profile = false
let print_emacs = ref false
-let xml_export = ref false
-
let ide_slave = ref false
let ideslave_coqtop_flags = ref None
diff --git a/lib/flags.mli b/lib/flags.mli
index 11909c5fa..5dba938b5 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -37,8 +37,6 @@ val profile : bool
val print_emacs : bool ref
-val xml_export : bool ref
-
val ide_slave : bool ref
val ideslave_coqtop_flags : string option ref
diff --git a/lib/system.ml b/lib/system.ml
index 59260fbf6..511b84ab4 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -209,56 +209,6 @@ let with_magic_number_check f a =
(str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++
strbrk "It is corrupted or was compiled with another version of Coq.")
-(* Communication through files with another executable *)
-
-let connect writefun readfun com =
- (* step 0 : prepare temporary files and I/O channels *)
- let name = Filename.basename com in
- let req,req_wr =
- try Filename.open_temp_file ("coq-"^name^"-in") ".xml"
- with Sys_error s -> error ("Cannot set connection to "^com^"("^s^")") in
- let ans,ans_wr =
- try Filename.open_temp_file ("coq-"^name^"-out") ".xml"
- with Sys_error s ->
- close_out req_wr;
- error ("Cannot set connection from "^com^"("^s^")") in
- let ans_wr' = Unix.descr_of_out_channel ans_wr in
- (* step 1 : fill the request file *)
- writefun req_wr;
- close_out req_wr;
- (* step 2a : prepare the request-reading descriptor for the sub-process *)
- let req_rd' =
- try Unix.openfile req [Unix.O_RDONLY] 0o644
- with Unix.Unix_error (err,_,_) ->
- close_out ans_wr;
- let msg = Unix.error_message err in
- error ("Cannot set connection to "^com^"("^msg^")")
- in
- (* step 2b : launch the sub-process *)
- let pid =
- try Unix.create_process com [|com|] req_rd' ans_wr' Unix.stdout
- with Unix.Unix_error (err,_,_) ->
- Unix.close req_rd'; close_out ans_wr; Unix.unlink req; Unix.unlink ans;
- let msg = Unix.error_message err in
- error ("Cannot execute "^com^"("^msg^")") in
- Unix.close req_rd';
- close_out ans_wr;
- (* step 2c : wait for termination of the sub-process *)
- (match CUnix.waitpid_non_intr pid with
- | Unix.WEXITED 127 -> error (com^": cannot execute")
- | Unix.WEXITED 0 -> ()
- | _ -> error (com^" exited abnormally"));
- (* step 3 : read the answer and handle it *)
- let ans_rd =
- try open_in ans
- with Sys_error s -> error ("Cannot read output of "^com^"("^s^")") in
- let a = readfun ans_rd in
- close_in ans_rd;
- (* step 4 : cleanup the temporary files *)
- unlink req;
- unlink ans;
- a
-
(* Time stamps. *)
type time = float * float * float
diff --git a/lib/system.mli b/lib/system.mli
index 0569c7889..af797121a 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -56,10 +56,6 @@ val marshal_out_segment : string -> out_channel -> 'a -> unit
val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t
val skip_in_segment : string -> in_channel -> int * Digest.t
-(** {6 Sending/receiving once with external executable } *)
-
-val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
-
(** {6 Time stamps.} *)
type time
diff --git a/library/declare.ml b/library/declare.ml
index 94239d0bf..8ec52d16a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -32,14 +32,6 @@ type internal_flag =
| KernelSilent (* kernel action, no message is displayed *)
| UserVerbose (* user action, a message is displayed *)
-(** XML output hooks *)
-
-let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore ()
-let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore ()
-let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore ()
-
-let if_xml f x = if !Flags.xml_export then f x else ()
-
(** Declaration of section variables and local definitions *)
type section_variable_entry =
@@ -91,7 +83,6 @@ let declare_variable id obj =
declare_var_implicits id;
Notation.declare_ref_arguments_scope (VarRef id);
Heads.declare_head (EvalVarRef id);
- if_xml (Hook.get f_xml_declare_variable) oname;
oname
@@ -291,7 +282,6 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
cst_locl = local;
} in
let kn = declare_constant_common id cst in
- let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
kn
let declare_definition ?(internal=UserVerbose)
@@ -412,7 +402,6 @@ let declare_mind isrecord mie =
declare_projections mind;
declare_mib_implicits mind;
declare_inductive_argument_scopes mind mie;
- if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
oname
(* Declaration messages *)
diff --git a/library/declare.mli b/library/declare.mli
index a9fd8956e..bda90229e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -70,11 +70,6 @@ val set_declare_scheme :
the whole block (boolean must be true iff it is a record) *)
val declare_mind : internal_flag -> mutual_inductive_entry -> object_name
-(** Hooks for XML output *)
-val xml_declare_variable : (object_name -> unit) Hook.t
-val xml_declare_constant : (internal_flag * constant -> unit) Hook.t
-val xml_declare_inductive : (internal_flag * object_name -> unit) Hook.t
-
(** Declaration messages *)
val definition_message : Id.t -> unit
diff --git a/library/lib.ml b/library/lib.ml
index f33f244b8..d85d38368 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -475,10 +475,6 @@ let full_section_segment_of_constant con =
(*************)
(* Sections. *)
-(* XML output hooks *)
-let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore ()
-let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore ()
-
let open_section id =
let olddir,(mp,oldsec) = !path_prefix in
let dir = add_dirpath_suffix olddir id in
@@ -490,7 +486,6 @@ let open_section id =
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
path_prefix := prefix;
- if !Flags.xml_export then Hook.get f_xml_open_section id;
add_section ()
@@ -519,7 +514,6 @@ let close_section () =
let full_olddir = fst !path_prefix in
pop_path_prefix ();
add_entry oname (ClosedSection (List.rev (mark::secdecls)));
- if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname));
let newdecls = List.map discharge_item secdecls in
Summary.unfreeze_summaries fs;
List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
diff --git a/library/lib.mli b/library/lib.mli
index b5a32f762..8e4ea4c21 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -156,10 +156,6 @@ val unfreeze : frozen -> unit
val init : unit -> unit
-(** XML output hooks *)
-val xml_open_section : (Names.Id.t -> unit) Hook.t
-val xml_close_section : (Names.Id.t -> unit) Hook.t
-
(** {6 Section management for discharge } *)
type variable_info = Names.Id.t * Decl_kinds.binding_kind *
Term.constr option * Term.types
diff --git a/library/library.ml b/library/library.ml
index 9552a6ca9..7bff05cda 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -600,8 +600,6 @@ let in_require : require_obj -> obj =
(* Require libraries, import them if [export <> None], mark them for export
if [export = Some true] *)
-let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
-
let require_library_from_dirpath modrefl export =
let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
@@ -615,7 +613,6 @@ let require_library_from_dirpath modrefl export =
end
else
add_anonymous_leaf (in_require (needed,modrefl,export));
- if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
add_frozen_state ()
let require_library qidl export =
@@ -632,7 +629,6 @@ let require_library_from_file idopt file export =
end
else
add_anonymous_leaf (in_require (needed,[modref],export));
- if !Flags.xml_export then Hook.get f_xml_require modref;
add_frozen_state ()
(* the function called by Vernacentries.vernac_import *)
diff --git a/library/library.mli b/library/library.mli
index 0f6f510d8..5154c25e4 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -66,9 +66,6 @@ val library_full_filename : DirPath.t -> string
(** - Overwrite the filename of all libraries (used when restoring a state) *)
val overwrite_library_filenames : string -> unit
-(** {6 Hook for the xml exportation of libraries } *)
-val xml_require : (DirPath.t -> unit) Hook.t
-
(** {6 Locate a library in the load paths } *)
exception LibUnmappedDir
exception LibNotFound
diff --git a/man/coqide.1 b/man/coqide.1
index 785a4a4c6..3fa7f0e41 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -121,12 +121,6 @@ Set sort Set impredicative.
.TP
.B \-dont\-load\-proofs
Don't load opaque proofs in memory.
-.TP
-.B \-xml
-Export XML files either to the hierarchy rooted in
-the directory
-.B COQ_XML_LIBRARY_ROOT
-(if set) or to stdout (if unset).
.SH SEE ALSO
diff --git a/man/coqtop.1 b/man/coqtop.1
index 068a5072b..1bc4629d0 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -152,12 +152,6 @@ set sort Set impredicative
.B \-dont\-load\-proofs
don't load opaque proofs in memory
-.TP
-.B \-xml
-export XML files either to the hierarchy rooted in
-the directory $COQ_XML_LIBRARY_ROOT (if set) or to
-stdout (if unset)
-
.SH SEE ALSO
.BR coqc (1),
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
deleted file mode 100644
index f639ee7c5..000000000
--- a/parsing/g_xml.ml4
+++ /dev/null
@@ -1,287 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Compat
-open Pp
-open Errors
-open Util
-open Names
-open Pcoq
-open Glob_term
-open Tacexpr
-open Libnames
-open Globnames
-open Detyping
-open Misctypes
-open Decl_kinds
-open Genredexpr
-open Tok (* necessary for camlp4 *)
-
-(* Generic xml parser without raw data *)
-
-type attribute = string * (Loc.t * string)
-type xml = XmlTag of Loc.t * string * attribute list * xml list
-
-let check_tags loc otag ctag =
- if not (String.equal otag ctag) then
- user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
- str "does not match open xml tag " ++ str otag ++ str ".")
-
-let xml_eoi = (Gram.entry_create "xml_eoi" : xml Gram.entry)
-
-GEXTEND Gram
- GLOBAL: xml_eoi;
-
- xml_eoi:
- [ [ x = xml; EOI -> x ] ]
- ;
- xml:
- [ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml;
- "<"; "/"; ctag = IDENT; ">" ->
- check_tags (!@loc) otag ctag;
- XmlTag (!@loc,ctag,attrs,l)
- | "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" ->
- XmlTag (!@loc,tag,attrs,[])
- ] ]
- ;
- attr:
- [ [ name = IDENT; "="; data = STRING -> (name, (!@loc, data)) ] ]
- ;
-END
-
-(* Errors *)
-
-let error_bad_arity loc n =
- let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in
- user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^")."))
-
-(* Interpreting attributes *)
-
-let nmtoken (loc,a) =
- try int_of_string a
- with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
-
-let get_xml_attr s al =
- try String.List.assoc s al
- with Not_found -> error ("No attribute "^s)
-
-(* Interpreting specific attributes *)
-
-let ident_of_cdata (loc,a) = Id.of_string a
-
-let uri_of_data s =
- try
- let n = String.index s ':' in
- let p = String.index s '.' in
- let s = String.sub s (n+2) (p-n-2) in
- for i = 0 to String.length s - 1 do
- match s.[i] with
- | '/' -> s.[i] <- '.'
- | _ -> ()
- done;
- qualid_of_string s
- with Not_found | Invalid_argument _ ->
- error ("Malformed URI \""^s^"\"")
-
-let constant_of_cdata (loc,a) =
- let q = uri_of_data a in
- try Nametab.locate_constant q
- with Not_found -> error ("No such constant "^string_of_qualid q)
-
-let global_of_cdata (loc,a) =
- let q = uri_of_data a in
- try Nametab.locate q
- with Not_found -> error ("No such global "^string_of_qualid q)
-
-let inductive_of_cdata a = match global_of_cdata a with
- | IndRef (kn,_) -> kn
- | _ -> error (string_of_qualid (uri_of_data (snd a)) ^" is not an inductive")
-
-let ltacref_of_cdata (loc,a) =
- let q = uri_of_data a in
- try (loc,Nametab.locate_tactic q)
- with Not_found -> error ("No such ltac "^string_of_qualid q)
-
-let sort_of_cdata (loc,a) = match a with
- | "Prop" -> GProp
- | "Set" -> GSet
- | "Type" -> GType None
- | _ -> user_err_loc (loc,"",str "sort expected.")
-
-let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
-
-let get_xml_inductive_kn al =
- inductive_of_cdata (* uriType apparent synonym of uri *)
- (try get_xml_attr "uri" al
- with UserError _ -> get_xml_attr "uriType" al)
-
-let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
-
-let get_xml_inductive al =
- (get_xml_inductive_kn al, nmtoken (get_xml_attr "noType" al))
-
-let get_xml_constructor al =
- (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al))
-
-let get_xml_binder al =
- try Name (ident_of_cdata (String.List.assoc "binder" al))
- with Not_found -> Anonymous
-
-let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
-
-let get_xml_name al = ident_of_cdata (get_xml_attr "name" al)
-
-let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
-
-let get_xml_no al = Evar.unsafe_of_int (nmtoken (get_xml_attr "no" al))
-
-(* A leak in the xml dtd: arities of constructor need to know global env *)
-
-let compute_branches_lengths ind =
- let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
- mip.Declarations.mind_consnrealdecls
-
-let compute_inductive_ndecls ind =
- Inductiveops.inductive_nrealdecls ind
-
-(* Interpreting constr as a glob_constr *)
-
-let rec interp_xml_constr = function
- | XmlTag (loc,"REL",al,[]) ->
- GVar (loc, get_xml_ident al)
- | XmlTag (loc,"VAR",al,[]) ->
- error "XML parser: unable to interp free variables"
- | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
- let body,decls = List.sep_last xl in
- let ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b))
- ctx (interp_xml_target body)
- | XmlTag (loc,"PROD",al,(_::_ as xl)) ->
- let body,decls = List.sep_last xl in
- let ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b))
- ctx (interp_xml_target body)
- | XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
- let body,defs = List.sep_last xl in
- let ctx = List.map interp_xml_def defs in
- List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b))
- ctx (interp_xml_target body)
- | XmlTag (loc,"APPLY",_,x::xl) ->
- GApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
- | XmlTag (loc,"instantiate",_,
- (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
- GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
- | XmlTag (loc,"META",al,xl) ->
- GEvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
- | XmlTag (loc,"CONST",al,[]) ->
- GRef (loc, ConstRef (get_xml_constant al), None)
- | XmlTag (loc,"MUTCASE",al,x::y::yl) ->
- let ind = get_xml_inductive al in
- let p = interp_xml_patternsType x in
- let tm = interp_xml_inductiveTerm y in
- let vars = compute_branches_lengths ind in
- let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
- in
- let mat = simple_cases_matrix_of_branches ind brs in
- let n = compute_inductive_ndecls ind in
- let nal,rtn = return_type_of_predicate ind n p in
- GCases (loc,RegularStyle,rtn,[tm,nal],mat)
- | XmlTag (loc,"MUTIND",al,[]) ->
- GRef (loc, IndRef (get_xml_inductive al), None)
- | XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
- GRef (loc, ConstructRef (get_xml_constructor al), None)
- | XmlTag (loc,"FIX",al,xl) ->
- let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
- let ln,lc,lt = List.split3 lnct in
- let lctx = List.map (fun _ -> []) ln in
- GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
- | XmlTag (loc,"COFIX",al,xl) ->
- let ln,lc,lt = List.split3 (List.map interp_xml_CoFixFunction xl) in
- GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
- | XmlTag (loc,"CAST",al,[x1;x2]) ->
- GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2))
- | XmlTag (loc,"SORT",al,[]) ->
- GSort (loc, get_xml_sort al)
- | XmlTag (loc,s,_,_) ->
- user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
-
-and interp_xml_tag s = function
- | XmlTag (loc,tag,al,xl) when String.equal tag s -> (loc,al,xl)
- | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "",
- str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".")
-
-and interp_xml_constr_alias s x =
- match interp_xml_tag s x with
- | (_,_,[x]) -> interp_xml_constr x
- | (loc,_,_) -> error_bad_arity loc 1
-
-and interp_xml_term x = interp_xml_constr_alias "term" x
-and interp_xml_type x = interp_xml_constr_alias "type" x
-and interp_xml_target x = interp_xml_constr_alias "target" x
-and interp_xml_body x = interp_xml_constr_alias "body" x
-and interp_xml_pattern x = interp_xml_constr_alias "pattern" x
-and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x
-and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x
-and interp_xml_arg x = interp_xml_constr_alias "arg" x
-and interp_xml_substitution x = interp_xml_constr_alias "substitution" x
- (* no support for empty substitution from official dtd *)
-
-and interp_xml_decl_alias s x =
- match interp_xml_tag s x with
- | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
- | (loc,_,_) -> error_bad_arity loc 1
-
-and interp_xml_def x = interp_xml_decl_alias "def" x
-and interp_xml_decl x = interp_xml_decl_alias "decl" x
-
-and interp_xml_recursionOrder x =
- let (loc, al, l) = interp_xml_tag "RecursionOrder" x in
- let (locs, s) = get_xml_attr "type" al in
- match s, l with
- | "Structural", [] -> GStructRec
- | "Structural", _ -> error_bad_arity loc 0
- | "WellFounded", [c] -> GWfRec (interp_xml_type c)
- | "WellFounded", _ -> error_bad_arity loc 1
- | "Measure", [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r))
- | "Measure", _ -> error_bad_arity loc 2
- | _ -> user_err_loc (locs,"",str "Invalid recursion order.")
-
-and interp_xml_FixFunction x =
- match interp_xml_tag "FixFunction" x with
- | (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *)
- ((Some (nmtoken (get_xml_attr "recIndex" al)),
- interp_xml_recursionOrder x1),
- (get_xml_name al, interp_xml_type x2, interp_xml_body x3))
- | (loc,al,[x1;x2]) ->
- ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec),
- (get_xml_name al, interp_xml_type x1, interp_xml_body x2))
- | (loc,_,_) ->
- error_bad_arity loc 1
-
-and interp_xml_CoFixFunction x =
- match interp_xml_tag "CoFixFunction" x with
- | (loc,al,[x1;x2]) ->
- (get_xml_name al, interp_xml_type x1, interp_xml_body x2)
- | (loc,_,_) ->
- error_bad_arity loc 1
-
-(* Interpreting tactic argument *)
-
-let rec interp_xml_tactic_arg = function
- | XmlTag (loc,"TERM",[],[x]) ->
- ConstrMayEval (ConstrTerm (interp_xml_constr x,None))
- | XmlTag (loc,"CALL",al,xl) ->
- let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in
- TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl)
- | XmlTag (loc,s,_,_) ->
- user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
-
-let parse_tactic_arg ch =
- interp_xml_tactic_arg
- (Pcoq.Gram.entry_parse xml_eoi
- (Pcoq.Gram.parsable (Stream.of_channel ch)))
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 13f835951..a78bbdcd9 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -298,9 +298,6 @@ let rec string in_comments bp len = parser
| [< 'c; s >] -> string in_comments bp (store len c) s
| [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
-(* Hook for exporting comment into xml theory files *)
-let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
-
(* Utilities for comments in beautify *)
let comment_begin = ref None
let comm_loc bp = match !comment_begin with
@@ -343,9 +340,6 @@ let null_comment s =
let comment_stop ep =
let current_s = Buffer.contents current in
- if !Flags.xml_export && Buffer.length current > 0 &&
- (!between_com || not(null_comment current_s)) then
- Hook.get f_xml_output_comment current_s;
(if Flags.do_beautify() && Buffer.length current > 0 &&
(!between_com || not(null_comment current_s)) then
let bp = match !comment_begin with
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index dd811acfe..0ec5a80b4 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -29,8 +29,6 @@ type com_state
val com_state: unit -> com_state
val restore_com_state: com_state -> unit
-val xml_output_comment : (string -> unit) Hook.t
-
val terminal : string -> Tok.t
(** The lexer of Coq: *)
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 81a556671..0f7abb78e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -346,25 +346,7 @@ modules/%.vo: modules/%.v
# Miscellaneous tests
#######################################################################
-misc: misc/xml.log misc/deps-order.log misc/universes.log
-
-# Test xml compilation
-xml: misc/xml.log
-misc/xml.log:
- @echo "TEST misc/xml"
- $(HIDE){ \
- echo $(call log_intro,xml); \
- rm -rf misc/xml; \
- COQ_XML_LIBRARY_ROOT=misc/xml \
- $(bincoqc) -xml misc/berardi_test 2>&1; times; \
- if [ ! -d misc/xml ]; then \
- echo $(log_failure); \
- echo " misc/xml... failed"; \
- else \
- echo $(log_success); \
- echo " misc/xml...apparently ok"; \
- fi; rm -rf misc/xml; \
- } > "$@"
+misc: misc/deps-order.log misc/universes.log
# Check that both coqdep and coqtop/coqc supports -R
# Check that both coqdep and coqtop/coqc takes the later -R
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b41826995..ef52a5774 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -430,7 +430,6 @@ let parse_args arglist =
|"-verbose-compat-notations" -> verb_compat_ntn := true
|"-vm" -> use_vm := true
|"-where" -> print_where := true
- |"-xml" -> Flags.xml_export := true
(* Deprecated options *)
|"-byte" -> warning "option -byte deprecated, call with .byte suffix"
@@ -446,6 +445,7 @@ let parse_args arglist =
|"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"."
|"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ())
|"-quality" -> warning "Obsolete option \"-quality\"."
+ |"-xml" -> warning "Obsolete option \"-xml\"."
(* Unknown option *)
| s -> extras := s :: !extras
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index eac46f566..0183cfaa1 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -61,9 +61,6 @@ let print_usage_channel co command =
\n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
\n -impredicative-set set sort Set impredicative\
\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
-\n -xml export XML files either to the hierarchy rooted in\
-\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
-\n stdout (if unset)\
\n -time display the time taken by each command\
\n -h, --help print this list of options\
\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5e9d77bed..248a6b513 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -291,10 +291,6 @@ let checknav loc ast =
let eval_expr loc_ast = vernac_com true checknav loc_ast
-(* XML output hooks *)
-let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
-let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
-
(* Load a vernac file. Errors are annotated with file and location *)
let load_vernac verb file =
chan_beautify :=
@@ -320,7 +316,6 @@ let compile verbosely f =
Aux_file.start_aux_file_for long_f_dot_v;
Dumpglob.start_dump_glob long_f_dot_v;
Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
- if !Flags.xml_export then Hook.get f_xml_start_library ();
let wall_clock1 = Unix.gettimeofday () in
let _ = load_vernac verbosely long_f_dot_v in
Stm.join ();
@@ -330,7 +325,6 @@ let compile verbosely f =
Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Aux_file.stop_aux_file ();
- if !Flags.xml_export then Hook.get f_xml_end_library ();
Dumpglob.end_dump_glob ()
| BuildVi ->
let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index f3988d53e..d46622a02 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -23,10 +23,6 @@ val just_parsing : bool ref
val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit
-(** Set XML hooks *)
-val xml_start_library : (unit -> unit) Hook.t
-val xml_end_library : (unit -> unit) Hook.t
-
(** Load a vernac file, verbosely or not. Errors are annotated with file
and location *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 03:49:24 +0000