diff options
Diffstat (limited to 'ide')
68 files changed, 2394 insertions, 325 deletions
diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template index e224e81204..fbe7773dd4 100644 --- a/ide/MacOS/Info.plist.template +++ b/ide/MacOS/Info.plist.template @@ -66,7 +66,7 @@ <key>CFBundleGetInfoString</key> <string>Coq_vVERSION</string> <key>NSHumanReadableCopyright</key> - <string>Copyright 1999-2015, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string> + <string>Copyright 1999-2016, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string> <key>CFBundleHelpBookFolder</key> <string>share/doc/coq/html/</string> <key>CFAppleHelpAnchor</key> diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 3671535680..ac9cc57bc0 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/coq.lang b/ide/coq.lang index e25eedbca9..484264ece3 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -95,11 +95,24 @@ <keyword>Type</keyword> </context> - <context id="coq" class="no-spell-check"> + <!-- Terms --> + <context id="constr"> <include> <context ref="string"/> <context ref="coqdoc"/> <context ref="comment"/> + <context ref="constr-sort"/> + <context ref="constr-keyword"/> + <context id="dot-nosep"> + <match>\.\.</match> + </context> + </include> + </context> + + <context id="coq" class="no-spell-check"> + <include> + <context ref="coqdoc"/> + <context ref="comment"/> <context id="declaration"> <start>\%{decl_head}</start> @@ -110,14 +123,7 @@ <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/> <context sub-pattern="id_list" where="start" style-ref="identifier"/> <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/> - <context ref="constr-keyword"/> - <context ref="constr-sort"/> - <context id="dot-nosep"> - <match>\.\.</match> - </context> - <context ref="string"/> - <context ref="coqdoc"/> - <context ref="comment"/> + <context ref="constr"/> </include> </context> @@ -127,21 +133,19 @@ <include> <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> <context sub-pattern="0" where="end" style-ref="vernac-keyword"/> - <context ref="command-in-proof"/> - <context ref="string"/> <context ref="coqdoc"/> <context ref="comment"/> - <context ref="constr-keyword"/> - <context ref="constr-sort"/> - <context id="bullet" extend-parent="false"> - <match>\%{dot_sep}\s*(?'bul'\%{bullet})</match> + <context id="bullet" style-ref="vernac-keyword" extend-parent="false"> + <match>\%{bullet}</match> + </context> + <context extend-parent="false"> + <start>\%[</start> + <end>\%{dot_sep}</end> <include> - <context sub-pattern="bul" style-ref="vernac-keyword"/> + <context ref="command-in-proof"/> + <context ref="constr"/> </include> </context> - <context id="bullet-sol" style-ref="vernac-keyword"> - <match>^\s*\%{bullet}</match> - </context> </include> </context> @@ -150,11 +154,19 @@ <end>\%{dot_sep}</end> <include> <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> - <context ref="constr-keyword"/> - <context ref="constr-sort"/> + <context ref="constr"/> </include> </context> + <context ref="command"/> + </include> + </context> + + <!-- Toplevel commands --> + <context id="command" extend-parent="false"> + <start>\%[</start> + <end>\%{dot_sep}</end> + <include> <context id="command-in-proof" style-ref="vernac-keyword"> <keyword>About</keyword> <keyword>Check</keyword> @@ -166,7 +178,7 @@ <keyword>Transparent</keyword> </context> - <context id="command" style-ref="vernac-keyword"> + <context id="toplevel-command" style-ref="vernac-keyword"> <keyword>Add</keyword> <keyword>Load</keyword> <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword> @@ -228,7 +240,10 @@ <context sub-pattern="qua_list" style-ref="identifier"/> </include> </context> + + <context ref="constr"/> </include> </context> + </definitions> </language> diff --git a/ide/coq.ml b/ide/coq.ml index 268a95a336..61f002576b 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -290,23 +290,20 @@ let rec check_errors = function | `NVAL :: _ -> raise (TubeError "NVAL") | `OUT :: _ -> raise (TubeError "OUT") -let handle_intermediate_message handle xml = - let message = Pp.to_message xml in - let level = message.Pp.message_level in - let content = message.Pp.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 - | Pp.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s) - | Pp.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s) - | Pp.Notice -> fun s -> Minilib.log ~level:`NOTICE (xml_to_string s) - | Pp.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s) - | Pp.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s) + | Feedback.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s) + | Feedback.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s) + | Feedback.Notice -> fun s -> Minilib.log ~level:`NOTICE (xml_to_string s) + | 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 Pp.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 = @@ -460,10 +462,6 @@ let close_coqtop coqtop = let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop -let break_coqtop coqtop = - try !interrupter (CoqTop.unixpid coqtop.handle.proc) - with _ -> Minilib.log "Error while sending Ctrl-C" - let get_arguments coqtop = coqtop.sup_args let set_arguments coqtop args = @@ -513,6 +511,17 @@ let search flags = eval_call (Xmlprotocol.search flags) let init x = eval_call (Xmlprotocol.init x) let stop_worker x = eval_call (Xmlprotocol.stop_worker x) +let break_coqtop coqtop workers = + if coqtop.status = Busy then + try !interrupter (CoqTop.unixpid coqtop.handle.proc) + with _ -> Minilib.log "Error while sending Ctrl-C" + else + let rec aux = function + | [] -> Void + | w :: ws -> stop_worker w coqtop.handle (fun _ -> aux ws) + in + let Void = aux workers in () + module PrintOpt = struct type t = string list diff --git a/ide/coq.mli b/ide/coq.mli index 2dc5ad3078..7cef6a4d0a 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -70,8 +70,8 @@ val init_coqtop : coqtop -> unit task -> unit (** Finish initializing a freshly spawned coqtop, by running a first task on it. The task should run its inner continuation at the end. *) -val break_coqtop : coqtop -> unit -(** Interrupt the current computation of coqtop. *) +val break_coqtop : coqtop -> string list -> unit +(** Interrupt the current computation of coqtop or the worker if coqtop it not running. *) val close_coqtop : coqtop -> unit (** Close coqtop. Subsequent requests will be discarded. Hook ignored. *) diff --git a/ide/coq.png b/ide/coq.png Binary files differindex cccd5a9a19..136bfdd5fe 100644 --- a/ide/coq.png +++ b/ide/coq.png diff --git a/ide/coqOps.ml b/ide/coqOps.ml index d9b84498b7..9301359957 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -12,7 +12,9 @@ open Ideutils open Interface open Feedback -type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string ] +let b2c = byte_offset_to_char_offset + +type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string ] type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ] let mem_flag_of_flag : flag -> mem_flag = function | `ERROR _ -> `ERROR @@ -44,12 +46,9 @@ module SentenceId : sig val mk_sentence : start:GText.mark -> stop:GText.mark -> flag list -> sentence - val set_flags : sentence -> flag list -> unit val add_flag : sentence -> flag -> unit val has_flag : sentence -> mem_flag -> bool val remove_flag : sentence -> mem_flag -> unit - val same_sentence : sentence -> sentence -> bool - val hidden_edit_id : unit -> int val find_all_tooltips : sentence -> int -> string list val add_tooltip : sentence -> int -> int -> string -> unit val set_index : sentence -> int -> unit @@ -87,18 +86,15 @@ end = struct index = -1; changed_sig = new GUtil.signal (); } - let hidden_edit_id () = decr id; !id let changed s = s.changed_sig#call (s.index, List.map mem_flag_of_flag s.flags) - let set_flags s f = s.flags <- f; changed s let add_flag s f = s.flags <- CList.add_set (=) f s.flags; changed s let has_flag s mf = List.exists (fun f -> mem_flag_of_flag f = mf) s.flags let remove_flag s mf = s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags; changed s - let same_sentence s1 s2 = s1.edit_id = s2.edit_id let find_all_tooltips s off = CList.map_filter (fun (start,stop,t) -> if start <= off && off <= stop then Some t else None) @@ -174,6 +170,55 @@ let validate s = module Doc = Document +let segment_model (doc : sentence Doc.document) : Wg_Segment.model = +object (self) + + val mutable cbs = [] + + val mutable document_length = 0 + + method length = document_length + + method changed ~callback = cbs <- callback :: cbs + + method fold : 'a. ('a -> Wg_Segment.color -> 'a) -> 'a -> 'a = fun f accu -> + let fold accu _ _ s = + let flags = List.map mem_flag_of_flag s.flags in + f accu (flags_to_color flags) + in + Doc.fold_all doc accu fold + + method private on_changed (i, f) = + let data = (i, flags_to_color f) in + List.iter (fun f -> f (`SET data)) cbs + + method private on_push s ctx = + let after = match ctx with + | None -> [] + | Some (l, _) -> l + in + List.iter (fun s -> set_index s (s.index + 1)) after; + set_index s (document_length - List.length after); + ignore ((SentenceId.connect s)#changed self#on_changed); + document_length <- document_length + 1; + List.iter (fun f -> f `INSERT) cbs + + method private on_pop s ctx = + let () = match ctx with + | None -> () + | Some (l, _) -> List.iter (fun s -> set_index s (s.index - 1)) l + in + set_index s (-1); + document_length <- document_length - 1; + List.iter (fun f -> f `REMOVE) cbs + + initializer + let _ = (Doc.connect doc)#pushed self#on_push in + let _ = (Doc.connect doc)#popped self#on_pop in + () + +end + class coqops (_script:Wg_ScriptView.script_view) (_pv:Wg_ProofView.proof_view) @@ -206,20 +251,8 @@ object(self) script#misc#set_has_tooltip true; ignore(script#misc#connect#query_tooltip ~callback:self#tooltip_callback); feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback; - let on_changed (i, f) = segment#add i (flags_to_color f) in - let on_push s = - set_index s document_length; - ignore ((SentenceId.connect s)#changed on_changed); - document_length <- succ document_length; - segment#set_length document_length; - let flags = List.map mem_flag_of_flag s.flags in - segment#add s.index (flags_to_color flags); - in - let on_pop s = - set_index s (-1); - document_length <- pred document_length; - segment#set_length document_length; - in + let md = segment_model document in + segment#set_model md; let on_click id = let find _ _ s = Int.equal s.index id in let sentence = Doc.find document find in @@ -235,8 +268,6 @@ object(self) script#buffer#place_cursor iter; ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter) in - let _ = (Doc.connect document)#pushed on_push in - let _ = (Doc.connect document)#popped on_pop in let _ = segment#connect#clicked on_click in () @@ -367,8 +398,8 @@ object(self) let start_sentence, stop_sentence, phrase = self#get_sentence sentence in let pre_chars, post_chars = if Loc.is_ghost loc then 0, String.length phrase else Loc.unloc loc in - let pre = Ideutils.glib_utf8_pos_to_offset phrase ~off:pre_chars in - let post = Ideutils.glib_utf8_pos_to_offset phrase ~off:post_chars in + let pre = b2c phrase pre_chars in + let post = b2c phrase post_chars in let start = start_sentence#forward_chars pre in let stop = start_sentence#forward_chars post in let markup = Glib.Markup.escape_text text in @@ -432,7 +463,7 @@ object(self) | ErrorMsg(loc, msg), Some (id,sentence) -> log "ErrorMsg" id; remove_flag sentence `PROCESSING; - add_flag sentence (`ERROR msg); + add_flag sentence (`ERROR (loc, msg)); self#mark_as_needed sentence; self#attach_tooltip sentence loc msg; if not (Loc.is_ghost loc) then @@ -471,8 +502,8 @@ object(self) | None -> () | Some (start, stop) -> buffer#apply_tag Tags.Script.error - ~start:(iter#forward_chars (byte_offset_to_char_offset phrase start)) - ~stop:(iter#forward_chars (byte_offset_to_char_offset phrase stop)) + ~start:(iter#forward_chars (b2c phrase start)) + ~stop:(iter#forward_chars (b2c phrase stop)) method private position_error_tag_at_sentence sentence loc = let start, _, phrase = self#get_sentence sentence in @@ -488,7 +519,7 @@ object(self) self#position_error_tag_at_iter start phrase loc; buffer#place_cursor ~where:stop; messages#clear; - messages#push Pp.Error msg; + messages#push Feedback.Error msg; self#show_goals end else self#show_goals_aux ~move_insert:true () @@ -564,7 +595,8 @@ object(self) if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> - logger Pp.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted"); + + logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted"); self#discard_command_queue queue; conclude [] | `Skip(start,stop), (_,s) :: topstack -> @@ -580,7 +612,7 @@ object(self) let handle_answer = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> Doc.assign_tip_id document id; - logger Pp.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Richpp.richpp_of_string msg); self#commit_queue_transaction sentence; loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> @@ -588,7 +620,7 @@ object(self) let topstack, _ = Doc.context document in self#exit_focus; self#cleanup (Doc.cut_at document tip); - logger Pp.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Richpp.richpp_of_string msg); self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) @@ -607,7 +639,7 @@ object(self) let next = function | Good _ -> messages#clear; - messages#push Pp.Info (Richpp.richpp_of_string "All proof terms checked by the kernel"); + messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel"); Coq.return () | Fail x -> self#handle_failure x in Coq.bind (Coq.status ~logger:messages#push true) next @@ -623,7 +655,15 @@ object(self) method get_errors = let extract_error s = match List.find (function `ERROR _ -> true | _ -> false) s.flags with - | `ERROR msg -> (buffer#get_iter_at_mark s.start)#line + 1, msg + | `ERROR (loc, msg) -> + let iter = + if Loc.is_ghost loc then + buffer#get_iter_at_mark s.start + else + 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 | _ -> assert false in List.rev (Doc.fold_all document [] (fun acc _ _ s -> @@ -701,8 +741,8 @@ object(self) self#cleanup (Doc.cut_at document to_id); conclusion () | Fail (safe_id, loc, msg) -> - if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC"); - messages#push Pp.Error msg; + if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); + messages#push Feedback.Error msg; if Stateid.equal safe_id Stateid.dummy then self#show_goals else undo safe_id (Doc.focused document && Doc.is_in_focus document safe_id)) @@ -720,7 +760,7 @@ object(self) ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = messages#clear; - messages#push Pp.Error msg; + messages#push Feedback.Error msg; ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) else @@ -834,7 +874,10 @@ object(self) method initialize = let get_initial_state = let next = function - | Fail _ -> messages#set (Richpp.richpp_of_string "Couln't initialize Coq"); Coq.return () + | Fail (_, _, message) -> + let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in + let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in + ignore (popup#run ()); exit 1 | Good id -> initial_state <- id; Coq.return () in Coq.bind (Coq.init (get_filename ())) next in Coq.seq get_initial_state Coq.PrintOpt.enforce diff --git a/ide/coqOps.mli b/ide/coqOps.mli index 8e76d3b270..4a37a1fa55 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 37e38a5464..d55e7f9dd7 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index e333c0b24c..b6286c49fb 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/coqide.ml b/ide/coqide.ml index 5fdb4a2a41..758a5a4c99 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -570,7 +570,7 @@ module Nav = struct let restart _ = on_current_term restart let interrupt sn = Minilib.log "User break received"; - Coq.break_coqtop sn.coqtop + Coq.break_coqtop sn.coqtop CString.(Set.elements (Map.domain sn.jobpage#data)) let interrupt = cb_on_current_term interrupt let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document) end @@ -783,7 +783,7 @@ let coqtop_arguments sn = let args = String.concat " " args in let msg = Printf.sprintf "Invalid arguments: %s" args in let () = sn.messages#clear in - sn.messages#push Pp.Error (Richpp.richpp_of_string msg) + sn.messages#push Feedback.Error (Richpp.richpp_of_string msg) else dialog#destroy () in let _ = entry#connect#activate ok_cb in diff --git a/ide/coqide.mli b/ide/coqide.mli index 6691512845..744b974ffa 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index db69ec661f..534a3f179d 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib index 92301dc30e..ed1fa465d2 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/document.ml b/ide/document.ml index bb431e7914..62457fe56b 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -16,8 +16,8 @@ type id = Stateid.t class type ['a] signals = object - method popped : callback:('a -> unit) -> unit - method pushed : callback:('a -> unit) -> unit + method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit + method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit end class ['a] signal () = @@ -32,14 +32,14 @@ end type 'a document = { mutable stack : 'a sentence list; mutable context : ('a sentence list * 'a sentence list) option; - pushed_sig : 'a signal; - popped_sig : 'a signal; + pushed_sig : ('a * ('a list * 'a list) option) signal; + popped_sig : ('a * ('a list * 'a list) option) signal; } -let connect d = +let connect d : 'a signals = object - method pushed ~callback = d.pushed_sig#connect callback - method popped ~callback = d.popped_sig#connect callback + method pushed ~callback = d.pushed_sig#connect (fun (x, ctx) -> callback x ctx) + method popped ~callback = d.popped_sig#connect (fun (x, ctx) -> callback x ctx) end let create () = { @@ -49,6 +49,12 @@ let create () = { popped_sig = new signal (); } +let repr_context s = match s.context with +| None -> None +| Some (cl, cr) -> + let map s = s.data in + Some (List.map map cl, List.map map cr) + (* Invariant, only the tip is a allowed to have state_id = None *) let invariant l = l = [] || (List.hd l).state_id <> None @@ -64,12 +70,13 @@ let tip_data = function let push d x = assert(invariant d.stack); d.stack <- { data = x; state_id = None } :: d.stack; - d.pushed_sig#call x + d.pushed_sig#call (x, repr_context d) let pop = function | { stack = [] } -> raise Empty - | { stack = { data }::xs } as s -> s.stack <- xs; s.popped_sig#call data; data - + | { stack = { data }::xs } as s -> + s.stack <- xs; s.popped_sig#call (data, repr_context s); data + let focus d ~cond_top:c_start ~cond_bot:c_stop = assert(invariant d.stack); if d.context <> None then invalid_arg "focus"; diff --git a/ide/document.mli b/ide/document.mli index 0d803ff003..fb96cb6d76 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -108,8 +108,8 @@ val print : class type ['a] signals = object - method popped : callback:('a -> unit) -> unit - method pushed : callback:('a -> unit) -> unit + method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit + method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit end val connect : 'a document -> 'a signals diff --git a/ide/fileOps.ml b/ide/fileOps.ml index eccd61d0d9..7be1bdb927 100644 --- a/ide/fileOps.ml +++ b/ide/fileOps.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/fileOps.mli b/ide/fileOps.mli index 48b7c8f656..9f0b75ac56 100644 --- a/ide/fileOps.mli +++ b/ide/fileOps.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index 79ccf61a43..f905053ddb 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/ide.mllib b/ide/ide.mllib index 83b3142839..b2f32fcf7b 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 d8b8bd4610..9071410e5b 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -98,11 +98,11 @@ let coqide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then - msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + Feedback.msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then - msg_warning (strbrk "Rather use CoqIDE navigation instead"); + Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead"); if is_query ast then - msg_warning (strbrk "Query commands should not be inserted in scripts") + Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts") (** Interpretation (cf. [Ide_intf.interp]) *) @@ -130,7 +130,8 @@ let annotate phrase = (** Goal display *) -let hyp_next_tac sigma env (id,_,ast) = +let hyp_next_tac sigma env decl = + let (id,_,ast) = Context.Named.Declaration.to_tuple decl in let id_s = Names.Id.to_string id in let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in [ @@ -187,8 +188,12 @@ let process_goal sigma g = Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d (env,l) = - let d = Context.NamedList.Declaration.map (Reductionops.nf_evar sigma) d in - let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in + let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in + let d' = List.map (fun name -> let open Context.Named.Declaration in + match pi2 d with + | None -> LocalAssum (name, pi3 d) + | Some value -> LocalDef (name, value, pi3 d)) + (pi1 d) in (List.fold_right Environ.push_named d' env, (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in let (_env, hyps) = @@ -207,7 +212,7 @@ let export_pre_goals pgs = let goals () = Stm.finish (); let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); + if not (String.is_empty s) then Feedback.msg_info (str s); try let pfts = Proof_global.give_me_the_proof () in Some (export_pre_goals (Proof.map_structured_proof pfts process_goal)) @@ -217,7 +222,7 @@ let evars () = try Stm.finish (); let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); + if not (String.is_empty s) then Feedback.msg_info (str s); let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in @@ -250,7 +255,7 @@ let status force = Stm.finish (); if force then Stm.join (); let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); + if not (String.is_empty s) then Feedback.msg_info (str s); let path = let l = Names.DirPath.repr (Lib.cwd ()) in List.rev_map Names.Id.to_string l @@ -366,6 +371,7 @@ let init = 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) else Stm.get_current_state (), `NewTip in Stm.set_compilation_hints file; + Stm.finish (); initial_id end @@ -387,6 +393,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 = @@ -417,7 +432,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 @@ -438,16 +453,12 @@ let print_xml = let slave_logger xml_oc level message = (* convert the message into XML *) let msg = hov 0 message in - let message = { - Pp.message_level = level; - Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg)); - } in - let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in - let xml = Pp.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 *) @@ -465,8 +476,8 @@ let loop () = CThread.thread_friendly_read in_ch s ~off:0 ~len) in let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in - set_logger (slave_logger xml_oc); - set_feeder (slave_feeder xml_oc); + Feedback.set_logger (slave_logger xml_oc); + Feedback.set_feeder (slave_feeder xml_oc); (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; Vernacentries.qed_display_script := false; @@ -476,7 +487,7 @@ let loop () = (* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in let () = pr_debug_call q in - let r = eval_call xml_oc (slave_logger xml_oc Pp.Notice) q in + let r = eval_call xml_oc (slave_logger xml_oc Feedback.Notice) q in let () = pr_debug_answer q r in (* pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *) print_xml xml_oc (Xmlprotocol.of_answer q r); @@ -488,7 +499,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/ideutils.ml b/ide/ideutils.ml index 51ae76ff54..00c3f88e56 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -297,15 +297,15 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Pp.message_level -> Richpp.richpp -> unit +type logger = Feedback.level -> Richpp.richpp -> unit let default_logger level message = let level = match level with - | Pp.Debug _ -> `DEBUG - | Pp.Info -> `INFO - | Pp.Notice -> `NOTICE - | Pp.Warning -> `WARNING - | Pp.Error -> `ERROR + | Feedback.Debug _ -> `DEBUG + | Feedback.Info -> `INFO + | Feedback.Notice -> `NOTICE + | Feedback.Warning -> `WARNING + | Feedback.Error -> `ERROR in Minilib.log ~level (xml_to_string message) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index db2dce5a39..491e8e823d 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -69,7 +69,7 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Pp.message_level -> Richpp.richpp -> unit +type logger = Feedback.level -> Richpp.richpp -> unit val default_logger : logger (** Default logger. It logs messages that the casual user should not see. *) diff --git a/ide/interface.mli b/ide/interface.mli index f2f121ac01..2a9b8b241f 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 0668ad09f4..93bdeb324c 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/preferences.ml b/ide/preferences.ml index 3d11e94feb..c4dc55972b 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -386,14 +386,6 @@ let processing_color = let _ = attach_bg processing_color Tags.Script.to_process let _ = attach_bg processing_color Tags.Script.incomplete -let default_tag = { - tag_fg_color = None; - tag_bg_color = None; - tag_bold = false; - tag_italic = false; - tag_underline = false; -} - let tags = ref Util.String.Map.empty let list_tags () = !tags diff --git a/ide/preferences.mli b/ide/preferences.mli index b5c7ea2221..1733091a58 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 081094e2b6..de0720e033 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -56,24 +56,24 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) | ("-full"|"-opt") :: r -> process_cmd_line orig_dir (project_file,makefile,install,true) l r | "-impredicative-set" :: r -> - Pp.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform."); + 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 -> - Pp.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead"))); + 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 Pp.msg_warning (Pp.str "-install sets more than once."); + 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 - | _ -> Pp.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install."))); + | _ -> 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 -> - Pp.msg_warning (Pp.app + 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.") ); @@ -94,7 +94,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match project_file with | None -> () - | Some _ -> Pp.msg_warning (Pp.str + | 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 @@ -109,7 +109,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) let () = match makefile with |None -> () |Some f -> - Pp.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be."))) + 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 -> diff --git a/ide/richprinter.ml b/ide/richprinter.ml new file mode 100644 index 0000000000..5f39f36eab --- /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 0000000000..c9e84e3eb4 --- /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/sentence.ml b/ide/sentence.ml index 8195051c6c..6897779e80 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/sentence.mli b/ide/sentence.mli index f0ba5d22c3..feb3c0ac03 100644 --- a/ide/sentence.mli +++ b/ide/sentence.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/serialize.ml b/ide/serialize.ml new file mode 100644 index 0000000000..7b568501ed --- /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 0000000000..bf9e184ebb --- /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/session.ml b/ide/session.ml index e4cc177428..cdec392ecc 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -16,6 +16,7 @@ class type ['a] page = inherit GObj.widget method update : 'a -> unit method on_update : callback:('a -> unit) -> unit + method data : 'a end class type control = @@ -316,6 +317,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = errs end method on_update ~callback:cb = callback := cb + method data = !last_update end let create_jobpage coqtop coqops : jobpage = @@ -355,6 +357,7 @@ let create_jobpage coqtop coqops : jobpage = jobs end method on_update ~callback:cb = callback := cb + method data = !last_update end let create_proof () = diff --git a/ide/session.mli b/ide/session.mli index 3a6b458582..028a1f9de6 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -14,6 +14,7 @@ class type ['a] page = inherit GObj.widget method update : 'a -> unit method on_update : callback:('a -> unit) -> unit + method data : 'a end class type control = diff --git a/ide/tags.ml b/ide/tags.ml index 09b562530b..9ccff9fb51 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/tags.mli b/ide/tags.mli index 6418d1b2e5..5a932f3300 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml new file mode 100644 index 0000000000..d1d6de9ae8 --- /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 0000000000..858847fb6a --- /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/utf8_convert.mll b/ide/utf8_convert.mll index 4ebf9a62e1..5cc8cbc0d2 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml index 580f1fbcb3..8f6cb382a5 100644 --- a/ide/utils/okey.ml +++ b/ide/utils/okey.ml @@ -52,33 +52,6 @@ let int_of_modifier = function | `RELEASE -> 1 lsl 30 | `SUPER -> 1 lsl 21 -let print_modifier l = - List.iter - (fun m -> - print_string - (((function - `SHIFT -> "SHIFT" - | `LOCK -> "LOCK" - | `CONTROL -> "CONTROL" - | `MOD1 -> "MOD1" - | `MOD2 -> "MOD2" - | `MOD3 -> "MOD3" - | `MOD4 -> "MOD4" - | `MOD5 -> "MOD5" - | `BUTTON1 -> "B1" - | `BUTTON2 -> "B2" - | `BUTTON3 -> "B3" - | `BUTTON4 -> "B4" - | `BUTTON5 -> "B5" - | `HYPER -> "HYPER" - | `META -> "META" - | `RELEASE -> "" - | `SUPER -> "SUPER") - m)^" ") - ) - l; - print_newline () - let int_of_modifiers l = List.fold_left (fun acc -> fun m -> acc + (int_of_modifier m)) 0 l diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 7d8993aa8b..946aaf010d 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli index 1f0e31988a..fa50ba5fdd 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 7d77679ce5..aeae3e1fdb 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -86,7 +86,7 @@ let signals = [ end_s#disconnect; ] in object (self : 'a) - inherit GUtil.ml_signals signals as super + inherit GUtil.ml_signals signals method start_completion = start_s#connect ~after method update_completion = update_s#connect ~after method end_completion = end_s#connect ~after diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli index c3cb230d79..dd496aa5f5 100644 --- a/ide/wg_Completion.mli +++ b/ide/wg_Completion.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml index 53c634d7e2..3d1b63dfae 100644 --- a/ide/wg_Detachable.ml +++ b/ide/wg_Detachable.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_Detachable.mli b/ide/wg_Detachable.mli index 71f85ad828..a7e8f46763 100644 --- a/ide/wg_Detachable.mli +++ b/ide/wg_Detachable.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index dc7071c278..3d847ddcc1 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_Find.mli b/ide/wg_Find.mli index 7811fc43ef..1ef1c4d499 100644 --- a/ide/wg_Find.mli +++ b/ide/wg_Find.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 615e989de9..758f383d6d 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -73,8 +73,8 @@ let message_view () : message_view = method push level msg = let tags = match level with - | Pp.Error -> [Tags.Message.error] - | Pp.Warning -> [Tags.Message.warning] + | Feedback.Error -> [Tags.Message.error] + | Feedback.Warning -> [Tags.Message.warning] | _ -> [] in let rec non_empty = function @@ -88,7 +88,7 @@ let message_view () : message_view = push#call (level, msg) end - method add msg = self#push Pp.Notice msg + method add msg = self#push Feedback.Notice msg method add_string s = self#add (Richpp.richpp_of_string s) diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 388ab259fd..2d34533dee 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml index 0611c3f396..08d7d19833 100644 --- a/ide/wg_Notebook.ml +++ b/ide/wg_Notebook.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_Notebook.mli b/ide/wg_Notebook.mli index 15a2ba41e9..34eb1d11e3 100644 --- a/ide/wg_Notebook.mli +++ b/ide/wg_Notebook.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 642a577878..47c86045a5 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -91,7 +91,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with let () = proof#buffer#insert head_str in let () = insert_hyp hyps_hints hyps in let () = - let tags = Tags.Proof.goal :: if goal_hints <> [] then + let _ = if goal_hints <> [] then let tag = proof#buffer#create_tag [] in let () = hook_tag_cb tag goal_hints sel_cb on_hover in [tag] diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index c5e042ea52..b6eae48b39 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index b672e016b4..218cedb363 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -287,7 +287,7 @@ let completion = new Wg_Completion.complete_model ct view#buffer in let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in object (self) - inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super + inherit GSourceView2.source_view (Gobject.unsafe_cast tv) val undo_manager = new undo_manager view#buffer diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index 6e54c4452f..6cce5e5b43 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index 2ee2884547..dbc1740ef6 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -11,53 +11,13 @@ open Preferences type color = GDraw.color -module Segment : -sig - type +'a t - val length : 'a t -> int - val resize : 'a t -> int -> 'a t - val empty : 'a t - val add : int -> 'a -> 'a t -> 'a t - val remove : int -> 'a t -> 'a t - val fold : ('a -> 'a -> bool) -> (int -> int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b -end = -struct - type 'a t = { - length : int; - content : 'a Int.Map.t; - } - - let empty = { length = 0; content = Int.Map.empty } - - let length s = s.length - - let resize s len = - if s.length <= len then { s with length = len } - else - let filter i v = i < len in - { length = len; content = Int.Map.filter filter s.content } - - let add i v s = - if i < s.length then - { s with content = Int.Map.add i v s.content } - else s - - let remove i s = { s with content = Int.Map.remove i s.content } - - let fold eq f s accu = - let make k v (cur, accu) = match cur with - | None -> Some (k, k, v), accu - | Some (i, j, w) -> - if k = j + 1 && eq v w then Some (i, k, w), accu - else Some (k, k, v), (i, j, w) :: accu - in - let p, segments = Int.Map.fold make s.content (None, []) in - let segments = match p with - | None -> segments - | Some p -> p :: segments - in - List.fold_left (fun accu (i, j, v) -> f i j v accu) accu segments +type model_event = [ `INSERT | `REMOVE | `SET of int * color ] +class type model = +object + method changed : callback:(model_event -> unit) -> unit + method length : int + method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a end let i2f = float_of_int @@ -96,10 +56,12 @@ object (self) val mutable width = 1 val mutable height = 20 - val mutable data = Segment.empty + val mutable model : model option = None 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 (); @@ -114,10 +76,12 @@ object (self) end in let _ = box#misc#connect#size_allocate cb in - let clicked_cb ev = + let clicked_cb ev = match model with + | None -> true + | Some md -> let x = GdkEvent.Button.x ev in let (width, _) = pixmap#size in - let len = Segment.length data in + let len = md#length in let idx = f2i ((x *. i2f len) /. i2f width) in let () = clicked#call idx in true @@ -126,19 +90,27 @@ 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 - - method length = Segment.length data - - method set_length len = - data <- Segment.resize data len; - if self#misc#visible then self#refresh () + 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 need_refresh <- true + | `SET (i, color) -> + if self#misc#visible then self#fill_range color i (i + 1) + in + md#changed changed_cb - method private fill_range color i j = + method private fill_range color i j = match model with + | None -> () + | Some md -> let i = i2f i in let j = i2f j in let width = i2f width in - let len = i2f (Segment.length data) in + let len = i2f md#length in let x = f2i ((i *. width) /. len) in let x' = f2i ((j *. width) /. len) in let w = x' - x in @@ -146,14 +118,6 @@ object (self) pixmap#rectangle ~x ~y:0 ~width:w ~height ~filled:true (); draw#set_mask None; - method add i color = - data <- Segment.add i color data; - if self#misc#visible then self#fill_range color i (i + 1) - - method remove i = - data <- Segment.remove i data; - if self#misc#visible then self#fill_range default i (i + 1) - method set_default_color color = default <- color method default_color = default @@ -162,11 +126,24 @@ object (self) draw#set_pixmap pixmap; self#refresh (); - method private refresh () = + 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 fold i j v () = self#fill_range v i (j + 1) in - Segment.fold color_eq fold data (); + let make (k, cur, accu) v = match cur with + | None -> pred k, Some (k, k, v), accu + | Some (i, j, w) -> + if k = j - 1 && color_eq v w then pred k, Some (k, i, w), accu + else pred k, Some (k, k, v), (i, j, w) :: accu + in + let _, p, segments = md#fold make (md#length - 1, None, []) in + let segments = match p with + | None -> segments + | Some p -> p :: segments + in + List.iter (fun (i, j, v) -> self#fill_range v i (j + 1)) segments; draw#set_mask None; method connect = diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli index 0263856ae1..29cbbedacf 100644 --- a/ide/wg_Segment.mli +++ b/ide/wg_Segment.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -8,6 +8,8 @@ type color = GDraw.color +type model_event = [ `INSERT | `REMOVE | `SET of int * color ] + class type segment_signals = object inherit GObj.misc_signals @@ -15,15 +17,19 @@ object method clicked : callback:(int -> unit) -> GtkSignal.id end +class type model = +object + method changed : callback:(model_event -> unit) -> unit + method length : int + method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a +end + class segment : unit -> object inherit GObj.widget val obj : Gtk.widget Gtk.obj + method set_model : model -> unit method connect : segment_signals - method length : int - method set_length : int -> unit method default_color : color method set_default_color : color -> unit - method add : int -> color -> unit - method remove : int -> unit end diff --git a/ide/xml_lexer.mli b/ide/xml_lexer.mli new file mode 100644 index 0000000000..e61cb055f7 --- /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 0000000000..290f2c89ab --- /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 0000000000..8db3f9e8ba --- /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 0000000000..ac2eab352f --- /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 0000000000..e7e4d0cebc --- /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 " "; + | '>' -> output ">" + | '<' -> output "<" + | '&' -> + if p < l - 1 && text.[p + 1] = '#' then + output' '&' + else + output "&" + | '\'' -> output "'" + | '"' -> output """ + | 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 "<" + | '&' -> output "&" + | 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 0000000000..f24f51fff5 --- /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 bb6a18158d..a55d19aa1b 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -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 7806550d1c..6bca8772ed 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -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 *) + |
