diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coqOps.ml | 33 | ||||
-rw-r--r-- | ide/coq_commands.ml | 3 | ||||
-rw-r--r-- | ide/coqide.ml | 50 | ||||
-rw-r--r-- | ide/ide.mllib | 2 | ||||
-rw-r--r-- | ide/ide_slave.ml | 8 | ||||
-rw-r--r-- | ide/project_file.ml4 | 202 | ||||
-rw-r--r-- | ide/texmacspp.ml | 769 | ||||
-rw-r--r-- | ide/texmacspp.mli | 12 | ||||
-rw-r--r-- | ide/xmlprotocol.ml | 4 |
9 files changed, 836 insertions, 247 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index b180aa556..d30d7ab5e 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -14,7 +14,7 @@ open Feedback let b2c = byte_offset_to_char_offset -type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string | `WARNING of Loc.t * string ] +type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string Loc.located | `WARNING of string Loc.located ] type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ] let mem_flag_of_flag : flag -> mem_flag = function | `ERROR _ -> `ERROR @@ -462,20 +462,18 @@ object(self) self#attach_tooltip ~loc sentence (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> - let uloc = Option.default Loc.ghost loc in log_pp ?id Pp.(str "ErrorMsg" ++ msg); remove_flag sentence `PROCESSING; - let rmsg = Pp.string_of_ppcmds msg in - add_flag sentence (`ERROR (uloc, rmsg)); + let rmsg = Pp.string_of_ppcmds msg in + add_flag sentence (`ERROR (loc, rmsg)); self#mark_as_needed sentence; - self#attach_tooltip sentence ?loc rmsg; + self#attach_tooltip ?loc sentence rmsg; self#position_tag_at_sentence ?loc Tags.Script.error sentence | Message(Warning, loc, msg), Some (id,sentence) -> - let uloc = Option.default Loc.ghost loc in log_pp ?id Pp.(str "WarningMsg" ++ msg); let rmsg = Pp.string_of_ppcmds msg in - add_flag sentence (`WARNING (uloc, rmsg)); - self#attach_tooltip sentence ?loc rmsg; + add_flag sentence (`WARNING (loc, rmsg)); + self#attach_tooltip ?loc sentence rmsg; self#position_tag_at_sentence ?loc Tags.Script.warning sentence; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> @@ -525,14 +523,14 @@ object(self) let start, stop, phrase = self#get_sentence sentence in self#position_tag_at_iter ?loc start stop tag phrase - method private process_interp_error queue sentence loc msg tip id = + method private process_interp_error ?loc queue sentence msg tip id = Coq.bind (Coq.return ()) (function () -> let start, stop, phrase = self#get_sentence sentence in buffer#remove_tag Tags.Script.to_process ~start ~stop; self#discard_command_queue queue; pop_info (); if Stateid.equal id tip || Stateid.equal id Stateid.dummy then begin - self#position_tag_at_iter ~loc start stop Tags.Script.error phrase; + self#position_tag_at_iter ?loc start stop Tags.Script.error phrase; buffer#place_cursor ~where:stop; messages#clear; messages#push Feedback.Error msg; @@ -646,9 +644,9 @@ object(self) if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) | Fail (id, loc, msg) -> - let loc = Option.cata Loc.make_loc Loc.ghost loc in + let loc = Option.map Loc.make_loc loc in let sentence = Doc.pop document in - self#process_interp_error queue sentence loc msg tip id in + self#process_interp_error ?loc queue sentence msg tip id in Coq.bind coq_query handle_answer in let tip = @@ -678,14 +676,13 @@ object(self) let extract_error s = match List.find (function `ERROR _ -> true | _ -> false) s.flags with | `ERROR (loc, msg) -> - let iter = - if Loc.is_ghost loc then - buffer#get_iter_at_mark s.start - else + let iter = begin match loc with + | None -> buffer#get_iter_at_mark s.start + | Some loc -> let (iter, _, phrase) = self#get_sentence s in let (start, _) = Loc.unloc loc in - iter#forward_chars (b2c phrase start) in - iter#line + 1, msg + iter#forward_chars (b2c phrase start) + end in iter#line + 1, msg | _ -> assert false in List.rev (Doc.fold_all document [] (fun acc _ _ s -> diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index d55e7f9dd..5912bec35 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -105,8 +105,7 @@ let commands = [ "Reset Extraction Inline"; "Restore State"; ]; - [ "Save."; - "Scheme"; + [ "Scheme"; "Section"; "Set Extraction AutoInline"; "Set Extraction Optimize"; diff --git a/ide/coqide.ml b/ide/coqide.ml index 0b7567a5a..a1e78ee3c 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -46,7 +46,7 @@ open Session (** The arguments that will be passed to coqtop. No quoting here, since no /bin/sh when using create_process instead of open_process. *) -let custom_project_files = ref [] +let custom_project_file = ref None let sup_args = ref [] let logfile = ref None @@ -81,17 +81,27 @@ let pr_exit_status = function | Unix.WEXITED 0 -> " succeeded" | _ -> " failed" -let make_coqtop_args = function - |None -> "", !sup_args - |Some the_file -> - let get_args f = Project_file.args_from_project f - !custom_project_files project_file_name#get - in - match read_project#get with - |Ignore_args -> "", !sup_args - |Append_args -> - let fname, args = get_args the_file in fname, args @ !sup_args - |Subst_args -> get_args the_file +let make_coqtop_args fname = + let open CoqProject_file in + let base_args = match read_project#get with + | Ignore_args -> !sup_args + | Append_args -> !sup_args + | Subst_args -> [] in + if read_project#get = Ignore_args then "", base_args + else + match !custom_project_file, fname with + | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args + | None, None -> "", base_args + | None, Some the_file -> + match + CoqProject_file.find_project_file + ~from:(Filename.dirname the_file) + ~projfile_name:project_file_name#get + with + | None -> "", base_args + | Some proj -> + proj, coqtop_args_from_project (read_project_file proj) @ base_args +;; (** Setting drag & drop on widgets *) @@ -1103,8 +1113,8 @@ let build_ui () = menu templates_menu [ item "Templates" ~label:"Te_mplates"; - template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "J"); - template_item ("Theorem new_theorem : .\nProof.\n\nSave.\n", 8,11, "T"); + template_item ("Lemma new_lemma : .\nProof.\n\nQed.\n", 6,9, "J"); + template_item ("Theorem new_theorem : .\nProof.\n\nQed.\n", 8,11, "T"); template_item ("Definition ident := .\n", 11,5, "E"); template_item ("Inductive ident : :=\n | : .\n", 10,5, "I"); template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F"); @@ -1345,9 +1355,11 @@ let read_coqide_args argv = if coqtop = None then filter_coqtop (Some prog) project_files out args else (output_string stderr "Error: multiple -coqtop options"; exit 1) |"-f" :: file :: args -> + if project_files <> None then + (output_string stderr "Error: multiple -f options"; exit 1); let d = CUnix.canonical_path_name (Filename.dirname file) in - let p = Project_file.read_project_file file in - filter_coqtop coqtop ((d,p) :: project_files) out args + let p = CoqProject_file.read_project_file file in + filter_coqtop coqtop (Some (d,p)) out args |"-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 |"-coqtop" :: [] -> @@ -1364,11 +1376,11 @@ let read_coqide_args argv = (* argument added by MacOS during .app launch *) filter_coqtop coqtop project_files out args |arg::args -> filter_coqtop coqtop project_files (arg::out) args - |[] -> (coqtop,List.rev project_files,List.rev out) + |[] -> (coqtop,project_files,List.rev out) in - let coqtop,project_files,argv = filter_coqtop None [] [] argv in + let coqtop,project_files,argv = filter_coqtop None None [] argv in Ideutils.custom_coqtop := coqtop; - custom_project_files := project_files; + custom_project_file := project_files; argv diff --git a/ide/ide.mllib b/ide/ide.mllib index 78b4c01e8..57e9fe5ad 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -9,6 +9,8 @@ Config_lexer Utf8_convert Preferences Project_file +Serialize +Richprinter Xml_lexer Xml_parser Xml_printer diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index aeff19afe..4e613f163 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -65,8 +65,8 @@ let is_known_option cmd = match cmd with (** Check whether a command is forbidden in the IDE *) let ide_cmd_checks ~id (loc,ast) = - let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in - let warn msg = Feedback.(feedback ~id (Message (Warning, Some loc, strbrk msg))) in + let user_error s = CErrors.user_err ?loc ~hdr:"CoqIde" (str s) in + let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in if is_debug ast then user_error "Debug mode not available in the IDE"; if is_known_option ast then @@ -343,8 +343,8 @@ let about () = { let handle_exn (e, info) = let dummy = Stateid.dummy in let loc_of e = match Loc.get_loc e with - | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) - | _ -> None in + | Some loc -> Some (Loc.unloc loc) + | _ -> None in let mk_msg () = CErrors.print ~info e in match e with | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!" diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 deleted file mode 100644 index de0720e03..000000000 --- a/ide/project_file.ml4 +++ /dev/null @@ -1,202 +0,0 @@ -type target = - | ML of string (* ML file : foo.ml -> (ML "foo.ml") *) - | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) - | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) - | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) - | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Arg of string - | Special of string * string * bool * string - (* file, dependencies, is_phony, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | MLInclude of string (* -I physicalpath *) - | Include of string * string (* -Q physicalpath logicalpath *) - | RInclude of string * string (* -R physicalpath logicalpath *) - -type install = - | NoInstall - | TraditionalInstall - | UserInstall - | UnspecInstall - -exception Parsing_error -let rec parse_string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string s) - | [< >] -> "" -and parse_string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) - | [< >] -> raise Parsing_error -and parse_skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> parse_skip_comment s - | [< >] -> [< >] -and parse_args = parser - | [< '' ' | '\n' | '\t'; s >] -> parse_args s - | [< ''#'; s >] -> parse_args (parse_skip_comment s) - | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s - | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s) - | [< >] -> [] - - -let parse f = - let c = open_in f in - let res = parse_args (Stream.of_channel c) in - close_in c; - res - -let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function - | [] -> opts, l - | ("-h"|"--help") :: _ -> - raise Parsing_error - | ("-no-opt"|"-byte") :: r -> - process_cmd_line orig_dir (project_file,makefile,install,false) l r - | ("-full"|"-opt") :: r -> - process_cmd_line orig_dir (project_file,makefile,install,true) l r - | "-impredicative-set" :: r -> - Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform."); - process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r - | "-no-install" :: r -> - Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead"))); - process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r - | "-install" :: d :: r -> - if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once."); - let install = - match d with - | "user" -> UserInstall - | "none" -> NoInstall - | "global" -> TraditionalInstall - | _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install."))); - install - in - process_cmd_line orig_dir (project_file,makefile,install,opt) l r - | "-custom" :: com :: dependencies :: file :: r -> - Feedback.msg_warning (Pp.app - (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".") - (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.") - ); - process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r - | "-extra" :: file :: dependencies :: com :: r -> - process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r - | "-extra-phony" :: target :: dependencies :: com :: r -> - process_cmd_line orig_dir opts (Special (target,dependencies,true,com) :: l) r - | "-Q" :: d :: lp :: r -> - process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r - | "-I" :: d :: r -> - process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r - | "-R" :: p :: lp :: r -> - process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r - | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ -> - raise Parsing_error - | "-f" :: file :: r -> - let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in - let () = match project_file with - | None -> () - | Some _ -> Feedback.msg_warning (Pp.str - "Several features will not work with multiple project files.") - in - let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in - process_cmd_line orig_dir opts' l' r - | ["-f"] -> - raise Parsing_error - | "-o" :: file :: r -> - begin try - let _ = String.index file '/' in - raise Parsing_error - with Not_found -> - let () = match makefile with - |None -> () - |Some f -> - Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be."))) - in process_cmd_line orig_dir (project_file,Some file,install,opt) l r - end - | v :: "=" :: def :: r -> - process_cmd_line orig_dir opts (Def (v,def) :: l) r - | "-arg" :: a :: r -> - process_cmd_line orig_dir opts (Arg a :: l) r - | f :: r -> - let f = CUnix.correct_path f orig_dir in - process_cmd_line orig_dir opts (( - if Filename.check_suffix f ".v" then V f - else if (Filename.check_suffix f ".ml") then ML f - else if (Filename.check_suffix f ".ml4") then ML4 f - else if (Filename.check_suffix f ".mli") then MLI f - else if (Filename.check_suffix f ".mllib") then MLLIB f - else if (Filename.check_suffix f ".mlpack") then MLPACK f - else Subdir f) :: l) r - -let process_cmd_line orig_dir opts l args = - let (opts, l) = process_cmd_line orig_dir opts l args in - opts, List.rev l - -let rec post_canonize f = - if Filename.basename f = Filename.current_dir_name - then let dir = Filename.dirname f in - if dir = Filename.current_dir_name then f else post_canonize dir - else f - -(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *) -let split_arguments args = - List.fold_right - (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t), - (ml_inc,q_inc,r_inc as i),(args,defs as d)) -> - match a with - | V n -> - ((CUnix.remove_path_dot n::v,m,o,s),i,d) - | ML n -> - ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d) - | MLI n -> - ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d) - | ML4 n -> - ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d) - | MLLIB n -> - ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d) - | MLPACK n -> - ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d) - | Special (n,dep,is_phony,c) -> - ((v,m,(n,dep,is_phony,c)::o,s),i,d) - | Subdir n -> - ((v,m,o,n::s),i,d) - | MLInclude p -> - let ml_new = (CUnix.remove_path_dot (post_canonize p), - CUnix.canonical_path_name p) in - (t,(ml_new::ml_inc,q_inc,r_inc),d) - | Include (p,l) -> - let q_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml_inc,q_new::q_inc,r_inc),d) - | RInclude (p,l) -> - let r_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml_inc,q_inc,r_new::r_inc),d) - | Def (v,def) -> - (t,i,(args,(v,def)::defs)) - | Arg a -> - (t,i,(a::args,defs))) - args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[])) - -let read_project_file f = - split_arguments - (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f))) - -let args_from_project file project_files default_name = - let build_cmd_line ml_inc i_inc r_inc args = - List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc - (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc - (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc - (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args []))) - in try - let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in - fname, build_cmd_line ml_inc i_inc r_inc args - with Failure _ -> - let rec find_project_file dir = try - let fname = Filename.concat dir default_name in - let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) = - read_project_file fname in - fname, build_cmd_line ml_inc i_inc r_inc args - with Sys_error s -> - let newdir = Filename.dirname dir in - if dir = newdir then "",[] else find_project_file newdir - in find_project_file (Filename.dirname file) diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml new file mode 100644 index 000000000..ddb62313f --- /dev/null +++ b/ide/texmacspp.ml @@ -0,0 +1,769 @@ +(************************************************************************) +(* 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 +open Constrexpr_ops + +let unlock ?loc = + let start, stop = Option.cata Loc.unloc (0,0) 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 ?loc typ name xml = + xmlWithLoc ?loc "theorem" ["type", typ; "name", name] xml + +let xmlDef ?loc typ name xml = + xmlWithLoc ?loc "definition" ["type", typ; "name", name] xml + +let xmlNotation ?loc attr name xml = + xmlWithLoc ?loc "notation" (("name", name) :: attr) xml + +let xmlReservedNotation ?loc attr name = + xmlWithLoc ?loc "reservednotation" (("name", name) :: attr) [] + +let xmlCst ?loc ?(attr=[]) name = + xmlWithLoc ?loc "constant" (("name", name) :: attr) [] + +let xmlOperator ?loc ?(attr=[]) ?(pprules=[]) name = + 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 ?loc kind 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 ?loc kind xml = xmlWithLoc ?loc "assumption" ["kind",kind] xml + +let xmlComment ?loc xml = xmlWithLoc ?loc "comment" [] xml + +let xmlCanonicalStructure ?loc attr = xmlWithLoc ?loc "canonicalstructure" attr [] + +let xmlQed ?loc ?(attr=[]) = xmlWithLoc ?loc "qed" attr [] + +let xmlPatvar ?loc id = xmlWithLoc ?loc "patvar" ["id", id] [] + +let xmlReference ref = + let name = Libnames.string_of_reference ref in + let i, j = Option.cata Loc.unloc (0,0) (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 ?(attr=[]) action 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 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] + | SetOnlyPrinting -> ["onlyprinting", ""] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion 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 ?loc (string_of_name name)) loc_names) in + match e.CAst.v 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 + | CLocalDef ((loc, nam), ce, ty) -> + let attrs = ["name", string_of_name nam] in + let value = match ty with + Some t -> CAst.make ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t) + | None -> ce in + pp_expr ~attr:attrs value + | CLocalAssum (namll, _, ce) -> + let ppl = + List.map (fun (loc, nam) -> (xmlCst ?loc (string_of_name nam))) namll in + xmlTyped (ppl @ [pp_expr ce]) + | CLocalPattern _ -> + assert false +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 = Option.cata Loc.unloc (0,0) 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 ?loc (Id.to_string id) +and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce] +and pp_cases_pattern_expr {loc ; CAst.v = cpe} = + match cpe with + | CPatAlias (cpe, id) -> + xmlApply ?loc + (xmlOperator ?loc ~attr:["name", string_of_id id] "alias" :: + [pp_cases_pattern_expr cpe]) + | CPatCstr (ref, None, cpel2) -> + xmlApply ?loc + (xmlOperator ?loc "reference" + ~attr:["name", Libnames.string_of_reference ref] :: + [Element ("impargs", [], []); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatCstr (ref, Some cpel1, cpel2) -> + xmlApply ?loc + (xmlOperator ?loc "reference" + ~attr:["name", Libnames.string_of_reference ref] :: + [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1)); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatAtom optr -> + let attrs = match optr with + | None -> [] + | Some r -> ["name", Libnames.string_of_reference r] in + xmlApply ?loc (xmlOperator ?loc "atom" ~attr:attrs :: []) + | CPatOr cpel -> + xmlApply ?loc (xmlOperator ?loc "or" :: List.map pp_cases_pattern_expr cpel) + | CPatNotation (n, (subst_constr, subst_rec), cpel) -> + xmlApply ?loc + (xmlOperator ?loc "notation" :: + [xmlOperator ?loc n; + 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 tok -> pp_token ?loc tok + | CPatRecord rcl -> + xmlApply ?loc + (xmlOperator ?loc "record" :: + List.map (fun (r, cpe) -> + Element ("field", + ["reference", Libnames.string_of_reference r], + [pp_cases_pattern_expr cpe])) + rcl) + | CPatDelimiters (delim, cpe) -> + xmlApply ?loc + (xmlOperator ?loc "delimiter" ~attr:["name", delim] :: + [pp_cases_pattern_expr cpe]) + | CPatCast _ -> assert false +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=[]) { loc; CAst.v = e } = + match e with + | CRef (r, _) -> + xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r) + | CProdN (bl, e) -> + xmlApply ?loc + (xmlOperator ?loc "forall" :: [pp_bindlist bl] @ [pp_expr e]) + | CApp ((_, hd), args) -> + xmlApply ?loc ~attr (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args) + | CAppExpl ((_, r, _), args) -> + xmlApply ?loc ~attr + (xmlCst ?loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r) + :: List.map pp_expr args) + | CNotation (notation, ([],[],[])) -> + xmlOperator ?loc notation + | CNotation (notation, (args, cell, lbll)) -> + let fmts = Notation.find_notation_extra_printing_rules notation in + let oper = xmlOperator ?loc notation ~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(s) -> + xmlOperator ?loc (string_of_glob_sort s) + | CDelimiters (scope, ce) -> + xmlApply ?loc (xmlOperator ?loc "delimiter" ~attr:["name", scope] :: + [pp_expr ce]) + | CPrim tok -> pp_token ?loc tok + | CGeneralization (kind, _, e) -> + let kind= match kind with + | Explicit -> "explicit" + | Implicit -> "implicit" in + xmlApply ?loc + (xmlOperator ?loc ~attr:["kind", kind] "generalization" :: [pp_expr e]) + | CCast (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 (ek, cel) -> + let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in + xmlApply ?loc + (xmlOperator ?loc "evar" ~attr:["id", string_of_id ek] :: + ppcel) + | CPatVar id -> xmlPatvar ?loc (string_of_id id) + | CHole (_, _, _) -> xmlCst ?loc ~attr "_" + | CIf (test, (_, ret), th, el) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc "if" :: + return @ [pp_expr th] @ [pp_expr el]) + | CLetTuple (names, (_, ret), value, body) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc "lettuple" :: + return @ + (List.map (fun (loc, var) -> xmlCst ?loc (string_of_name var)) names) @ + [pp_expr value; pp_expr body]) + | CCases (sty, ret, cel, bel) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc ~attr:["style", (string_of_case_style sty)] "match" :: + (return @ + [Element ("scrutinees", [], List.map pp_case_expr cel)] @ + [pp_branch_expr_list bel])) + | CRecord _ -> assert false + | CLetIn ((varloc, var), value, typ, body) -> + let value = match typ with + | Some t -> + CAst.make ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t)) + | None -> value in + xmlApply ?loc + (xmlOperator ?loc "let" :: + [xmlCst ?loc:varloc (string_of_name var) ; pp_expr value; pp_expr body]) + | CLambdaN (bl, e) -> + xmlApply ?loc + (xmlOperator ?loc "lambda" :: [pp_bindlist bl] @ [pp_expr e]) + | CCoFix (_, _) -> assert false + | CFix (lid, fel) -> + xmlApply ?loc + (xmlOperator ?loc "fix" :: + 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 ?loc v = + 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 ?loc e]) + | VernacRedirect (s, (loc,e)) -> + xmlApply ?loc (Element("redirect",["path", s],[]) :: + [tmpp ?loc e]) + | VernacTimeout (s,e) -> + xmlApply ?loc (Element("timeout",["val",string_of_int s],[]) :: + [tmpp ?loc e]) + | VernacFail e -> xmlApply ?loc (Element("fail",[],[]) :: [tmpp ?loc e]) + + (* Syntax *) + | VernacSyntaxExtension (_, ((_, name), sml)) -> + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + xmlReservedNotation ?loc attrs name + + | 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 ?loc (sc_attr @ attrs) name [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 ?loc (sc_attr @ attrs) name [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 ?loc str_dk str_id [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 ?loc str_tk str_id [pp_expr statement]) + | VernacStartTheoremProof _ as x -> xmlTODO ?loc x + | VernacEndProof pe -> + begin + match pe with + | Admitted -> xmlQed ?loc ?attr:None + | Proved (_, Some ((_, id), Some tk)) -> + let nam = Id.to_string id in + let typ = Kindops.string_of_theorem_kind tk in + xmlQed ?loc ~attr:["name", nam; "type", typ] + | Proved (_, Some ((_, id), None)) -> + let nam = Id.to_string id in + xmlQed ?loc ~attr:["name", nam] + | Proved _ -> xmlQed ?loc ?attr:None + 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 ?loc kind 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 ?loc kind 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 ?loc attr + | 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 ?loc attrs name [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 + | VernacSetAppendOption _ 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 = None (** FIXME *) 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 ?loc e]) + | VernacLocal (b,e) -> + xmlApply ?loc (Element("local",["flag",string_of_bool b],[]) :: + [tmpp ?loc e]) + +let tmpp ?loc v = + match tmpp ?loc v 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..c1086a633 --- /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 : ?loc:Loc.t -> vernac_expr -> xml diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index bf52b0b52..53eb1a95f 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -863,7 +863,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "workerstatus", [ns] -> let n, s = to_pair to_string to_string ns in WorkerStatus(n,s) - | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) + | "custom", [loc;name;x]-> Custom (to_option to_loc loc, to_string name, x) | "filedependency", [from; dep] -> FileDependency (to_option to_string from, to_string dep) | "fileloaded", [dirpath; filename] -> @@ -896,7 +896,7 @@ let of_feedback_content = function constructor "feedback_content" "workerstatus" [of_pair of_string of_string (n,s)] | Custom (loc, name, x) -> - constructor "feedback_content" "custom" [of_loc loc; of_string name; x] + constructor "feedback_content" "custom" [of_option of_loc loc; of_string name; x] | FileDependency (from, depends_on) -> constructor "feedback_content" "filedependency" [ of_option of_string from; |