aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml36
-rw-r--r--ide/coqidetop.mllib7
-rw-r--r--ide/ide.mllib7
-rw-r--r--ide/ide_slave.ml53
-rw-r--r--ide/richprinter.ml24
-rw-r--r--ide/richprinter.mli36
-rw-r--r--ide/serialize.ml121
-rw-r--r--ide/serialize.mli39
-rw-r--r--ide/texmacspp.ml762
-rw-r--r--ide/texmacspp.mli12
-rw-r--r--ide/wg_Segment.ml9
-rw-r--r--ide/xml_lexer.mli44
-rw-r--r--ide/xml_lexer.mll317
-rw-r--r--ide/xml_parser.ml232
-rw-r--r--ide/xml_parser.mli106
-rw-r--r--ide/xml_printer.ml145
-rw-r--r--ide/xml_printer.mli29
-rw-r--r--ide/xmlprotocol.ml189
-rw-r--r--ide/xmlprotocol.mli14
19 files changed, 2124 insertions, 58 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 7a32faffc..61f002576 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -290,12 +290,9 @@ let rec check_errors = function
| `NVAL :: _ -> raise (TubeError "NVAL")
| `OUT :: _ -> raise (TubeError "OUT")
-let handle_intermediate_message handle xml =
- let message = Feedback.to_message xml in
- let level = message.Feedback.message_level in
- let content = message.Feedback.message_content in
- let logger = match handle.waiting_for with
- | Some (_, l) -> l
+let handle_intermediate_message handle level content =
+ let logger = match handle.waiting_for with
+ | Some (_, l) -> l
| None -> function
| Feedback.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s)
| Feedback.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s)
@@ -303,10 +300,10 @@ let handle_intermediate_message handle xml =
| Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
| Feedback.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s)
in
- logger level (Richpp.richpp_of_xml content)
+ logger level content
let handle_feedback feedback_processor xml =
- let feedback = Feedback.to_feedback xml in
+ let feedback = Xmlprotocol.to_feedback xml in
feedback_processor feedback
let handle_final_answer handle xml =
@@ -335,15 +332,18 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
let l_end = Lexing.lexeme_end lex in
state.fragment <- String.sub s l_end (String.length s - l_end);
state.lexerror <- None;
- if Feedback.is_message xml then begin
- handle_intermediate_message handle xml;
+ match Xmlprotocol.is_message xml with
+ | Some (lvl, msg) ->
+ handle_intermediate_message handle lvl msg;
loop ()
- end else if Feedback.is_feedback xml then begin
- handle_feedback feedback_processor xml;
- loop ()
- end else begin
- ignore (handle_final_answer handle xml)
- end
+ | None ->
+ if Xmlprotocol.is_feedback xml then begin
+ handle_feedback feedback_processor xml;
+ loop ()
+ end else
+ begin
+ ignore (handle_final_answer handle xml)
+ end
in
try loop ()
with Xml_parser.Error _ as e ->
@@ -357,7 +357,9 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
let print_exception = function
| Xml_parser.Error e -> Xml_parser.error e
- | Serialize.Marshal_error -> "Protocol violation"
+ | Serialize.Marshal_error(expected,actual) ->
+ "Protocol violation. Expected: " ^ expected ^ " Actual: "
+ ^ Xml_printer.to_string actual
| e -> Printexc.to_string e
let input_watch handle respawner feedback_processor =
diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib
index 92301dc30..ed1fa465d 100644
--- a/ide/coqidetop.mllib
+++ b/ide/coqidetop.mllib
@@ -1,2 +1,9 @@
+Xml_lexer
+Xml_parser
+Xml_printer
+Serialize
+Richprinter
Xmlprotocol
+Texmacspp
+Document
Ide_slave
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 83b314283..b2f32fcf7 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -14,8 +14,13 @@ Config_lexer
Utf8_convert
Preferences
Project_file
-Ideutils
+Serialize
+Richprinter
+Xml_lexer
+Xml_parser
+Xml_printer
Xmlprotocol
+Ideutils
Coq
Coq_lex
Sentence
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 59efc2d82..6a386e050 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -281,11 +281,33 @@ let export_coq_object t = {
Interface.coq_object_object = t.Search.coq_object_object
}
+let pattern_of_string ?env s =
+ let env =
+ match env with
+ | None -> Global.env ()
+ | Some e -> e
+ in
+ let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
+ let (_, pat) = Constrintern.intern_constr_pattern env constr in
+ pat
+
+let dirpath_of_string_list s =
+ let path = String.concat "." s in
+ let m = Pcoq.parse_string Pcoq.Constr.global path in
+ let (_, qid) = Libnames.qualid_of_reference m in
+ let id =
+ try Nametab.full_name_module qid
+ with Not_found ->
+ Errors.errorlabstrm "Search.interface_search"
+ (str "Module " ++ str path ++ str " not found.")
+ in
+ id
+
let import_search_constraint = function
- | Interface.Name_Pattern s -> Search.Name_Pattern s
- | Interface.Type_Pattern s -> Search.Type_Pattern s
- | Interface.SubType_Pattern s -> Search.SubType_Pattern s
- | Interface.In_Module ms -> Search.In_Module ms
+ | Interface.Name_Pattern s -> Search.Name_Pattern (Str.regexp s)
+ | Interface.Type_Pattern s -> Search.Type_Pattern (pattern_of_string s)
+ | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s)
+ | Interface.In_Module ms -> Search.In_Module (dirpath_of_string_list ms)
| Interface.Include_Blacklist -> Search.Include_Blacklist
let search flags =
@@ -393,6 +415,15 @@ let interp ((_raw, verbose), s) =
let quit = ref false
+(** Serializes the output of Stm.get_ast *)
+let print_ast id =
+ match Stm.get_ast id with
+ | Some (expr, loc) -> begin
+ try Texmacspp.tmpp expr loc
+ with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e)
+ end
+ | None -> Xml_datatype.PCData "ERROR"
+
(** Grouping all call handlers together + error handling *)
let eval_call xml_oc log c =
@@ -423,7 +454,7 @@ let eval_call xml_oc log c =
Interface.interp = interruptible interp;
Interface.handle_exn = handle_exn;
Interface.stop_worker = Stm.stop_worker;
- Interface.print_ast = Stm.print_ast;
+ Interface.print_ast = print_ast;
Interface.annotate = interruptible annotate;
} in
Xmlprotocol.abstract_eval_call handler c
@@ -444,16 +475,12 @@ let print_xml =
let slave_logger xml_oc level message =
(* convert the message into XML *)
let msg = hov 0 message in
- let message = {
- Feedback.message_level = level;
- Feedback.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
- } in
- let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
- let xml = Feedback.of_message message in
+ let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
+ let xml = Xmlprotocol.of_message level (Richpp.richpp_of_pp message) in
print_xml xml_oc xml
let slave_feeder xml_oc msg =
- let xml = Feedback.of_feedback msg in
+ let xml = Xmlprotocol.of_feedback msg in
print_xml xml_oc xml
(** The main loop *)
@@ -494,7 +521,7 @@ let loop () =
| Xml_parser.Error (err, loc) ->
pr_debug ("Syntax error in query: " ^ Xml_parser.error_msg err);
exit 1
- | Serialize.Marshal_error ->
+ | Serialize.Marshal_error _ ->
pr_debug "Incorrect query.";
exit 1
| any ->
diff --git a/ide/richprinter.ml b/ide/richprinter.ml
new file mode 100644
index 000000000..5f39f36ea
--- /dev/null
+++ b/ide/richprinter.ml
@@ -0,0 +1,24 @@
+open Richpp
+
+module RichppConstr = Ppconstr.Richpp
+module RichppVernac = Ppvernac.Richpp
+module RichppTactic = Pptactic.Richpp
+
+type rich_pp =
+ Ppannotation.t Richpp.located Xml_datatype.gxml
+ * Xml_datatype.xml
+
+let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
+
+let make_richpp pr ast =
+ let rich_pp =
+ rich_pp get_annotations (pr ast)
+ in
+ let xml = Ppannotation.(
+ xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
+ )
+ in
+ (rich_pp, xml)
+
+let richpp_vernac = make_richpp RichppVernac.pr_vernac
+let richpp_constr = make_richpp RichppConstr.pr_constr_expr
diff --git a/ide/richprinter.mli b/ide/richprinter.mli
new file mode 100644
index 000000000..c9e84e3eb
--- /dev/null
+++ b/ide/richprinter.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** This module provides an entry point to "rich" pretty-printers that
+ produce pretty-printing as done by {!Printer} but with additional
+ annotations represented as a semi-structured document.
+
+ To understand what are these annotations and how they are represented
+ as standard XML attributes, please refer to {!Ppannotation}.
+
+ In addition to these annotations, each node of the semi-structured
+ document contains a [startpos] and an [endpos] attribute that
+ relate this node to the raw pretty-printing.
+ Please refer to {!Richpp} for more details. *)
+
+(** A rich pretty-print is composed of: *)
+type rich_pp =
+
+ (** - a generalized semi-structured document whose attributes are
+ annotations ; *)
+ Ppannotation.t Richpp.located Xml_datatype.gxml
+
+ (** - an XML document, representing annotations as usual textual
+ XML attributes. *)
+ * Xml_datatype.xml
+
+(** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *)
+val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp
+
+(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *)
+val richpp_constr : Constrexpr.constr_expr -> rich_pp
diff --git a/ide/serialize.ml b/ide/serialize.ml
new file mode 100644
index 000000000..7b568501e
--- /dev/null
+++ b/ide/serialize.ml
@@ -0,0 +1,121 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Xml_datatype
+
+exception Marshal_error of string * xml
+
+(** Utility functions *)
+
+let rec get_attr attr = function
+ | [] -> raise Not_found
+ | (k, v) :: l when CString.equal k attr -> v
+ | _ :: l -> get_attr attr l
+
+let massoc x l =
+ try get_attr x l
+ with Not_found -> raise (Marshal_error("attribute " ^ x,PCData "not there"))
+
+let constructor t c args = Element (t, ["val", c], args)
+let do_match t mf = function
+ | Element (s, attrs, args) when CString.equal s t ->
+ let c = massoc "val" attrs in
+ mf c args
+ | x -> raise (Marshal_error (t,x))
+
+let singleton = function
+ | [x] -> x
+ | l -> raise (Marshal_error
+ ("singleton",PCData ("list of length " ^ string_of_int (List.length l))))
+
+let raw_string = function
+ | [] -> ""
+ | [PCData s] -> s
+ | x::_ -> raise (Marshal_error("raw string",x))
+
+(** Base types *)
+
+let of_unit () = Element ("unit", [], [])
+let to_unit : xml -> unit = function
+ | Element ("unit", [], []) -> ()
+ | x -> raise (Marshal_error ("unit",x))
+
+let of_bool (b : bool) : xml =
+ if b then constructor "bool" "true" []
+ else constructor "bool" "false" []
+let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with
+ | "true" -> true
+ | "false" -> false
+ | x -> raise (Marshal_error("bool",PCData x)))
+
+let of_list (f : 'a -> xml) (l : 'a list) =
+ Element ("list", [], List.map f l)
+let to_list (f : xml -> 'a) : xml -> 'a list = function
+ | Element ("list", [], l) -> List.map f l
+ | x -> raise (Marshal_error("list",x))
+
+let of_option (f : 'a -> xml) : 'a option -> xml = function
+ | None -> Element ("option", ["val", "none"], [])
+ | Some x -> Element ("option", ["val", "some"], [f x])
+let to_option (f : xml -> 'a) : xml -> 'a option = function
+ | Element ("option", ["val", "none"], []) -> None
+ | Element ("option", ["val", "some"], [x]) -> Some (f x)
+ | x -> raise (Marshal_error("option",x))
+
+let of_string (s : string) : xml = Element ("string", [], [PCData s])
+let to_string : xml -> string = function
+ | Element ("string", [], l) -> raw_string l
+ | x -> raise (Marshal_error("string",x))
+
+let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)])
+let to_int : xml -> int = function
+ | Element ("int", [], [PCData s]) ->
+ (try int_of_string s with Failure _ -> raise(Marshal_error("int",PCData s)))
+ | x -> raise (Marshal_error("int",x))
+
+let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml =
+ Element ("pair", [], [f (fst x); g (snd x)])
+let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function
+ | Element ("pair", [], [x; y]) -> (f x, g y)
+ | x -> raise (Marshal_error("pair",x))
+
+let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function
+ | CSig.Inl x -> Element ("union", ["val","in_l"], [f x])
+ | CSig.Inr x -> Element ("union", ["val","in_r"], [g x])
+let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function
+ | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x)
+ | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x)
+ | x -> raise (Marshal_error("union",x))
+
+(** More elaborate types *)
+
+let of_edit_id i = Element ("edit_id",["val",string_of_int i],[])
+let to_edit_id = function
+ | Element ("edit_id",["val",i],[]) ->
+ let id = int_of_string i in
+ assert (id <= 0 );
+ id
+ | x -> raise (Marshal_error("edit_id",x))
+
+let of_loc loc =
+ let start, stop = Loc.unloc loc in
+ Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
+let to_loc xml =
+ match xml with
+ | Element ("loc", l,[]) ->
+ let start = massoc "start" l in
+ let stop = massoc "stop" l in
+ (try
+ Loc.make_loc (int_of_string start, int_of_string stop)
+ with Not_found | Invalid_argument _ -> raise (Marshal_error("loc",PCData(start^":"^stop))))
+ | x -> raise (Marshal_error("loc",x))
+
+let of_xml x = Element ("xml", [], [x])
+let to_xml xml = match xml with
+| Element ("xml", [], [x]) -> x
+| x -> raise (Marshal_error("xml",x))
diff --git a/ide/serialize.mli b/ide/serialize.mli
new file mode 100644
index 000000000..bf9e184eb
--- /dev/null
+++ b/ide/serialize.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Xml_datatype
+
+exception Marshal_error of string * xml
+
+val massoc: string -> (string * string) list -> string
+val constructor: string -> string -> xml list -> xml
+val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b
+val singleton: 'a list -> 'a
+val raw_string: xml list -> string
+val of_unit: unit -> xml
+val to_unit: xml -> unit
+val of_bool: bool -> xml
+val to_bool: xml -> bool
+val of_list: ('a -> xml) -> 'a list -> xml
+val to_list: (xml -> 'a) -> xml -> 'a list
+val of_option: ('a -> xml) -> 'a option -> xml
+val to_option: (xml -> 'a) -> xml -> 'a option
+val of_string: string -> xml
+val to_string: xml -> string
+val of_int: int -> xml
+val to_int: xml -> int
+val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml
+val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b
+val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml
+val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union
+val of_edit_id: int -> xml
+val to_edit_id: xml -> int
+val of_loc : Loc.t -> xml
+val to_loc : xml -> Loc.t
+val of_xml : xml -> xml
+val to_xml : xml -> xml
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
new file mode 100644
index 000000000..d1d6de9ae
--- /dev/null
+++ b/ide/texmacspp.ml
@@ -0,0 +1,762 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Xml_datatype
+open Vernacexpr
+open Constrexpr
+open Names
+open Misctypes
+open Bigint
+open Decl_kinds
+open Extend
+open Libnames
+
+let unlock loc =
+ let start, stop = Loc.unloc loc in
+ (string_of_int start, string_of_int stop)
+
+let xmlWithLoc loc ename attr xml =
+ let start, stop = unlock loc in
+ Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
+
+let get_fst_attr_in_xml_list attr xml_list =
+ let attrs_list =
+ List.map (function
+ | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
+ | _ -> [])
+ xml_list in
+ match List.flatten attrs_list with
+ | [] -> (attr, "")
+ | l -> (List.hd l)
+
+let backstep_loc xmllist =
+ let start_att = get_fst_attr_in_xml_list "begin" xmllist in
+ let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in
+ [start_att ; stop_att]
+
+let compare_begin_att xml1 xml2 =
+ let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
+ let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
+ match att1, att2 with
+ | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
+ | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
+ | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
+ | _ -> 0
+
+let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] []
+
+let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] []
+
+let xmlThm typ name loc xml =
+ xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
+
+let xmlDef typ name loc xml =
+ xmlWithLoc loc "definition" ["type", typ; "name", name] xml
+
+let xmlNotation attr name loc xml =
+ xmlWithLoc loc "notation" (("name", name) :: attr) xml
+
+let xmlReservedNotation attr name loc =
+ xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
+
+let xmlCst name ?(attr=[]) loc =
+ xmlWithLoc loc "constant" (("name", name) :: attr) []
+
+let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
+ xmlWithLoc loc "operator"
+ (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
+
+let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml
+
+let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml
+
+let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
+
+let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
+
+let xmlCase xml = Element("case", [], xml)
+
+let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
+
+let xmlWith xml = Element("with", [], xml)
+
+let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
+
+let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml
+
+let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
+
+let xmlFixpoint xml = Element("fixpoint", [], xml)
+
+let xmlCheck loc xml = xmlWithLoc loc "check" [] xml
+
+let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
+
+let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
+
+let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
+
+let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
+
+let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
+
+let xmlReference ref =
+ let name = Libnames.string_of_reference ref in
+ let i, j = Loc.unloc (Libnames.loc_of_reference ref) in
+ let b, e = string_of_int i, string_of_int j in
+ Element("reference",["name", name; "begin", b; "end", e] ,[])
+
+let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
+let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
+
+let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
+let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
+let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
+
+let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
+
+let xmlScope loc action ?(attr=[]) name xml =
+ xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml
+
+let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
+
+let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
+
+let xmlRawTactic name rtac =
+ Element("rawtactic", ["name",name],
+ [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))])
+
+let xmlSectionSubsetDescr name ssd =
+ Element("sectionsubsetdescr",["name",name],
+ [PCData (Proof_using.to_string ssd)])
+
+let xmlDeclareMLModule loc s =
+ xmlWithLoc loc "declarexmlmodule" []
+ (List.map (fun x -> Element("path",["value",x],[])) s)
+
+(* tactics *)
+let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml
+
+(* toplevel commands *)
+let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml
+
+let xmlTODO loc x =
+ xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+let string_of_name n =
+ match n with
+ | Anonymous -> "_"
+ | Name id -> Id.to_string id
+
+let string_of_glob_sort s =
+ match s with
+ | GProp -> "Prop"
+ | GSet -> "Set"
+ | GType _ -> "Type"
+
+let string_of_cast_sort c =
+ match c with
+ | CastConv _ -> "CastConv"
+ | CastVM _ -> "CastVM"
+ | CastNative _ -> "CastNative"
+ | CastCoerce -> "CastCoerce"
+
+let string_of_case_style s =
+ match s with
+ | LetStyle -> "Let"
+ | IfStyle -> "If"
+ | LetPatternStyle -> "LetPattern"
+ | MatchStyle -> "Match"
+ | RegularStyle -> "Regular"
+
+let attribute_of_syntax_modifier sm =
+match sm with
+ | SetItemLevel (sl, NumLevel n) ->
+ List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
+ | SetItemLevel (sl, NextLevel) ->
+ List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
+ | SetLevel i -> ["level", string_of_int i]
+ | SetAssoc a ->
+ begin match a with
+ | NonA -> ["",""]
+ | RightA -> ["associativity", "right"]
+ | LeftA -> ["associativity", "left"]
+ end
+ | SetEntryType (s, _) -> ["entrytype", s]
+ | SetOnlyParsing v -> ["compat", Flags.pr_version v]
+ | SetFormat (system, (loc, s)) ->
+ let start, stop = unlock loc in
+ ["format-"^system, s; "begin", start; "end", stop]
+
+let string_of_assumption_kind l a many =
+ match l, a, many with
+ | (Discharge, Logical, true) -> "Hypotheses"
+ | (Discharge, Logical, false) -> "Hypothesis"
+ | (Discharge, Definitional, true) -> "Variables"
+ | (Discharge, Definitional, false) -> "Variable"
+ | (Global, Logical, true) -> "Axioms"
+ | (Global, Logical, false) -> "Axiom"
+ | (Global, Definitional, true) -> "Parameters"
+ | (Global, Definitional, false) -> "Parameter"
+ | (Local, Logical, true) -> "Local Axioms"
+ | (Local, Logical, false) -> "Local Axiom"
+ | (Local, Definitional, true) -> "Local Parameters"
+ | (Local, Definitional, false) -> "Local Parameter"
+ | (Global, Conjectural, _) -> "Conjecture"
+ | ((Discharge | Local), Conjectural, _) -> assert false
+
+let rec pp_bindlist bl =
+ let tlist =
+ List.flatten
+ (List.map
+ (fun (loc_names, _, e) ->
+ let names =
+ (List.map
+ (fun (loc, name) ->
+ xmlCst (string_of_name name) loc) loc_names) in
+ match e with
+ | CHole _ -> names
+ | _ -> names @ [pp_expr e])
+ bl) in
+ match tlist with
+ | [e] -> e
+ | l -> xmlTyped l
+and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
+ Element ("decl_notation", ["name", s], [pp_expr ce])
+and pp_local_binder lb = (* don't know what it is for now *)
+ match lb with
+ | LocalRawDef ((_, nam), ce) ->
+ let attrs = ["name", string_of_name nam] in
+ pp_expr ~attr:attrs ce
+ | LocalRawAssum (namll, _, ce) ->
+ let ppl =
+ List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
+ xmlTyped (ppl @ [pp_expr ce])
+and pp_local_decl_expr lde = (* don't know what it is for now *)
+ match lde with
+ | AssumExpr (_, ce) -> pp_expr ce
+ | DefExpr (_, ce, _) -> pp_expr ce
+and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
+ (* inductive_expr *)
+ let b,e = Loc.unloc l in
+ let location = ["begin", string_of_int b; "end", string_of_int e] in
+ [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
+ begin match cl_or_rdexpr with
+ | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
+ | RecordDecl (_, ldewwwl) ->
+ List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
+ end @
+ begin match ceo with (* don't know what it is for now *)
+ | Some ce -> [pp_expr ce]
+ | None -> []
+ end @
+ (List.map pp_local_binder lbl)
+and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
+ let attrs =
+ match optid with
+ | None -> []
+ | Some (loc, id) ->
+ let start, stop = unlock loc in
+ ["begin", start; "end", stop ; "name", Id.to_string id] in
+ let kind, expr =
+ match roe with
+ | CStructRec -> "struct", []
+ | CWfRec e -> "rec", [pp_expr e]
+ | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
+ | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
+ Element ("recursion_order", ["kind", kind] @ attrs, expr)
+and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
+ (* fixpoint_expr *)
+ let start, stop = unlock loc in
+ let id = Id.to_string id in
+ [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
+ (* fixpoint name *)
+ [pp_recursion_order_expr optid roe] @
+ (List.map pp_local_binder lbl) @
+ [pp_expr ce] @
+ begin match ceo with (* don't know what it is for now *)
+ | Some ce -> [pp_expr ce]
+ | None -> []
+ end
+and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
+ (* Nota: it is like fixpoint_expr without (optid, roe)
+ * so could be merged if there is no more differences *)
+ let start, stop = unlock loc in
+ let id = Id.to_string id in
+ [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
+ (* cofixpoint name *)
+ (List.map pp_local_binder lbl) @
+ [pp_expr ce] @
+ begin match ceo with (* don't know what it is for now *)
+ | Some ce -> [pp_expr ce]
+ | None -> []
+ end
+and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
+and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
+and pp_cases_pattern_expr cpe =
+ match cpe with
+ | CPatAlias (loc, cpe, id) ->
+ xmlApply loc
+ (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
+ [pp_cases_pattern_expr cpe])
+ | CPatCstr (loc, ref, None, cpel2) ->
+ xmlApply loc
+ (xmlOperator "reference"
+ ~attr:["name", Libnames.string_of_reference ref] loc ::
+ [Element ("impargs", [], []);
+ Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
+ | CPatCstr (loc, ref, Some cpel1, cpel2) ->
+ xmlApply loc
+ (xmlOperator "reference"
+ ~attr:["name", Libnames.string_of_reference ref] loc ::
+ [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
+ Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
+ | CPatAtom (loc, optr) ->
+ let attrs = match optr with
+ | None -> []
+ | Some r -> ["name", Libnames.string_of_reference r] in
+ xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
+ | CPatOr (loc, cpel) ->
+ xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
+ | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
+ xmlApply loc
+ (xmlOperator "notation" loc ::
+ [xmlOperator n loc;
+ Element ("subst", [],
+ [Element ("subterms", [],
+ List.map pp_cases_pattern_expr subst_constr);
+ Element ("recsubterms", [],
+ List.map
+ (fun (cpel) ->
+ Element ("recsubterm", [],
+ List.map pp_cases_pattern_expr cpel))
+ subst_rec)]);
+ Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
+ | CPatPrim (loc, tok) -> pp_token loc tok
+ | CPatRecord (loc, rcl) ->
+ xmlApply loc
+ (xmlOperator "record" loc ::
+ List.map (fun (r, cpe) ->
+ Element ("field",
+ ["reference", Libnames.string_of_reference r],
+ [pp_cases_pattern_expr cpe]))
+ rcl)
+ | CPatDelimiters (loc, delim, cpe) ->
+ xmlApply loc
+ (xmlOperator "delimiter" ~attr:["name", delim] loc ::
+ [pp_cases_pattern_expr cpe])
+and pp_case_expr (e, name, pat) =
+ match name, pat with
+ | None, None -> xmlScrutinee [pp_expr e]
+ | Some (loc, name), None ->
+ let start, stop= unlock loc in
+ xmlScrutinee ~attr:["name", string_of_name name;
+ "begin", start; "end", stop] [pp_expr e]
+ | Some (loc, name), Some p ->
+ let start, stop= unlock loc in
+ xmlScrutinee ~attr:["name", string_of_name name;
+ "begin", start; "end", stop]
+ [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
+ | None, Some p ->
+ xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
+and pp_branch_expr_list bel =
+ xmlWith
+ (List.map
+ (fun (_, cpel, e) ->
+ let ppcepl =
+ List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
+ let ppe = [pp_expr e] in
+ xmlCase (ppcepl @ ppe))
+ bel)
+and pp_token loc tok =
+ let tokstr =
+ match tok with
+ | String s -> PCData s
+ | Numeral n -> PCData (to_string n) in
+ xmlToken loc [tokstr]
+and pp_local_binder_list lbl =
+ let l = (List.map pp_local_binder lbl) in
+ Element ("recurse", (backstep_loc l), l)
+and pp_const_expr_list cel =
+ let l = List.map pp_expr cel in
+ Element ("recurse", (backstep_loc l), l)
+and pp_expr ?(attr=[]) e =
+ match e with
+ | CRef (r, _) ->
+ xmlCst ~attr
+ (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
+ | CProdN (loc, bl, e) ->
+ xmlApply loc
+ (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
+ | CApp (loc, (_, hd), args) ->
+ xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
+ | CAppExpl (loc, (_, r, _), args) ->
+ xmlApply ~attr loc
+ (xmlCst (Libnames.string_of_reference r)
+ (Libnames.loc_of_reference r) :: List.map pp_expr args)
+ | CNotation (loc, notation, ([],[],[])) ->
+ xmlOperator notation loc
+ | CNotation (loc, notation, (args, cell, lbll)) ->
+ let fmts = Notation.find_notation_extra_printing_rules notation in
+ let oper = xmlOperator notation loc ~pprules:fmts in
+ let cels = List.map pp_const_expr_list cell in
+ let lbls = List.map pp_local_binder_list lbll in
+ let args = List.map pp_expr args in
+ xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
+ | CSort(loc, s) ->
+ xmlOperator (string_of_glob_sort s) loc
+ | CDelimiters (loc, scope, ce) ->
+ xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
+ [pp_expr ce])
+ | CPrim (loc, tok) -> pp_token loc tok
+ | CGeneralization (loc, kind, _, e) ->
+ let kind= match kind with
+ | Explicit -> "explicit"
+ | Implicit -> "implicit" in
+ xmlApply loc
+ (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
+ | CCast (loc, e, tc) ->
+ begin match tc with
+ | CastConv t | CastVM t |CastNative t ->
+ xmlApply loc
+ (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] ::
+ [pp_expr e; pp_expr t])
+ | CastCoerce ->
+ xmlApply loc
+ (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
+ [pp_expr e])
+ end
+ | CEvar (loc, ek, cel) ->
+ let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
+ xmlApply loc
+ (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
+ ppcel)
+ | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
+ | CHole (loc, _, _, _) -> xmlCst ~attr "_" loc
+ | CIf (loc, test, (_, ret), th, el) ->
+ let return = match ret with
+ | None -> []
+ | Some r -> [xmlReturn [pp_expr r]] in
+ xmlApply loc
+ (xmlOperator "if" loc ::
+ return @ [pp_expr th] @ [pp_expr el])
+ | CLetTuple (loc, names, (_, ret), value, body) ->
+ let return = match ret with
+ | None -> []
+ | Some r -> [xmlReturn [pp_expr r]] in
+ xmlApply loc
+ (xmlOperator "lettuple" loc ::
+ return @
+ (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
+ [pp_expr value; pp_expr body])
+ | CCases (loc, sty, ret, cel, bel) ->
+ let return = match ret with
+ | None -> []
+ | Some r -> [xmlReturn [pp_expr r]] in
+ xmlApply loc
+ (xmlOperator "match" loc ~attr:["style", (string_of_case_style sty)] ::
+ (return @
+ [Element ("scrutinees", [], List.map pp_case_expr cel)] @
+ [pp_branch_expr_list bel]))
+ | CRecord (_, _) -> assert false
+ | CLetIn (loc, (varloc, var), value, body) ->
+ xmlApply loc
+ (xmlOperator "let" loc ::
+ [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
+ | CLambdaN (loc, bl, e) ->
+ xmlApply loc
+ (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
+ | CCoFix (_, _, _) -> assert false
+ | CFix (loc, lid, fel) ->
+ xmlApply loc
+ (xmlOperator "fix" loc ::
+ List.flatten (List.map
+ (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
+ fel))
+
+let pp_comment (c) =
+ match c with
+ | CommentConstr e -> [pp_expr e]
+ | CommentString s -> [Element ("string", [], [PCData s])]
+ | CommentInt i -> [PCData (string_of_int i)]
+
+let rec tmpp v loc =
+ match v with
+ (* Control *)
+ | VernacLoad (verbose,f) ->
+ xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
+ | VernacTime (loc,e) ->
+ xmlApply loc (Element("time",[],[]) ::
+ [tmpp e loc])
+ | VernacRedirect (s, (loc,e)) ->
+ xmlApply loc (Element("redirect",["path", s],[]) ::
+ [tmpp e loc])
+ | VernacTimeout (s,e) ->
+ xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
+ [tmpp e loc])
+ | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
+ | VernacError _ -> xmlWithLoc loc "error" [] []
+
+ (* Syntax *)
+ | VernacSyntaxExtension (_, ((_, name), sml)) ->
+ let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+ xmlReservedNotation attrs name loc
+
+ | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
+ | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
+ | VernacDelimiters (name,Some tag) ->
+ xmlScope loc "delimit" name ~attr:["delimiter",tag] []
+ | VernacDelimiters (name,None) ->
+ xmlScope loc "undelimit" name ~attr:[] []
+ | VernacInfix (_,((_,name),sml),ce,sn) ->
+ let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+ let sc_attr =
+ match sn with
+ | Some scope -> ["scope", scope]
+ | None -> [] in
+ xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
+ | VernacNotation (_, ce, (lstr, sml), sn) ->
+ let name = snd lstr in
+ let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+ let sc_attr =
+ match sn with
+ | Some scope -> ["scope", scope]
+ | None -> [] in
+ xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
+ | VernacBindScope _ as x -> xmlTODO loc x
+ | VernacNotationAddFormat _ as x -> xmlTODO loc x
+ | VernacUniverse _
+ | VernacConstraint _
+ | VernacPolymorphic (_, _) as x -> xmlTODO loc x
+ (* Gallina *)
+ | VernacDefinition (ldk, ((_,id),_), de) ->
+ let l, dk =
+ match ldk with
+ | Some l, dk -> (l, dk)
+ | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
+ let e =
+ match de with
+ | ProveBody (_, ce) -> ce
+ | DefineBody (_, Some _, ce, None) -> ce
+ | DefineBody (_, None , ce, None) -> ce
+ | DefineBody (_, Some _, ce, Some _) -> ce
+ | DefineBody (_, None , ce, Some _) -> ce in
+ let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
+ let str_id = Id.to_string id in
+ (xmlDef str_dk str_id loc [pp_expr e])
+ | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
+ let str_tk = Kindops.string_of_theorem_kind tk in
+ let str_id = Id.to_string id in
+ (xmlThm str_tk str_id loc [pp_expr statement])
+ | VernacStartTheoremProof _ as x -> xmlTODO loc x
+ | VernacEndProof pe ->
+ begin
+ match pe with
+ | Admitted -> xmlQed loc
+ | Proved (_, Some ((_, id), Some tk)) ->
+ let nam = Id.to_string id in
+ let typ = Kindops.string_of_theorem_kind tk in
+ xmlQed ~attr:["name", nam; "type", typ] loc
+ | Proved (_, Some ((_, id), None)) ->
+ let nam = Id.to_string id in
+ xmlQed ~attr:["name", nam] loc
+ | Proved _ -> xmlQed loc
+ end
+ | VernacExactProof _ as x -> xmlTODO loc x
+ | VernacAssumption ((l, a), _, sbwcl) ->
+ let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
+ let many =
+ List.length (List.flatten (List.map fst binders)) > 1 in
+ let exprs =
+ List.flatten (List.map pp_simple_binder binders) in
+ let l = match l with Some x -> x | None -> Decl_kinds.Global in
+ let kind = string_of_assumption_kind l a many in
+ xmlAssumption kind loc exprs
+ | VernacInductive (_, _, iednll) ->
+ let kind =
+ let (_, _, _, k, _),_ = List.hd iednll in
+ begin
+ match k with
+ | Record -> "Record"
+ | Structure -> "Structure"
+ | Inductive_kw -> "Inductive"
+ | CoInductive -> "CoInductive"
+ | Class _ -> "Class"
+ | Variant -> "Variant"
+ end in
+ let exprs =
+ List.flatten (* should probably not be flattened *)
+ (List.map
+ (fun (ie, dnl) -> (pp_inductive_expr ie) @
+ (List.map pp_decl_notation dnl)) iednll) in
+ xmlInductive kind loc exprs
+ | VernacFixpoint (_, fednll) ->
+ let exprs =
+ List.flatten (* should probably not be flattened *)
+ (List.map
+ (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
+ (List.map pp_decl_notation dnl)) fednll) in
+ xmlFixpoint exprs
+ | VernacCoFixpoint (_, cfednll) ->
+ (* Nota: it is like VernacFixpoint without so could be merged *)
+ let exprs =
+ List.flatten (* should probably not be flattened *)
+ (List.map
+ (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
+ (List.map pp_decl_notation dnl)) cfednll) in
+ xmlCoFixpoint exprs
+ | VernacScheme _ as x -> xmlTODO loc x
+ | VernacCombinedScheme _ as x -> xmlTODO loc x
+
+ (* Gallina extensions *)
+ | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
+ | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
+ | VernacNameSectionHypSet _ as x -> xmlTODO loc x
+ | VernacRequire (from, import, l) ->
+ let import = match import with
+ | None -> []
+ | Some true -> ["export","true"]
+ | Some false -> ["import","true"]
+ in
+ let from = match from with
+ | None -> []
+ | Some r -> ["from", Libnames.string_of_reference r]
+ in
+ xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
+ xmlReference ref) l)
+ | VernacImport (true,l) ->
+ xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
+ xmlReference ref) l)
+ | VernacImport (false,l) ->
+ xmlImport loc (List.map (fun ref ->
+ xmlReference ref) l)
+ | VernacCanonical r ->
+ let attr =
+ match r with
+ | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
+ | AN (Ident (_, id)) -> ["id", Id.to_string id]
+ | ByNotation (_, s, _) -> ["notation", s] in
+ xmlCanonicalStructure attr loc
+ | VernacCoercion _ as x -> xmlTODO loc x
+ | VernacIdentityCoercion _ as x -> xmlTODO loc x
+
+ (* Type classes *)
+ | VernacInstance _ as x -> xmlTODO loc x
+
+ | VernacContext _ as x -> xmlTODO loc x
+
+ | VernacDeclareInstances _ as x -> xmlTODO loc x
+
+ | VernacDeclareClass _ as x -> xmlTODO loc x
+
+ (* Modules and Module Types *)
+ | VernacDeclareModule _ as x -> xmlTODO loc x
+ | VernacDefineModule _ as x -> xmlTODO loc x
+ | VernacDeclareModuleType _ as x -> xmlTODO loc x
+ | VernacInclude _ as x -> xmlTODO loc x
+
+ (* Solving *)
+
+ | (VernacSolveExistential _) as x ->
+ xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+ (* Auxiliary file and library management *)
+ | VernacAddLoadPath (recf,name,None) ->
+ xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] []
+ | VernacAddLoadPath (recf,name,Some dp) ->
+ xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name]
+ [PCData (Names.DirPath.to_string dp)]
+ | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] []
+ | VernacAddMLPath (recf,name) ->
+ xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
+ | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
+ | VernacChdir _ as x -> xmlTODO loc x
+
+ (* State management *)
+ | VernacWriteState _ as x -> xmlTODO loc x
+ | VernacRestoreState _ as x -> xmlTODO loc x
+
+ (* Resetting *)
+ | VernacResetName _ as x -> xmlTODO loc x
+ | VernacResetInitial as x -> xmlTODO loc x
+ | VernacBack _ as x -> xmlTODO loc x
+ | VernacBackTo _ -> PCData "VernacBackTo"
+
+ (* Commands *)
+ | VernacCreateHintDb _ as x -> xmlTODO loc x
+ | VernacRemoveHints _ as x -> xmlTODO loc x
+ | VernacHints _ as x -> xmlTODO loc x
+ | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
+ let name = Id.to_string name in
+ let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
+ xmlNotation attrs name loc [pp_expr ce]
+ | VernacDeclareImplicits _ as x -> xmlTODO loc x
+ | VernacArguments _ as x -> xmlTODO loc x
+ | VernacArgumentsScope _ as x -> xmlTODO loc x
+ | VernacReserve _ as x -> xmlTODO loc x
+ | VernacGeneralizable _ as x -> xmlTODO loc x
+ | VernacSetOpacity _ as x -> xmlTODO loc x
+ | VernacSetStrategy _ as x -> xmlTODO loc x
+ | VernacUnsetOption _ as x -> xmlTODO loc x
+ | VernacSetOption _ as x -> xmlTODO loc x
+ | VernacAddOption _ as x -> xmlTODO loc x
+ | VernacRemoveOption _ as x -> xmlTODO loc x
+ | VernacMemOption _ as x -> xmlTODO loc x
+ | VernacPrintOption _ as x -> xmlTODO loc x
+ | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e]
+ | VernacGlobalCheck _ as x -> xmlTODO loc x
+ | VernacDeclareReduction _ as x -> xmlTODO loc x
+ | VernacPrint _ as x -> xmlTODO loc x
+ | VernacSearch _ as x -> xmlTODO loc x
+ | VernacLocate _ as x -> xmlTODO loc x
+ | VernacRegister _ as x -> xmlTODO loc x
+ | VernacComments (cl) ->
+ xmlComment loc (List.flatten (List.map pp_comment cl))
+
+ (* Stm backdoor *)
+ | VernacStm _ as x -> xmlTODO loc x
+
+ (* Proof management *)
+ | VernacGoal _ as x -> xmlTODO loc x
+ | VernacAbort _ as x -> xmlTODO loc x
+ | VernacAbortAll -> PCData "VernacAbortAll"
+ | VernacRestart as x -> xmlTODO loc x
+ | VernacUndo _ as x -> xmlTODO loc x
+ | VernacUndoTo _ as x -> xmlTODO loc x
+ | VernacBacktrack _ as x -> xmlTODO loc x
+ | VernacFocus _ as x -> xmlTODO loc x
+ | VernacUnfocus as x -> xmlTODO loc x
+ | VernacUnfocused as x -> xmlTODO loc x
+ | VernacBullet _ as x -> xmlTODO loc x
+ | VernacSubproof _ as x -> xmlTODO loc x
+ | VernacEndSubproof as x -> xmlTODO loc x
+ | VernacShow _ as x -> xmlTODO loc x
+ | VernacCheckGuard as x -> xmlTODO loc x
+ | VernacProof (tac,using) ->
+ let tac = Option.map (xmlRawTactic "closingtactic") tac in
+ let using = Option.map (xmlSectionSubsetDescr "using") using in
+ xmlProof loc (Option.List.(cons tac (cons using [])))
+ | VernacProofMode name -> xmlProofMode loc name
+
+ (* Toplevel control *)
+ | VernacToplevelControl _ as x -> xmlTODO loc x
+
+ (* For extension *)
+ | VernacExtend _ as x ->
+ xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+ (* Flags *)
+ | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc])
+ | VernacLocal (b,e) ->
+ xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
+ [tmpp e loc])
+
+let tmpp v loc =
+ match tmpp v loc with
+ | Element("ltac",_,_) as x -> x
+ | xml -> xmlGallina loc [xml]
diff --git a/ide/texmacspp.mli b/ide/texmacspp.mli
new file mode 100644
index 000000000..858847fb6
--- /dev/null
+++ b/ide/texmacspp.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Xml_datatype
+open Vernacexpr
+
+val tmpp : vernac_expr -> Loc.t -> xml
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index c2799e40b..dbc1740ef 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -60,6 +60,8 @@ object (self)
val mutable default : color = `WHITE
val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
val clicked = new GUtil.signal ()
+ val mutable need_refresh = false
+ val refresh_timer = Ideutils.mktimer ()
initializer
box#misc#set_size_request ~height ();
@@ -88,13 +90,15 @@ object (self)
let cb show = if show then self#misc#show () else self#misc#hide () in
stick show_progress_bar self cb;
(** Initial pixmap *)
- draw#set_pixmap pixmap
+ draw#set_pixmap pixmap;
+ refresh_timer.Ideutils.run ~ms:300
+ ~callback:(fun () -> if need_refresh then self#refresh (); true)
method set_model md =
model <- Some md;
let changed_cb = function
| `INSERT | `REMOVE ->
- if self#misc#visible then self#refresh ()
+ if self#misc#visible then need_refresh <- true
| `SET (i, color) ->
if self#misc#visible then self#fill_range color i (i + 1)
in
@@ -125,6 +129,7 @@ object (self)
method private refresh () = match model with
| None -> ()
| Some md ->
+ need_refresh <- false;
pixmap#set_foreground default;
pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true ();
let make (k, cur, accu) v = match cur with
diff --git a/ide/xml_lexer.mli b/ide/xml_lexer.mli
new file mode 100644
index 000000000..e61cb055f
--- /dev/null
+++ b/ide/xml_lexer.mli
@@ -0,0 +1,44 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+type error =
+ | EUnterminatedComment
+ | EUnterminatedString
+ | EIdentExpected
+ | ECloseExpected
+ | ENodeExpected
+ | EAttributeNameExpected
+ | EAttributeValueExpected
+ | EUnterminatedEntity
+
+exception Error of error
+
+type token =
+ | Tag of string * (string * string) list * bool
+ | PCData of string
+ | Endtag of string
+ | Eof
+
+type pos = int * int * int * int
+
+val init : Lexing.lexbuf -> unit
+val close : unit -> unit
+val token : Lexing.lexbuf -> token
+val pos : Lexing.lexbuf -> pos
+val restore : pos -> unit
diff --git a/ide/xml_lexer.mll b/ide/xml_lexer.mll
new file mode 100644
index 000000000..290f2c89a
--- /dev/null
+++ b/ide/xml_lexer.mll
@@ -0,0 +1,317 @@
+{(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+open Lexing
+
+type error =
+ | EUnterminatedComment
+ | EUnterminatedString
+ | EIdentExpected
+ | ECloseExpected
+ | ENodeExpected
+ | EAttributeNameExpected
+ | EAttributeValueExpected
+ | EUnterminatedEntity
+
+exception Error of error
+
+type pos = int * int * int * int
+
+type token =
+ | Tag of string * (string * string) list * bool
+ | PCData of string
+ | Endtag of string
+ | Eof
+
+let last_pos = ref 0
+and current_line = ref 0
+and current_line_start = ref 0
+
+let tmp = Buffer.create 200
+
+let idents = Hashtbl.create 0
+
+let _ = begin
+ Hashtbl.add idents "nbsp;" " ";
+ Hashtbl.add idents "gt;" ">";
+ Hashtbl.add idents "lt;" "<";
+ Hashtbl.add idents "amp;" "&";
+ Hashtbl.add idents "apos;" "'";
+ Hashtbl.add idents "quot;" "\"";
+end
+
+let init lexbuf =
+ current_line := 1;
+ current_line_start := lexeme_start lexbuf;
+ last_pos := !current_line_start
+
+let close lexbuf =
+ Buffer.reset tmp
+
+let pos lexbuf =
+ !current_line , !current_line_start ,
+ !last_pos ,
+ lexeme_start lexbuf
+
+let restore (cl,cls,lp,_) =
+ current_line := cl;
+ current_line_start := cls;
+ last_pos := lp
+
+let newline lexbuf =
+ incr current_line;
+ last_pos := lexeme_end lexbuf;
+ current_line_start := !last_pos
+
+let error lexbuf e =
+ last_pos := lexeme_start lexbuf;
+ raise (Error e)
+
+}
+
+let newline = ['\n']
+let break = ['\r']
+let space = [' ' '\t']
+let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.']
+let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar*
+let entitychar = ['A'-'Z' 'a'-'z']
+let pcchar = [^ '\r' '\n' '<' '>' '&']
+
+rule token = parse
+ | newline | (newline break) | break
+ {
+ newline lexbuf;
+ PCData "\n"
+ }
+ | "<!--"
+ {
+ last_pos := lexeme_start lexbuf;
+ comment lexbuf;
+ token lexbuf
+ }
+ | "<?"
+ {
+ last_pos := lexeme_start lexbuf;
+ header lexbuf;
+ token lexbuf;
+ }
+ | '<' space* '/' space*
+ {
+ last_pos := lexeme_start lexbuf;
+ let tag = ident_name lexbuf in
+ ignore_spaces lexbuf;
+ close_tag lexbuf;
+ Endtag tag
+ }
+ | '<' space*
+ {
+ last_pos := lexeme_start lexbuf;
+ let tag = ident_name lexbuf in
+ ignore_spaces lexbuf;
+ let attribs, closed = attributes lexbuf in
+ Tag(tag, attribs, closed)
+ }
+ | "&#"
+ {
+ last_pos := lexeme_start lexbuf;
+ Buffer.reset tmp;
+ Buffer.add_string tmp (lexeme lexbuf);
+ PCData (pcdata lexbuf)
+ }
+ | '&'
+ {
+ last_pos := lexeme_start lexbuf;
+ Buffer.reset tmp;
+ Buffer.add_string tmp (entity lexbuf);
+ PCData (pcdata lexbuf)
+ }
+ | pcchar+
+ {
+ last_pos := lexeme_start lexbuf;
+ Buffer.reset tmp;
+ Buffer.add_string tmp (lexeme lexbuf);
+ PCData (pcdata lexbuf)
+ }
+ | eof { Eof }
+ | _
+ { error lexbuf ENodeExpected }
+
+and ignore_spaces = parse
+ | newline | (newline break) | break
+ {
+ newline lexbuf;
+ ignore_spaces lexbuf
+ }
+ | space +
+ { ignore_spaces lexbuf }
+ | ""
+ { () }
+
+and comment = parse
+ | newline | (newline break) | break
+ {
+ newline lexbuf;
+ comment lexbuf
+ }
+ | "-->"
+ { () }
+ | eof
+ { raise (Error EUnterminatedComment) }
+ | _
+ { comment lexbuf }
+
+and header = parse
+ | newline | (newline break) | break
+ {
+ newline lexbuf;
+ header lexbuf
+ }
+ | "?>"
+ { () }
+ | eof
+ { error lexbuf ECloseExpected }
+ | _
+ { header lexbuf }
+
+and pcdata = parse
+ | newline | (newline break) | break
+ {
+ Buffer.add_char tmp '\n';
+ newline lexbuf;
+ pcdata lexbuf
+ }
+ | pcchar+
+ {
+ Buffer.add_string tmp (lexeme lexbuf);
+ pcdata lexbuf
+ }
+ | "&#"
+ {
+ Buffer.add_string tmp (lexeme lexbuf);
+ pcdata lexbuf;
+ }
+ | '&'
+ {
+ Buffer.add_string tmp (entity lexbuf);
+ pcdata lexbuf
+ }
+ | ""
+ { Buffer.contents tmp }
+
+and entity = parse
+ | entitychar+ ';'
+ {
+ let ident = lexeme lexbuf in
+ try
+ Hashtbl.find idents (String.lowercase ident)
+ with
+ Not_found -> "&" ^ ident
+ }
+ | _ | eof
+ { raise (Error EUnterminatedEntity) }
+
+and ident_name = parse
+ | ident
+ { lexeme lexbuf }
+ | _ | eof
+ { error lexbuf EIdentExpected }
+
+and close_tag = parse
+ | '>'
+ { () }
+ | _ | eof
+ { error lexbuf ECloseExpected }
+
+and attributes = parse
+ | '>'
+ { [], false }
+ | "/>"
+ { [], true }
+ | "" (* do not read a char ! *)
+ {
+ let key = attribute lexbuf in
+ let data = attribute_data lexbuf in
+ ignore_spaces lexbuf;
+ let others, closed = attributes lexbuf in
+ (key, data) :: others, closed
+ }
+
+and attribute = parse
+ | ident
+ { lexeme lexbuf }
+ | _ | eof
+ { error lexbuf EAttributeNameExpected }
+
+and attribute_data = parse
+ | space* '=' space* '"'
+ {
+ Buffer.reset tmp;
+ last_pos := lexeme_end lexbuf;
+ dq_string lexbuf
+ }
+ | space* '=' space* '\''
+ {
+ Buffer.reset tmp;
+ last_pos := lexeme_end lexbuf;
+ q_string lexbuf
+ }
+ | _ | eof
+ { error lexbuf EAttributeValueExpected }
+
+and dq_string = parse
+ | '"'
+ { Buffer.contents tmp }
+ | '\\' [ '"' '\\' ]
+ {
+ Buffer.add_char tmp (lexeme_char lexbuf 1);
+ dq_string lexbuf
+ }
+ | '&'
+ {
+ Buffer.add_string tmp (entity lexbuf);
+ dq_string lexbuf
+ }
+ | eof
+ { raise (Error EUnterminatedString) }
+ | _
+ {
+ Buffer.add_char tmp (lexeme_char lexbuf 0);
+ dq_string lexbuf
+ }
+
+and q_string = parse
+ | '\''
+ { Buffer.contents tmp }
+ | '\\' [ '\'' '\\' ]
+ {
+ Buffer.add_char tmp (lexeme_char lexbuf 1);
+ q_string lexbuf
+ }
+ | '&'
+ {
+ Buffer.add_string tmp (entity lexbuf);
+ q_string lexbuf
+ }
+ | eof
+ { raise (Error EUnterminatedString) }
+ | _
+ {
+ Buffer.add_char tmp (lexeme_char lexbuf 0);
+ q_string lexbuf
+ }
diff --git a/ide/xml_parser.ml b/ide/xml_parser.ml
new file mode 100644
index 000000000..8db3f9e8b
--- /dev/null
+++ b/ide/xml_parser.ml
@@ -0,0 +1,232 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ * Copyright (C) 2003 Jacques Garrigue
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+open Printf
+open Xml_datatype
+
+type xml = Xml_datatype.xml
+
+type error_pos = {
+ eline : int;
+ eline_start : int;
+ emin : int;
+ emax : int;
+}
+
+type error_msg =
+ | UnterminatedComment
+ | UnterminatedString
+ | UnterminatedEntity
+ | IdentExpected
+ | CloseExpected
+ | NodeExpected
+ | AttributeNameExpected
+ | AttributeValueExpected
+ | EndOfTagExpected of string
+ | EOFExpected
+ | Empty
+
+type error = error_msg * error_pos
+
+exception Error of error
+
+exception File_not_found of string
+
+type t = {
+ mutable check_eof : bool;
+ mutable concat_pcdata : bool;
+ source : Lexing.lexbuf;
+ stack : Xml_lexer.token Stack.t;
+}
+
+type source =
+ | SChannel of in_channel
+ | SString of string
+ | SLexbuf of Lexing.lexbuf
+
+exception Internal_error of error_msg
+exception NoMoreData
+
+let xml_error = ref (fun _ -> assert false)
+let file_not_found = ref (fun _ -> assert false)
+
+let is_blank s =
+ let len = String.length s in
+ let break = ref true in
+ let i = ref 0 in
+ while !break && !i < len do
+ let c = s.[!i] in
+ (* no '\r' because we replaced them in the lexer *)
+ if c = ' ' || c = '\n' || c = '\t' then incr i
+ else break := false
+ done;
+ !i = len
+
+let _raises e f =
+ xml_error := e;
+ file_not_found := f
+
+let make source =
+ let source = match source with
+ | SChannel chan -> Lexing.from_channel chan
+ | SString s -> Lexing.from_string s
+ | SLexbuf lexbuf -> lexbuf
+ in
+ let () = Xml_lexer.init source in
+ {
+ check_eof = false;
+ concat_pcdata = true;
+ source = source;
+ stack = Stack.create ();
+ }
+
+let check_eof p v = p.check_eof <- v
+
+let pop s =
+ try
+ Stack.pop s.stack
+ with
+ Stack.Empty ->
+ Xml_lexer.token s.source
+
+let push t s =
+ Stack.push t s.stack
+
+let canonicalize l =
+ let has_elt = List.exists (function Element _ -> true | _ -> false) l in
+ if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l
+ else l
+
+let rec read_xml do_not_canonicalize s =
+ let rec read_node s =
+ match pop s with
+ | Xml_lexer.PCData s -> PCData s
+ | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, [])
+ | Xml_lexer.Tag (tag, attr, false) ->
+ let elements = read_elems tag s in
+ let elements =
+ if do_not_canonicalize then elements else canonicalize elements
+ in
+ Element (tag, attr, elements)
+ | t ->
+ push t s;
+ raise NoMoreData
+
+ and read_elems tag s =
+ let elems = ref [] in
+ (try
+ while true do
+ let node = read_node s in
+ match node, !elems with
+ | PCData c , (PCData c2) :: q ->
+ elems := PCData (c2 ^ c) :: q
+ | _, l ->
+ elems := node :: l
+ done
+ with
+ NoMoreData -> ());
+ match pop s with
+ | Xml_lexer.Endtag s when s = tag -> List.rev !elems
+ | t -> raise (Internal_error (EndOfTagExpected tag))
+ in
+ match read_node s with
+ | (Element _) as node ->
+ node
+ | PCData c ->
+ if is_blank c then
+ read_xml do_not_canonicalize s
+ else
+ raise (Xml_lexer.Error Xml_lexer.ENodeExpected)
+
+let convert = function
+ | Xml_lexer.EUnterminatedComment -> UnterminatedComment
+ | Xml_lexer.EUnterminatedString -> UnterminatedString
+ | Xml_lexer.EIdentExpected -> IdentExpected
+ | Xml_lexer.ECloseExpected -> CloseExpected
+ | Xml_lexer.ENodeExpected -> NodeExpected
+ | Xml_lexer.EAttributeNameExpected -> AttributeNameExpected
+ | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected
+ | Xml_lexer.EUnterminatedEntity -> UnterminatedEntity
+
+let error_of_exn xparser = function
+ | NoMoreData when pop xparser = Xml_lexer.Eof -> Empty
+ | NoMoreData -> NodeExpected
+ | Internal_error e -> e
+ | Xml_lexer.Error e -> convert e
+ | e ->
+ (*let e = Errors.push e in: We do not record backtrace here. *)
+ raise e
+
+let do_parse do_not_canonicalize xparser =
+ try
+ Xml_lexer.init xparser.source;
+ let x = read_xml do_not_canonicalize xparser in
+ if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
+ Xml_lexer.close ();
+ x
+ with any ->
+ Xml_lexer.close ();
+ raise (!xml_error (error_of_exn xparser any) xparser.source)
+
+let parse ?(do_not_canonicalize=false) p =
+ do_parse do_not_canonicalize p
+
+let error_msg = function
+ | UnterminatedComment -> "Unterminated comment"
+ | UnterminatedString -> "Unterminated string"
+ | UnterminatedEntity -> "Unterminated entity"
+ | IdentExpected -> "Ident expected"
+ | CloseExpected -> "Element close expected"
+ | NodeExpected -> "Xml node expected"
+ | AttributeNameExpected -> "Attribute name expected"
+ | AttributeValueExpected -> "Attribute value expected"
+ | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag
+ | EOFExpected -> "End of file expected"
+ | Empty -> "Empty"
+
+let error (msg,pos) =
+ if pos.emin = pos.emax then
+ sprintf "%s line %d character %d" (error_msg msg) pos.eline
+ (pos.emin - pos.eline_start)
+ else
+ sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline
+ (pos.emin - pos.eline_start) (pos.emax - pos.eline_start)
+
+let line e = e.eline
+
+let range e =
+ e.emin - e.eline_start , e.emax - e.eline_start
+
+let abs_range e =
+ e.emin , e.emax
+
+let pos source =
+ let line, lstart, min, max = Xml_lexer.pos source in
+ {
+ eline = line;
+ eline_start = lstart;
+ emin = min;
+ emax = max;
+ }
+
+let () = _raises (fun x p ->
+ (* local cast : Xml.error_msg -> error_msg *)
+ Error (x, pos p))
+ (fun f -> File_not_found f)
diff --git a/ide/xml_parser.mli b/ide/xml_parser.mli
new file mode 100644
index 000000000..ac2eab352
--- /dev/null
+++ b/ide/xml_parser.mli
@@ -0,0 +1,106 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+(** Xml Light Parser
+
+ While basic parsing functions can be used in the {!Xml} module, this module
+ is providing a way to create, configure and run an Xml parser.
+
+*)
+
+
+(** An Xml node is either
+ [Element (tag-name, attributes, children)] or [PCData text] *)
+type xml = Xml_datatype.xml
+
+(** Abstract type for an Xml parser. *)
+type t
+
+(** {6:exc Xml Exceptions} *)
+
+(** Several exceptions can be raised when parsing an Xml document : {ul
+ {li {!Xml.Error} is raised when an xml parsing error occurs. the
+ {!Xml.error_msg} tells you which error occurred during parsing
+ and the {!Xml.error_pos} can be used to retrieve the document
+ location where the error occurred at.}
+ {li {!Xml.File_not_found} is raised when an error occurred while
+ opening a file with the {!Xml.parse_file} function.}
+ }
+ *)
+
+type error_pos
+
+type error_msg =
+ | UnterminatedComment
+ | UnterminatedString
+ | UnterminatedEntity
+ | IdentExpected
+ | CloseExpected
+ | NodeExpected
+ | AttributeNameExpected
+ | AttributeValueExpected
+ | EndOfTagExpected of string
+ | EOFExpected
+ | Empty
+
+type error = error_msg * error_pos
+
+exception Error of error
+
+exception File_not_found of string
+
+(** Get a full error message from an Xml error. *)
+val error : error -> string
+
+(** Get the Xml error message as a string. *)
+val error_msg : error_msg -> string
+
+(** Get the line the error occurred at. *)
+val line : error_pos -> int
+
+(** Get the relative character range (in current line) the error occurred at.*)
+val range : error_pos -> int * int
+
+(** Get the absolute character range the error occurred at. *)
+val abs_range : error_pos -> int * int
+
+val pos : Lexing.lexbuf -> error_pos
+
+(** Several kind of resources can contain Xml documents. *)
+type source =
+| SChannel of in_channel
+| SString of string
+| SLexbuf of Lexing.lexbuf
+
+(** This function returns a new parser with default options. *)
+val make : source -> t
+
+(** When a Xml document is parsed, the parser may check that the end of the
+ document is reached, so for example parsing ["<A/><B/>"] will fail instead
+ of returning only the A element. You can turn on this check by setting
+ [check_eof] to [true] {i (by default, check_eof is false, unlike
+ in the original Xmllight)}. *)
+val check_eof : t -> bool -> unit
+
+(** Once the parser is configured, you can run the parser on a any kind
+ of xml document source to parse its contents into an Xml data structure.
+
+ When [do_not_canonicalize] is set, the XML document is given as
+ is, without trying to remove blank PCDATA elements. *)
+val parse : ?do_not_canonicalize:bool -> t -> xml
diff --git a/ide/xml_printer.ml b/ide/xml_printer.ml
new file mode 100644
index 000000000..e7e4d0ceb
--- /dev/null
+++ b/ide/xml_printer.ml
@@ -0,0 +1,145 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Xml_datatype
+
+type xml = Xml_datatype.xml
+
+type target = TChannel of out_channel | TBuffer of Buffer.t
+
+type t = target
+
+let make x = x
+
+let buffer_pcdata tmp text =
+ let output = Buffer.add_string tmp in
+ let output' = Buffer.add_char tmp in
+ let l = String.length text in
+ for p = 0 to l-1 do
+ match text.[p] with
+ | ' ' -> output "&nbsp;";
+ | '>' -> output "&gt;"
+ | '<' -> output "&lt;"
+ | '&' ->
+ if p < l - 1 && text.[p + 1] = '#' then
+ output' '&'
+ else
+ output "&amp;"
+ | '\'' -> output "&apos;"
+ | '"' -> output "&quot;"
+ | c -> output' c
+ done
+
+let buffer_attr tmp (n,v) =
+ let output = Buffer.add_string tmp in
+ let output' = Buffer.add_char tmp in
+ output' ' ';
+ output n;
+ output "=\"";
+ let l = String.length v in
+ for p = 0 to l - 1 do
+ match v.[p] with
+ | '\\' -> output "\\\\"
+ | '"' -> output "\\\""
+ | '<' -> output "&lt;"
+ | '&' -> output "&amp;"
+ | c -> output' c
+ done;
+ output' '"'
+
+let to_buffer tmp x =
+ let pcdata = ref false in
+ let output = Buffer.add_string tmp in
+ let output' = Buffer.add_char tmp in
+ let rec loop = function
+ | Element (tag,alist,[]) ->
+ output' '<';
+ output tag;
+ List.iter (buffer_attr tmp) alist;
+ output "/>";
+ pcdata := false;
+ | Element (tag,alist,l) ->
+ output' '<';
+ output tag;
+ List.iter (buffer_attr tmp) alist;
+ output' '>';
+ pcdata := false;
+ List.iter loop l;
+ output "</";
+ output tag;
+ output' '>';
+ pcdata := false;
+ | PCData text ->
+ if !pcdata then output' ' ';
+ buffer_pcdata tmp text;
+ pcdata := true;
+ in
+ loop x
+
+let pcdata_to_string s =
+ let b = Buffer.create 13 in
+ buffer_pcdata b s;
+ Buffer.contents b
+
+let to_string x =
+ let b = Buffer.create 200 in
+ to_buffer b x;
+ Buffer.contents b
+
+let to_string_fmt x =
+ let tmp = Buffer.create 200 in
+ let output = Buffer.add_string tmp in
+ let output' = Buffer.add_char tmp in
+ let rec loop ?(newl=false) tab = function
+ | Element (tag, alist, []) ->
+ output tab;
+ output' '<';
+ output tag;
+ List.iter (buffer_attr tmp) alist;
+ output "/>";
+ if newl then output' '\n';
+ | Element (tag, alist, [PCData text]) ->
+ output tab;
+ output' '<';
+ output tag;
+ List.iter (buffer_attr tmp) alist;
+ output ">";
+ buffer_pcdata tmp text;
+ output "</";
+ output tag;
+ output' '>';
+ if newl then output' '\n';
+ | Element (tag, alist, l) ->
+ output tab;
+ output' '<';
+ output tag;
+ List.iter (buffer_attr tmp) alist;
+ output ">\n";
+ List.iter (loop ~newl:true (tab^" ")) l;
+ output tab;
+ output "</";
+ output tag;
+ output' '>';
+ if newl then output' '\n';
+ | PCData text ->
+ buffer_pcdata tmp text;
+ if newl then output' '\n';
+ in
+ loop "" x;
+ Buffer.contents tmp
+
+let print t xml =
+ let tmp, flush = match t with
+ | TChannel oc ->
+ let b = Buffer.create 200 in
+ b, (fun () -> Buffer.output_buffer oc b; flush oc)
+ | TBuffer b ->
+ b, (fun () -> ())
+ in
+ to_buffer tmp xml;
+ flush ()
diff --git a/ide/xml_printer.mli b/ide/xml_printer.mli
new file mode 100644
index 000000000..f24f51fff
--- /dev/null
+++ b/ide/xml_printer.mli
@@ -0,0 +1,29 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type xml = Xml_datatype.xml
+
+type t
+type target = TChannel of out_channel | TBuffer of Buffer.t
+
+val make : target -> t
+
+(** Print the xml data structure to a source into a compact xml string (without
+ any user-readable formating ). *)
+val print : t -> xml -> unit
+
+(** Print the xml data structure into a compact xml string (without
+ any user-readable formating ). *)
+val to_string : xml -> string
+
+(** Print the xml data structure into an user-readable string with
+ tabs and lines break between different nodes. *)
+val to_string_fmt : xml -> string
+
+(** Print PCDATA as a string by escaping XML entities. *)
+val pcdata_to_string : string -> string
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 232630e5b..a55d19aa1 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -39,7 +39,7 @@ let to_search_cst = do_match "search_cst" (fun s args -> match s with
| "subtype_pattern" -> SubType_Pattern (to_string (singleton args))
| "in_module" -> In_Module (to_list to_string (singleton args))
| "include_blacklist" -> Include_Blacklist
- | _ -> raise Marshal_error)
+ | x -> raise (Marshal_error("search",PCData x)))
let of_coq_object f ans =
let prefix = of_list of_string ans.coq_object_prefix in
@@ -56,7 +56,7 @@ let to_coq_object f = function
coq_object_qualid = qualid;
coq_object_object = obj;
}
-| _ -> raise Marshal_error
+| x -> raise (Marshal_error("coq_object",x))
let of_option_value = function
| IntValue i -> constructor "option_value" "intvalue" [of_option of_int i]
@@ -68,7 +68,7 @@ let to_option_value = do_match "option_value" (fun s args -> match s with
| "boolvalue" -> BoolValue (to_bool (singleton args))
| "stringvalue" -> StringValue (to_string (singleton args))
| "stringoptvalue" -> StringOptValue (to_option to_string (singleton args))
- | _ -> raise Marshal_error)
+ | x -> raise (Marshal_error("*value",PCData x)))
let of_option_state s =
Element ("option_state", [], [
@@ -82,8 +82,20 @@ let to_option_state = function
opt_depr = to_bool depr;
opt_name = to_string name;
opt_value = to_option_value value }
- | _ -> raise Marshal_error
+ | x -> raise (Marshal_error("option_state",x))
+let to_stateid = function
+ | Element ("state_id",["val",i],[]) ->
+ let id = int_of_string i in
+ Stateid.of_int id
+ | _ -> raise (Invalid_argument "to_state_id")
+
+let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[])
+
+let of_richpp x = Element ("richpp", [], [Richpp.repr x])
+let to_richpp xml = match xml with
+ | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x
+ | x -> raise Serialize.(Marshal_error("richpp",x))
let of_value f = function
| Good x -> Element ("value", ["val", "good"], [f x])
@@ -91,8 +103,9 @@ let of_value f = function
let loc = match loc with
| None -> []
| Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
- let id = Stateid.to_xml id in
- Element ("value", ["val", "fail"] @ loc, [id; Richpp.of_richpp msg])
+ let id = of_stateid id in
+ Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg])
+
let to_value f = function
| Element ("value", attrs, l) ->
let ans = massoc "val" attrs in
@@ -103,14 +116,14 @@ let to_value f = function
let loc_s = int_of_string (Serialize.massoc "loc_s" attrs) in
let loc_e = int_of_string (Serialize.massoc "loc_e" attrs) in
Some (loc_s, loc_e)
- with Marshal_error | Failure _ -> None
+ with Marshal_error _ | Failure _ -> None
in
- let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise Marshal_error in
- let id = Stateid.of_xml id in
- let msg = Richpp.to_richpp msg in
+ let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in
+ let id = to_stateid id in
+ let msg = to_richpp msg in
Fail (id, loc, msg)
- else raise Marshal_error
-| _ -> raise Marshal_error
+ else raise (Marshal_error("good or fail",PCData ans))
+| x -> raise (Marshal_error("value",x))
let of_status s =
let of_so = of_option of_string in
@@ -126,25 +139,25 @@ let to_status = function
status_proofname = to_option to_string name;
status_allproofs = to_list to_string prfs;
status_proofnum = to_int pnum; }
- | _ -> raise Marshal_error
+ | x -> raise (Marshal_error("status",x))
let of_evar s = Element ("evar", [], [PCData s.evar_info])
let to_evar = function
| Element ("evar", [], data) -> { evar_info = raw_string data; }
- | _ -> raise Marshal_error
+ | x -> raise (Marshal_error("evar",x))
let of_goal g =
- let hyp = of_list Richpp.of_richpp g.goal_hyp in
- let ccl = Richpp.of_richpp g.goal_ccl in
+ let hyp = of_list of_richpp g.goal_hyp in
+ let ccl = of_richpp g.goal_ccl in
let id = of_string g.goal_id in
Element ("goal", [], [id; hyp; ccl])
let to_goal = function
| Element ("goal", [], [id; hyp; ccl]) ->
- let hyp = to_list Richpp.to_richpp hyp in
- let ccl = Richpp.to_richpp ccl in
+ let hyp = to_list to_richpp hyp in
+ let ccl = to_richpp ccl in
let id = to_string id in
{ goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
- | _ -> raise Marshal_error
+ | x -> raise (Marshal_error("goal",x))
let of_goals g =
let of_glist = of_list of_goal in
@@ -162,7 +175,7 @@ let to_goals = function
let given_up = to_list to_goal given_up in
{ fg_goals = fg; bg_goals = bg; shelved_goals = shelf;
given_up_goals = given_up }
- | _ -> raise Marshal_error
+ | x -> raise (Marshal_error("goals",x))
let of_coq_info info =
let version = of_string info.coqtop_version in
@@ -176,7 +189,7 @@ let to_coq_info = function
protocol_version = to_string protocol;
release_date = to_string release;
compile_date = to_string compile; }
- | _ -> raise Marshal_error
+ | x -> raise (Marshal_error("coq_info",x))
end
include Xml_marshalling
@@ -286,7 +299,7 @@ end = struct
| Coq_object t -> (of_coq_object (convert t))
| Pair (t1,t2) -> (of_pair (convert t1) (convert t2))
| Union (t1,t2) -> (of_union (convert t1) (convert t2))
- | State_id -> Stateid.to_xml
+ | State_id -> of_stateid
| Search_cst -> of_search_cst
in
convert ty
@@ -309,7 +322,7 @@ end = struct
| Coq_object t -> (to_coq_object (convert t))
| Pair (t1,t2) -> (to_pair (convert t1) (convert t2))
| Union (t1,t2) -> (to_union (convert t1) (convert t2))
- | State_id -> Stateid.of_xml
+ | State_id -> to_stateid
| Search_cst -> to_search_cst
in
convert ty
@@ -422,7 +435,7 @@ end = struct
(pr_xml (of_bool true)) (pr_xml (of_bool false));
Printf.printf "%s:\n\n%s\n\n" (print_val_t String) (pr_xml (of_string "hello"));
Printf.printf "%s:\n\n%s\n\n" (print_val_t Int) (pr_xml (of_int 256));
- Printf.printf "%s:\n\n%s\n\n" (print_val_t State_id) (pr_xml (Stateid.to_xml Stateid.initial));
+ Printf.printf "%s:\n\n%s\n\n" (print_val_t State_id) (pr_xml (of_stateid Stateid.initial));
Printf.printf "%s:\n\n%s\n\n" (print_val_t (List Int)) (pr_xml (of_list of_int [3;4;5]));
Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t (Option Int))
(pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None));
@@ -682,7 +695,7 @@ let to_call : xml -> unknown_call =
| "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a))
| "PrintAst" -> Unknown (PrintAst (mkCallArg print_ast_sty_t a))
| "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a))
- | _ -> raise Marshal_error)
+ | x -> raise (Marshal_error("call",PCData x)))
(** Debug printing *)
@@ -750,4 +763,130 @@ let document to_string_fmt =
(Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message"))));
document_type_encoding to_string_fmt
+(* Moved from feedback.mli : This is IDE specific and we don't want to
+ pollute the core with it *)
+
+open Feedback
+
+let of_message_level = function
+ | Debug s ->
+ Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
+ | Info -> Serialize.constructor "message_level" "info" []
+ | Notice -> Serialize.constructor "message_level" "notice" []
+ | Warning -> Serialize.constructor "message_level" "warning" []
+ | Error -> Serialize.constructor "message_level" "error" []
+let to_message_level =
+ Serialize.do_match "message_level" (fun s args -> match s with
+ | "debug" -> Debug (Serialize.raw_string args)
+ | "info" -> Info
+ | "notice" -> Notice
+ | "warning" -> Warning
+ | "error" -> Error
+ | x -> raise Serialize.(Marshal_error("error level",PCData x)))
+
+let of_message lvl msg =
+ let lvl = of_message_level lvl in
+ let content = of_richpp msg in
+ Xml_datatype.Element ("message", [], [lvl; content])
+let to_message xml = match xml with
+ | Xml_datatype.Element ("message", [], [lvl; content]) ->
+ Message(to_message_level lvl, to_richpp content)
+ | x -> raise (Marshal_error("message",x))
+
+let is_message = function
+ | Xml_datatype.Element ("message", [], [lvl; content]) ->
+ Some (to_message_level lvl, to_richpp content)
+ | _ -> None
+
+let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
+ | "addedaxiom", _ -> AddedAxiom
+ | "processed", _ -> Processed
+ | "processingin", [where] -> ProcessingIn (to_string where)
+ | "incomplete", _ -> Incomplete
+ | "complete", _ -> Complete
+ | "globref", [loc; filepath; modpath; ident; ty] ->
+ GlobRef(to_loc loc, to_string filepath,
+ to_string modpath, to_string ident, to_string ty)
+ | "globdef", [loc; ident; secpath; ty] ->
+ GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
+ | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s)
+ | "inprogress", [n] -> InProgress (to_int n)
+ | "workerstatus", [ns] ->
+ let n, s = to_pair to_string to_string ns in
+ WorkerStatus(n,s)
+ | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
+ | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
+ | "filedependency", [from; dep] ->
+ FileDependency (to_option to_string from, to_string dep)
+ | "fileloaded", [dirpath; filename] ->
+ FileLoaded (to_string dirpath, to_string filename)
+ | "message", [x] -> to_message x
+ | x,l -> raise (Marshal_error("feedback_content",PCData (x ^ " with attributes " ^ string_of_int (List.length l)))))
+
+let of_feedback_content = function
+ | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
+ | Processed -> constructor "feedback_content" "processed" []
+ | ProcessingIn where ->
+ constructor "feedback_content" "processingin" [of_string where]
+ | Incomplete -> constructor "feedback_content" "incomplete" []
+ | Complete -> constructor "feedback_content" "complete" []
+ | GlobRef(loc, filepath, modpath, ident, ty) ->
+ constructor "feedback_content" "globref" [
+ of_loc loc;
+ of_string filepath;
+ of_string modpath;
+ of_string ident;
+ of_string ty ]
+ | GlobDef(loc, ident, secpath, ty) ->
+ constructor "feedback_content" "globdef" [
+ of_loc loc;
+ of_string ident;
+ of_string secpath;
+ of_string ty ]
+ | ErrorMsg(loc, s) ->
+ constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
+ | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
+ | WorkerStatus(n,s) ->
+ constructor "feedback_content" "workerstatus"
+ [of_pair of_string of_string (n,s)]
+ | Goals (loc,s) ->
+ constructor "feedback_content" "goals" [of_loc loc;of_string s]
+ | Custom (loc, name, x) ->
+ constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
+ | FileDependency (from, depends_on) ->
+ constructor "feedback_content" "filedependency" [
+ of_option of_string from;
+ of_string depends_on]
+ | FileLoaded (dirpath, filename) ->
+ constructor "feedback_content" "fileloaded" [
+ of_string dirpath;
+ of_string filename ]
+ | Message (l,m) -> constructor "feedback_content" "message" [ of_message l m ]
+
+let of_edit_or_state_id = function
+ | Edit id -> ["object","edit"], of_edit_id id
+ | State id -> ["object","state"], of_stateid id
+
+let of_feedback msg =
+ let content = of_feedback_content msg.contents in
+ let obj, id = of_edit_or_state_id msg.id in
+ let route = string_of_int msg.route in
+ Element ("feedback", obj @ ["route",route], [id;content])
+
+let to_feedback xml = match xml with
+ | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
+ id = Edit(to_edit_id id);
+ route = int_of_string route;
+ contents = to_feedback_content content }
+ | Element ("feedback", ["object","state";"route",route], [id;content]) -> {
+ id = State(to_stateid id);
+ route = int_of_string route;
+ contents = to_feedback_content content }
+ | x -> raise (Marshal_error("feedback",x))
+
+let is_feedback = function
+ | Element ("feedback", _, _) -> true
+ | _ -> false
+
(* vim: set foldmethod=marker: *)
+
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 265a50c47..6bca8772e 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -56,3 +56,17 @@ val document : (xml -> string) -> unit
val pr_call : 'a call -> string
val pr_value : 'a value -> string
val pr_full_value : 'a call -> 'a value -> string
+
+(** * Serialization of rich documents *)
+val of_richpp : Richpp.richpp -> Xml_datatype.xml
+val to_richpp : Xml_datatype.xml -> Richpp.richpp
+
+(** * Serializaiton of feedback *)
+val of_feedback : Feedback.feedback -> xml
+val to_feedback : xml -> Feedback.feedback
+val is_feedback : xml -> bool
+
+val is_message : xml -> (Feedback.level * Richpp.richpp) option
+val of_message : Feedback.level -> Richpp.richpp -> xml
+(* val to_message : xml -> Feedback.message *)
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 11:52:01 +0000