From facf0520a47603d2679508136cbed43def0744cc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 13:46:07 +0100 Subject: [safe-string] ide No functional change, one extra copy introduced but it seems hard to avoid. --- ide/coqide.ml | 4 ++-- ide/ideutils.ml | 25 ++++++++++++++----------- 2 files changed, 16 insertions(+), 13 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 450bfcdfb1..eec829f345 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -887,8 +887,8 @@ let alpha_items menu_name item_name l = | [] -> () | [s] -> mk_item s | s::_ as ll -> - let name = item_name^" "^(String.make 1 s.[0]) in - let label = "_@..." in label.[1] <- s.[0]; + let name = Printf.sprintf "%s %c" item_name s.[0] in + let label = Printf.sprintf "_%c..." s.[0] in item name ~label menu_name; List.iter mk_item ll in diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 06a1327320..c3a2807967 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -294,18 +294,20 @@ let coqtop_path () = match cmd_coqtop#get with | Some s -> s | None -> - let prog = String.copy Sys.executable_name in try - let pos = String.length prog - 6 in - let i = Str.search_backward (Str.regexp_string "coqide") prog pos + let old_prog = Sys.executable_name in + let pos = String.length old_prog - 6 in + let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos in - String.blit "coqtop" 0 prog i 6; - if Sys.file_exists prog then prog + let new_prog = Bytes.of_string old_prog in + Bytes.blit_string "coqtop" 0 new_prog i 6; + let new_prog = Bytes.to_string new_prog in + if Sys.file_exists new_prog then new_prog else let in_macos_bundle = Filename.concat - (Filename.dirname prog) - (Filename.concat "../Resources/bin" (Filename.basename prog)) + (Filename.dirname new_prog) + (Filename.concat "../Resources/bin" (Filename.basename new_prog)) in if Sys.file_exists in_macos_bundle then in_macos_bundle else "coqtop" with Not_found -> "coqtop" @@ -357,7 +359,7 @@ let stat f = let maxread = 4096 -let read_string = String.create maxread +let read_string = Bytes.create maxread let read_buffer = Buffer.create maxread (** Read the content of file [f] and add it to buffer [b]. @@ -368,7 +370,7 @@ let read_file name buf = let len = ref 0 in try while len := input ic read_string 0 maxread; !len > 0 do - Buffer.add_substring buf read_string 0 !len + Buffer.add_subbytes buf read_string 0 !len done; close_in ic with e -> close_in ic; raise e @@ -381,8 +383,9 @@ let read_file name buf = let io_read_all chan = Buffer.clear read_buffer; let read_once () = - let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in - Buffer.add_substring read_buffer read_string 0 len + (* XXX: Glib.Io must be converted to bytes / -safe-string upstream *) + let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in + Buffer.add_subbytes read_buffer read_string 0 len in begin try while true do read_once () done -- cgit v1.2.3 From f1c5e2ce2a4515a7c90c5ca22aa6eff22dd2f5ff Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 28 Jun 2016 16:52:46 +0200 Subject: [ide] Use "log via feedback". We remove the custom logger handler in ide_slave, and handle everything via feedback. This is an experimental patch but it seems to bring quite a bit of cleanup and a more uniform handling to messaging. --- ide/coq.ml | 47 +++++++++++++++-------------------------------- ide/coq.mli | 12 ++++-------- ide/coqOps.ml | 21 +++++++++++---------- ide/coqide.ml | 2 +- ide/ide_slave.ml | 14 ++++---------- ide/wg_Command.ml | 6 +----- ide/xmlprotocol.ml | 6 ------ ide/xmlprotocol.mli | 2 -- 8 files changed, 36 insertions(+), 74 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index 6d44ca59e3..9637b5b3f2 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -205,7 +205,7 @@ type handle = { proc : CoqTop.process; xml_oc : Xml_printer.t; mutable alive : bool; - mutable waiting_for : (ccb * logger) option; (* last call + callback + log *) + mutable waiting_for : ccb option; (* last call + callback + log *) } (** Coqtop process status : @@ -290,18 +290,6 @@ let rec check_errors = function | `NVAL :: _ -> raise (TubeError "NVAL") | `OUT :: _ -> raise (TubeError "OUT") -let handle_intermediate_message handle level content = - let logger = match handle.waiting_for with - | Some (_, l) -> l - | None -> function - | Feedback.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s) - | Feedback.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s) - | 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 content - let handle_feedback feedback_processor xml = let feedback = Xmlprotocol.to_feedback xml in feedback_processor feedback @@ -310,7 +298,7 @@ let handle_final_answer handle xml = let () = Minilib.log "Handling coqtop answer" in let ccb = match handle.waiting_for with | None -> raise (AnswerWithoutRequest (Xml_printer.to_string_fmt xml)) - | Some (c, _) -> c in + | Some c -> c in let () = handle.waiting_for <- None in with_ccb ccb { bind_ccb = fun (c, f) -> f (Xmlprotocol.to_answer c xml) } @@ -332,18 +320,13 @@ 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; - match Xmlprotocol.is_message xml with - | Some (lvl, _loc, msg) -> - handle_intermediate_message handle lvl msg; + if Xmlprotocol.is_feedback xml then begin + handle_feedback feedback_processor xml; loop () - | None -> - if Xmlprotocol.is_feedback xml then begin - handle_feedback feedback_processor xml; - loop () - end else - begin - ignore (handle_final_answer handle xml) - end + end else + begin + ignore (handle_final_answer handle xml) + end in try loop () with Xml_parser.Error _ as e -> @@ -493,20 +476,20 @@ let init_coqtop coqtop task = type 'a query = 'a Interface.value task -let eval_call ?(logger=default_logger) call handle k = +let eval_call call handle k = (** Send messages to coqtop and prepare the decoding of the answer *) Minilib.log ("Start eval_call " ^ Xmlprotocol.pr_call call); assert (handle.alive && handle.waiting_for = None); - handle.waiting_for <- Some (mk_ccb (call,k), logger); + handle.waiting_for <- Some (mk_ccb (call,k)); Xml_printer.print handle.xml_oc (Xmlprotocol.of_call call); Minilib.log "End eval_call"; Void -let add ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.add x) +let add x = eval_call (Xmlprotocol.add x) let edit_at i = eval_call (Xmlprotocol.edit_at i) -let query ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.query x) +let query x = eval_call (Xmlprotocol.query x) let mkcases s = eval_call (Xmlprotocol.mkcases s) -let status ?logger force = eval_call ?logger (Xmlprotocol.status force) +let status force = eval_call (Xmlprotocol.status force) let hints x = eval_call (Xmlprotocol.hints x) let search flags = eval_call (Xmlprotocol.search flags) let init x = eval_call (Xmlprotocol.init x) @@ -585,8 +568,8 @@ struct end -let goals ?logger x h k = - PrintOpt.enforce h (fun () -> eval_call ?logger (Xmlprotocol.goals x) h k) +let goals x h k = + PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.goals x) h k) let evars x h k = PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.evars x) h k) diff --git a/ide/coq.mli b/ide/coq.mli index 8a1fa3ed15..f2876de246 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -115,15 +115,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit type 'a query = 'a Interface.value task (** A type abbreviation for coqtop specific answers *) -val add : ?logger:Ideutils.logger -> - Interface.add_sty -> Interface.add_rty query +val add : Interface.add_sty -> Interface.add_rty query val edit_at : Interface.edit_at_sty -> Interface.edit_at_rty query -val query : ?logger:Ideutils.logger -> - Interface.query_sty -> Interface.query_rty query -val status : ?logger:Ideutils.logger -> - Interface.status_sty -> Interface.status_rty query -val goals : ?logger:Ideutils.logger -> - Interface.goals_sty -> Interface.goals_rty query +val query : Interface.query_sty -> Interface.query_rty query +val status : Interface.status_sty -> Interface.status_rty query +val goals : Interface.goals_sty -> Interface.goals_rty query val evars : Interface.evars_sty -> Interface.evars_rty query val hints : Interface.hints_sty -> Interface.hints_rty query val mkcases : Interface.mkcases_sty -> Interface.mkcases_rty query diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 1563c7ffb4..0f3629c8fc 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -345,7 +345,7 @@ object(self) script#recenter_insert end end; - Coq.bind (Coq.goals ~logger:messages#push ()) (function + Coq.bind (Coq.goals ()) (function | Fail x -> self#handle_failure_aux ~move_insert x | Good goals -> Coq.bind (Coq.evars ()) (function @@ -368,7 +368,7 @@ object(self) else messages#add s; in let query = - Coq.query ~logger:messages#push (phrase,Stateid.dummy) in + Coq.query (phrase,Stateid.dummy) in let next = function | Fail (_, _, err) -> display_error err; Coq.return () | Good msg -> @@ -476,13 +476,14 @@ object(self) self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) | Message(Warning, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let msg = Richpp.raw_print msg in + let rmsg = Richpp.raw_print msg in log "WarningMsg" id; - add_flag sentence (`WARNING (loc, msg)); - self#attach_tooltip sentence loc msg; - self#position_warning_tag_at_sentence sentence loc - | Message((Info|Notice|Debug as lvl), _, msg), _ -> - messages#push lvl msg + add_flag sentence (`WARNING (loc, rmsg)); + self#attach_tooltip sentence loc rmsg; + self#position_warning_tag_at_sentence sentence loc; + messages#push Warning msg + | Message(lvl, loc, msg), Some (id,sentence) -> + messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n @@ -641,7 +642,7 @@ object(self) add_flag sentence `PROCESSING; Doc.push document sentence; let _, _, phrase = self#get_sentence sentence in - let coq_query = Coq.add ~logger ((phrase,edit_id),(tip,verbose)) in + let coq_query = Coq.add ((phrase,edit_id),(tip,verbose)) in let handle_answer = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> Doc.assign_tip_id document id; @@ -675,7 +676,7 @@ object(self) 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 + Coq.bind (Coq.status true) next method stop_worker n = Coq.bind (Coq.stop_worker n) (fun _ -> Coq.return ()) diff --git a/ide/coqide.ml b/ide/coqide.ml index eec829f345..3d56f9dd49 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -536,7 +536,7 @@ let update_status sn = display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name); Coq.return () in - Coq.bind (Coq.status ~logger:sn.messages#push false) next + Coq.bind (Coq.status false) next let find_next_occurrence ~backward sn = (** go to the next occurrence of the current word, forward or backward *) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index ae3dcd94a9..7619c1452e 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -428,7 +428,7 @@ let print_ast id = (** Grouping all call handlers together + error handling *) -let eval_call xml_oc log c = +let eval_call log c = let interruptible f x = catch_break := true; Control.check_for_interrupt (); @@ -474,13 +474,6 @@ let print_xml = with e -> let e = CErrors.push e in Mutex.unlock m; iraise e -let slave_logger xml_oc ?loc level message = - (* convert the message into XML *) - let msg = hov 0 message in - let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in - let xml = Xmlprotocol.of_message level loc (Richpp.richpp_of_pp message) in - print_xml xml_oc xml - let slave_feeder xml_oc msg = let xml = Xmlprotocol.of_feedback msg in print_xml xml_oc xml @@ -500,8 +493,9 @@ 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 - Feedback.set_logger (slave_logger xml_oc); + Feedback.set_logger Feedback.feedback_logger; Feedback.add_feeder (slave_feeder xml_oc); + let f_log str = Feedback.(feedback (Message(Notice, None, Richpp.richpp_of_pp str))) in (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; Vernacentries.qed_display_script := false; @@ -511,7 +505,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 Feedback.Notice) q in + let r = eval_call f_log 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); diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 946aaf010d..d33c0add4a 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -100,12 +100,8 @@ object(self) if Str.string_match (Str.regexp "\\. *$") com 0 then com else com ^ " " ^ arg ^" . " in - let log level message = - Ideutils.insert_xml result#buffer message; - result#buffer#insert "\n"; - in let process = - Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function + Coq.bind (Coq.query (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> Ideutils.insert_xml result#buffer str; notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 5f82a8898b..65f44fdd38 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -795,12 +795,6 @@ let to_message xml = match xml with Message(to_message_level lvl, to_option to_loc xloc, to_richpp content) | x -> raise (Marshal_error("message",x)) -let is_message xml = - try begin match to_message xml with - | Message(l,c,m) -> Some (l,c,m) - | _ -> None - end with | Marshal_error _ -> None - let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "addedaxiom", _ -> AddedAxiom | "processed", _ -> Processed diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 1bb9989704..ca911178f5 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -66,7 +66,5 @@ val of_feedback : Feedback.feedback -> xml val to_feedback : xml -> Feedback.feedback val is_feedback : xml -> bool -val is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml -(* val to_message : xml -> Feedback.message *) -- cgit v1.2.3 From eda304d2f0531b8fa088a2d71d369d4482f29ed2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 28 Jun 2016 19:17:21 +0200 Subject: [ide] ide_slave doesnt't need to capture stdout The miscellaneous `msg_*` cleanup patches have finally enforced this invariant. --- ide/ide_slave.ml | 49 ++++++++++++------------------------------------- 1 file changed, 12 insertions(+), 37 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 7619c1452e..8a1f8c6383 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -35,21 +35,6 @@ let init_signal_handler () = (** Redirection of standard output to a printable buffer *) -let init_stdout, read_stdout = - let out_buff = Buffer.create 100 in - let out_ft = Format.formatter_of_buffer out_buff in - let deep_out_ft = Format.formatter_of_buffer out_buff in - let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in - (fun () -> - flush_all (); - Pp_control.std_ft := out_ft; - Pp_control.err_ft := out_ft; - Pp_control.deep_ft := deep_out_ft; - ), - (fun () -> Format.pp_print_flush out_ft (); - let r = Buffer.contents out_buff in - Buffer.clear out_buff; r) - let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s let pr_error s = pr_with_pid s @@ -115,14 +100,14 @@ let coqide_cmd_checks (loc,ast) = let add ((s,eid),(sid,verbose)) = let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in - newid, (rc, read_stdout ()) + newid, (rc, "") let edit_at id = match Stm.edit_at id with | `NewTip -> CSig.Inl () | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip)) -let query (s,id) = Stm.query ~at:id s; read_stdout () +let query (s,id) = Stm.query ~at:id s; "" let annotate phrase = let (loc, ast) = @@ -214,8 +199,6 @@ let export_pre_goals pgs = let goals () = Stm.finish (); - let s = read_stdout () in - 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)) @@ -224,8 +207,6 @@ let goals () = let evars () = try Stm.finish (); - let s = read_stdout () in - 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 @@ -257,8 +238,6 @@ let status force = and display the other parts (opened sections and modules) *) Stm.finish (); if force then Stm.join (); - let s = read_stdout () in - 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 @@ -365,8 +344,7 @@ let handle_exn (e, info) = | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) | _ -> None in let mk_msg () = - let msg = read_stdout () in - let msg = str msg ++ fnl () ++ CErrors.print ~info e in + let msg = CErrors.print ~info e in Richpp.richpp_of_pp msg in match e with @@ -409,7 +387,7 @@ let interp ((_raw, verbose), s) = | Some ast -> ast) () in Stm.interp verbose (vernac_parse s); - Stm.get_current_state (), CSig.Inl (read_stdout ()) + Stm.get_current_state (), CSig.Inl "" (** When receiving the Quit call, we don't directly do an [exit 0], but rather set this reference, in order to send a final answer @@ -428,14 +406,12 @@ let print_ast id = (** Grouping all call handlers together + error handling *) -let eval_call log c = +let eval_call c = let interruptible f x = catch_break := true; Control.check_for_interrupt (); let r = f x in catch_break := false; - let out = read_stdout () in - if not (String.is_empty out) then log (str out); r in let handler = { @@ -487,15 +463,15 @@ let slave_feeder xml_oc msg = let loop () = init_signal_handler (); catch_break := false; - let in_ch, out_ch = Spawned.get_channels () in - let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in - let in_lb = Lexing.from_function (fun s len -> - CThread.thread_friendly_read in_ch s ~off:0 ~len) in - let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in + let in_ch, out_ch = Spawned.get_channels () in + let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in + let in_lb = Lexing.from_function (fun s len -> + CThread.thread_friendly_read in_ch s ~off:0 ~len) in + (* SEXP parser make *) + let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in Feedback.set_logger Feedback.feedback_logger; Feedback.add_feeder (slave_feeder xml_oc); - let f_log str = Feedback.(feedback (Message(Notice, None, Richpp.richpp_of_pp str))) in (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; Vernacentries.qed_display_script := false; @@ -505,7 +481,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 f_log q in + let r = eval_call 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); @@ -536,7 +512,6 @@ let rec parse = function let () = Coqtop.toploop_init := (fun args -> let args = parse args in Flags.make_silent true; - init_stdout (); CoqworkmgrApi.(init Flags.High); args) -- cgit v1.2.3 From 8c5adfd5acb883a3bc2850b6fc8c29d352a421f8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 Jun 2016 17:52:39 +0200 Subject: [pp] Remove unused printing tagging infrastructure. Applications of it were not clear/unproven, it made printers more complex (as they needed to be functors) and as it lacked examples it confused some people. The printers now tag unconditionally, it is up to the backends to interpreted the tags. Tagging (and indeed the notion of rich document) should be reworked in a follow-up patch, so they are in sync, but this is a first step. Tested, test-suite passes. Notes: - We remove the `Richprinter` module. It was only used in the `annotate` IDE protocol call, its output was identical to the normal printer (or even inconsistent if taggers were not kept manually in sync). - Note that Richpp didn't need a single change. In particular, its main API entry point `Richpp.rich_pp` is not used by anyone. --- ide/ide_slave.ml | 7 ++----- ide/richprinter.ml | 23 ----------------------- ide/richprinter.mli | 36 ------------------------------------ 3 files changed, 2 insertions(+), 64 deletions(-) delete mode 100644 ide/richprinter.ml delete mode 100644 ide/richprinter.mli (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8a1f8c6383..0cb8d377f6 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -114,11 +114,8 @@ let annotate phrase = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in Vernac.parse_sentence (pa,None) in - let (_, xml) = - Richprinter.richpp_vernac ast - in - xml - + Richpp.repr (Richpp.richpp_of_pp (Ppvernac.pr_vernac ast)) + (** Goal display *) let hyp_next_tac sigma env decl = diff --git a/ide/richprinter.ml b/ide/richprinter.ml deleted file mode 100644 index 995cef1ac5..0000000000 --- a/ide/richprinter.ml +++ /dev/null @@ -1,23 +0,0 @@ -open Richpp - -module RichppConstr = Ppconstr.Richpp -module RichppVernac = Ppvernac.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 deleted file mode 100644 index c9e84e3eb4..0000000000 --- a/ide/richprinter.mli +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* rich_pp - -(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *) -val richpp_constr : Constrexpr.constr_expr -> rich_pp -- cgit v1.2.3 From 5b8bfee9d80e550cd81e326ec134430b2a4797a5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:30:21 +0200 Subject: [pp] Make feedback the only logging mechanism. Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent. --- ide/coq.ml | 2 +- ide/coqOps.ml | 44 ++++++----- ide/coqide.ml | 16 ++-- ide/coqidetop.mllib | 2 +- ide/ide.mllib | 4 +- ide/ide_slave.ml | 20 ++--- ide/ideutils.ml | 4 +- ide/ideutils.mli | 2 +- ide/interface.mli | 9 +-- ide/richpp.ml | 200 +++++++++++++++++++++++++++++++++++++++++++++++++ ide/richpp.mli | 64 ++++++++++++++++ ide/wg_Command.ml | 2 +- ide/wg_MessageView.ml | 21 ++---- ide/wg_MessageView.mli | 4 +- ide/wg_ProofView.ml | 12 +-- ide/xmlprotocol.ml | 71 ++++++++++++++---- ide/xmlprotocol.mli | 3 +- 17 files changed, 388 insertions(+), 92 deletions(-) create mode 100644 ide/richpp.ml create mode 100644 ide/richpp.mli (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index 9637b5b3f2..e2036beee3 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -205,7 +205,7 @@ type handle = { proc : CoqTop.process; xml_oc : Xml_printer.t; mutable alive : bool; - mutable waiting_for : ccb option; (* last call + callback + log *) + mutable waiting_for : ccb option; (* last call + callback *) } (** Coqtop process status : diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 0f3629c8fc..7982ffc8b8 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -162,13 +162,16 @@ let flags_to_color f = else if List.mem `INCOMPLETE f then `NAME "gray" else `NAME Preferences.processed_color#get -let validate s = - let open Xml_datatype in - let rec validate = function - | PCData s -> Glib.Utf8.validate s - | Element (_, _, children) -> List.for_all validate children - in - validate (Richpp.repr s) +(* Move to utils? *) +let rec validate (s : Pp.std_ppcmds) = match s with + | Pp.Ppcmd_empty + | Pp.Ppcmd_print_break _ + | Pp.Ppcmd_force_newline -> true + | Pp.Ppcmd_glue l -> List.for_all validate l + | Pp.Ppcmd_string s -> Glib.Utf8.validate s + | Pp.Ppcmd_box (_,s) + | Pp.Ppcmd_tag (_,s) -> validate s + | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s module Doc = Document @@ -418,9 +421,10 @@ object(self) | _ -> false method private enqueue_feedback msg = + (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *) let id = msg.id in if self#is_dummy_id id then () else Queue.add msg feedbacks - + method private process_feedback () = let rec eat_feedback n = if n = 0 then true else @@ -466,7 +470,7 @@ object(self) (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let msg = Richpp.raw_print msg in + let msg = Pp.string_of_ppcmds msg in log "ErrorMsg" id; remove_flag sentence `PROCESSING; add_flag sentence (`ERROR (loc, msg)); @@ -476,14 +480,15 @@ object(self) self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) | Message(Warning, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let rmsg = Richpp.raw_print msg in - log "WarningMsg" id; + let rmsg = Pp.string_of_ppcmds msg in + log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id; add_flag sentence (`WARNING (loc, rmsg)); self#attach_tooltip sentence loc rmsg; self#position_warning_tag_at_sentence sentence loc; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> - messages#push lvl msg + log ("Msg: " ^ Pp.string_of_ppcmds msg) id; + messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n @@ -629,10 +634,9 @@ object(self) if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> - - logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted"); + logger Feedback.Error (Pp.str "You must close the proof with Qed or Admitted"); self#discard_command_queue queue; - conclude [] + conclude [] | `Skip(start,stop), (_,s) :: topstack -> assert(start#equal (buffer#get_iter_at_mark s.start)); assert(stop#equal (buffer#get_iter_at_mark s.stop)); @@ -646,7 +650,7 @@ object(self) let handle_answer = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> Doc.assign_tip_id document id; - logger Feedback.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Pp.str msg); self#commit_queue_transaction sentence; loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> @@ -654,7 +658,7 @@ object(self) let topstack, _ = Doc.context document in self#exit_focus; self#cleanup (Doc.cut_at document tip); - logger Feedback.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Pp.str msg); self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) @@ -673,7 +677,7 @@ object(self) let next = function | Good _ -> messages#clear; - messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel"); + messages#push Feedback.Info (Pp.str "All proof terms checked by the kernel"); Coq.return () | Fail x -> self#handle_failure x in Coq.bind (Coq.status true) next @@ -860,7 +864,7 @@ object(self) let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); - messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase)); + messages#add (Pp.str ("Unsuccessfully tried: "^phrase)); more | Good msg -> messages#add_string msg; @@ -906,7 +910,7 @@ object(self) let get_initial_state = let next = function | Fail (_, _, message) -> - let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in + let message = "Couldn't initialize coqtop\n\n" ^ (Pp.string_of_ppcmds 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 diff --git a/ide/coqide.ml b/ide/coqide.ml index 3d56f9dd49..25858acced 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -318,7 +318,7 @@ let export kind sn = local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1" in - sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd)); + sn.messages#set (Pp.str ("Running: "^cmd)); let finally st = flash_info (cmd ^ pr_exit_status st) in run_command (fun msg -> sn.messages#add_string msg) finally cmd @@ -431,7 +431,7 @@ let compile sn = ^ " " ^ (Filename.quote f) ^ " 2>&1" in let buf = Buffer.create 1024 in - sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd)); + sn.messages#set (Pp.str ("Running: "^cmd)); let display s = sn.messages#add_string s; Buffer.add_string buf s @@ -441,8 +441,8 @@ let compile sn = flash_info (f ^ " successfully compiled") else begin flash_info (f ^ " failed to compile"); - sn.messages#set (Richpp.richpp_of_string "Compilation output:\n"); - sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf)); + sn.messages#set (Pp.str "Compilation output:\n"); + sn.messages#add (Pp.str (Buffer.contents buf)); end in run_command display finally cmd @@ -464,7 +464,7 @@ let make sn = |Some f -> File.saveall (); let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in - sn.messages#set (Richpp.richpp_of_string "Compilation output:\n"); + sn.messages#set (Pp.str "Compilation output:\n"); Buffer.reset last_make_buf; last_make := ""; last_make_index := 0; @@ -508,11 +508,11 @@ let next_error sn = let stopi = b#get_iter_at_byte ~line:(line-1) stop in b#apply_tag Tags.Script.error ~start:starti ~stop:stopi; b#place_cursor ~where:starti; - sn.messages#set (Richpp.richpp_of_string error_msg); + sn.messages#set (Pp.str error_msg); sn.script#misc#grab_focus () with Not_found -> last_make_index := 0; - sn.messages#set (Richpp.richpp_of_string "No more errors.\n") + sn.messages#set (Pp.str "No more errors.\n") let next_error = cb_on_current_term next_error @@ -789,7 +789,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 Feedback.Error (Richpp.richpp_of_string msg) + sn.messages#push Feedback.Error (Pp.str msg) else dialog#destroy () in let _ = entry#connect#activate ok_cb in diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib index ed1fa465d2..043ad6008b 100644 --- a/ide/coqidetop.mllib +++ b/ide/coqidetop.mllib @@ -2,7 +2,7 @@ Xml_lexer Xml_parser Xml_printer Serialize -Richprinter +Richpp Xmlprotocol Texmacspp Document diff --git a/ide/ide.mllib b/ide/ide.mllib index 72a14134bf..12170c4621 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -9,11 +9,11 @@ Config_lexer Utf8_convert Preferences Project_file -Serialize -Richprinter Xml_lexer Xml_parser Xml_printer +Serialize +Richpp Xmlprotocol Ideutils Coq diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 0cb8d377f6..88b61042ed 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -32,9 +32,6 @@ let init_signal_handler () = let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in Sys.set_signal Sys.sigint (Sys.Signal_handle f) - -(** Redirection of standard output to a printable buffer *) - let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s let pr_error s = pr_with_pid s @@ -174,13 +171,13 @@ let process_goal sigma g = let id = Goal.uid g in let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) + pr_goal_concl_style_env env sigma norm_constr in let process_hyp d (env,l) = let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in let d' = CompactedDecl.to_named_context d in (List.fold_right Environ.push_named d' env, - (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in + (pr_compacted_decl env sigma d) :: l) in let (_env, hyps) = Context.Compacted.fold process_hyp (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in @@ -340,13 +337,10 @@ let handle_exn (e, info) = let loc_of e = match Loc.get_loc e with | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) | _ -> None in - let mk_msg () = - let msg = CErrors.print ~info e in - Richpp.richpp_of_pp msg - in + let mk_msg () = CErrors.print ~info e in match e with - | CErrors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!" - | CErrors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!" + | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!" + | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!" | e -> match Stateid.get info with | Some (valid, _) -> valid, loc_of info, mk_msg () @@ -446,7 +440,6 @@ let print_xml = try Xml_printer.print oc xml; Mutex.unlock m with e -> let e = CErrors.push e in Mutex.unlock m; iraise e - let slave_feeder xml_oc msg = let xml = Xmlprotocol.of_feedback msg in print_xml xml_oc xml @@ -467,7 +460,6 @@ let loop () = (* SEXP parser make *) let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in - Feedback.set_logger Feedback.feedback_logger; Feedback.add_feeder (slave_feeder xml_oc); (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; @@ -478,7 +470,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 q in + let r = eval_call 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); diff --git a/ide/ideutils.ml b/ide/ideutils.ml index c3a2807967..498a911ee4 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -327,7 +327,7 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Feedback.level -> Richpp.richpp -> unit +type logger = Feedback.level -> Pp.std_ppcmds -> unit let default_logger level message = let level = match level with @@ -337,7 +337,7 @@ let default_logger level message = | Feedback.Warning -> `WARNING | Feedback.Error -> `ERROR in - Minilib.log ~level (xml_to_string message) + Minilib.log ~level (Pp.string_of_ppcmds message) (** {6 File operations} *) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index e32a4d9e38..1ae66e23e9 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -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 = Feedback.level -> Richpp.richpp -> unit +type logger = Feedback.level -> Pp.std_ppcmds -> 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 123cac6c22..43446f3918 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -12,15 +12,14 @@ type raw = bool type verbose = bool -type richpp = Richpp.richpp (** The type of coqtop goals *) type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : richpp list; + goal_hyp : Pp.std_ppcmds list; (** List of hypotheses *) - goal_ccl : richpp; + goal_ccl : Pp.std_ppcmds; (** Goal conclusion *) } @@ -119,7 +118,7 @@ type edit_id = Feedback.edit_id should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * richpp) + | Fail of (state_id * location * Pp.std_ppcmds) type ('a, 'b) union = ('a, 'b) Util.union @@ -203,7 +202,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * richpp +type handle_exn_rty = state_id * location * Pp.std_ppcmds (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string diff --git a/ide/richpp.ml b/ide/richpp.ml new file mode 100644 index 0000000000..c0128dbc2d --- /dev/null +++ b/ide/richpp.ml @@ -0,0 +1,200 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* assert false + | Node (node, child, pos, ctx) -> + let data = Buffer.contents pp_buffer in + let () = Buffer.clear pp_buffer in + let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in + context.offset <- context.offset + len + in + + let open_xml_tag tag = + let () = push_pcdata () in + context.stack <- Node (tag, [], context.offset, context.stack) + in + + let close_xml_tag tag = + let () = push_pcdata () in + match context.stack with + | Leaf -> assert false + | Node (node, child, pos, ctx) -> + let () = assert (String.equal tag node) in + let annotation = + try Int.Map.find (int_of_string node) context.annotations + with _ -> None + in + let annotation = { + annotation = annotation; + startpos = pos; + endpos = context.offset; + } in + let xml = Element (node, annotation, List.rev child) in + match ctx with + | Leaf -> + (** Final node: we keep the result in a dummy context *) + context.stack <- Node ("", [xml], 0, Leaf) + | Node (node, child, pos, ctx) -> + context.stack <- Node (node, xml :: child, pos, ctx) + in + + let open Format in + + let ft = formatter_of_buffer pp_buffer in + + let tag_functions = { + mark_open_tag = (fun tag -> let () = open_xml_tag tag in ""); + mark_close_tag = (fun tag -> let () = close_xml_tag tag in ""); + print_open_tag = ignore; + print_close_tag = ignore; + } in + + pp_set_formatter_tag_functions ft tag_functions; + pp_set_mark_tags ft true; + + (* Set formatter width. This is currently a hack and duplicate code + with Pp_control. Hopefully it will be fixed better in Coq 8.7 *) + let w = pp_get_margin str_formatter () in + let m = max (64 * w / 100) (w-30) in + pp_set_margin ft w; + pp_set_max_indent ft m; + + (** The whole output must be a valid document. To that + end, we nest the document inside tags. *) + pp_open_tag ft "pp"; + Pp.(pp_with ~pp_tag ft ppcmds); + pp_close_tag ft (); + + (** Get the resulting XML tree. *) + let () = pp_print_flush ft () in + let () = assert (Buffer.length pp_buffer = 0) in + match context.stack with + | Node ("", [xml], 0, Leaf) -> xml + | _ -> assert false + + +let annotations_positions xml = + let rec node accu = function + | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> + children ((annotation, (startpos, endpos)) :: accu) cs + | Element (_, _, cs) -> + children accu cs + | _ -> + accu + and children accu cs = + List.fold_left node accu cs + in + node [] xml + +let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = + let rec node = function + | Element (index, { annotation; startpos; endpos }, cs) -> + let attributes = + [ "startpos", string_of_int startpos; + "endpos", string_of_int endpos + ] + @ (match annotation with + | None -> [] + | Some annotation -> attributes_of_annotation annotation + ) + in + let tag = + match annotation with + | None -> index + | Some annotation -> tag_of_annotation annotation + in + Element (tag, attributes, List.map node cs) + | PCData s -> + PCData s + in + node xml + +type richpp = xml + +let repr xml = xml +let richpp_of_xml xml = xml +let richpp_of_string s = PCData s + +let richpp_of_pp pp = + let annotate t = Some (Ppstyle.repr t) in + let rec drop = function + | PCData s -> [PCData s] + | Element (_, annotation, cs) -> + let cs = List.concat (List.map drop cs) in + match annotation.annotation with + | None -> cs + | Some s -> [Element (String.concat "." s, [], cs)] + in + let xml = rich_pp annotate pp in + Element ("_", [], drop xml) + +let raw_print xml = + let buf = Buffer.create 1024 in + let rec print = function + | PCData s -> Buffer.add_string buf s + | Element (_, _, cs) -> List.iter print cs + in + let () = print xml in + Buffer.contents buf + diff --git a/ide/richpp.mli b/ide/richpp.mli new file mode 100644 index 0000000000..2e839e996b --- /dev/null +++ b/ide/richpp.mli @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'annotation option) -> Pp.std_ppcmds -> + 'annotation located Xml_datatype.gxml + +(** [annotations_positions ssdoc] returns a list associating each + annotations with its position in the string from which [ssdoc] is + built. *) +val annotations_positions : + 'annotation located Xml_datatype.gxml -> + ('annotation * (int * int)) list + +(** [xml_of_rich_pp ssdoc] returns an XML representation of the + semi-structured document [ssdoc]. *) +val xml_of_rich_pp : + ('annotation -> string) -> + ('annotation -> (string * string) list) -> + 'annotation located Xml_datatype.gxml -> + Xml_datatype.xml + +(** {5 Enriched text} *) + +type richpp +(** Type of text with style annotations *) + +val richpp_of_pp : Pp.std_ppcmds -> richpp +(** Extract style information from formatted text *) + +val richpp_of_xml : Xml_datatype.xml -> richpp +(** Do not use outside of dedicated areas *) + +val richpp_of_string : string -> richpp +(** Make a styled text out of a normal string *) + +val repr : richpp -> Xml_datatype.xml +(** Observe the styled text as XML *) + +(** {5 Debug/Compat} *) + +(** Represent the semi-structured document as a string, dropping any additional + information. *) +val raw_print : richpp -> string diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index d33c0add4a..b83bd107ee 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -103,7 +103,7 @@ object(self) let process = Coq.bind (Coq.query (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> - Ideutils.insert_xml result#buffer str; + Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp str); notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; Coq.return () | Interface.Good res -> diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 0330b8eff1..1cf389c75d 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -28,9 +28,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Richpp.richpp -> unit + method add : Pp.std_ppcmds -> unit method add_string : string -> unit - method set : Richpp.richpp -> unit + method set : Pp.std_ppcmds -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer @@ -79,21 +79,14 @@ let message_view () : message_view = | Feedback.Warning -> [Tags.Message.warning] | _ -> [] in - let rec non_empty = function - | Xml_datatype.PCData "" -> false - | Xml_datatype.PCData _ -> true - | Xml_datatype.Element (_, _, children) -> List.exists non_empty children - in - if non_empty (Richpp.repr msg) then begin - let mark = `MARK mark in - Ideutils.insert_xml ~mark buffer ~tags msg; - buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; - push#call (level, msg) - end + let mark = `MARK mark in + Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp msg); + buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; + push#call (level, msg) method add msg = self#push Feedback.Notice msg - method add_string s = self#add (Richpp.richpp_of_string s) + method add_string s = self#add (Pp.str s) method set msg = self#clear; self#add msg diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 2d34533dee..a71d345a5f 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -18,9 +18,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Richpp.richpp -> unit + method add : Pp.std_ppcmds -> unit method add_string : string -> unit - method set : Richpp.richpp -> unit + method set : Pp.std_ppcmds -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 47c86045a5..72aa9051a0 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -84,7 +84,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with let () = hook_tag_cb tag hint sel_cb on_hover in [tag], hints in - let () = insert_xml ~tags proof#buffer hyp in + let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp hyp) in proof#buffer#insert "\n"; insert_hyp rem_hints hs in @@ -98,13 +98,13 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with else [] in proof#buffer#insert (goal_str 1 goals_cnt); - insert_xml proof#buffer cur_goal; + insert_xml proof#buffer (Richpp.richpp_of_pp cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) let fold_goal i _ { Interface.goal_ccl = g } = proof#buffer#insert (goal_str i goals_cnt); - insert_xml proof#buffer g; + insert_xml proof#buffer (Richpp.richpp_of_pp g); proof#buffer#insert "\n" in let () = Util.List.fold_left_i fold_goal 2 () rem_goals in @@ -144,7 +144,7 @@ let display mode (view : #GText.view_skel) goals hints evars = (* The proof is finished, with the exception of given up goals. *) view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n"; let iter goal = - insert_xml view#buffer goal.Interface.goal_ccl; + insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl); view#buffer#insert "\n" in List.iter iter given_up_goals; @@ -153,7 +153,7 @@ let display mode (view : #GText.view_skel) goals hints evars = (* All the goals have been resolved but those on the shelf. *) view#buffer#insert "All the remaining goals are on the shelf:\n\n"; let iter goal = - insert_xml view#buffer goal.Interface.goal_ccl; + insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl); view#buffer#insert "\n" in List.iter iter shelved_goals @@ -166,7 +166,7 @@ let display mode (view : #GText.view_skel) goals hints evars = view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n"; let iter i goal = let () = view#buffer#insert (goal_str (succ i)) in - insert_xml view#buffer goal.Interface.goal_ccl; + insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl); view#buffer#insert "\n" in List.iteri iter bg diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 65f44fdd38..08f23d3d4e 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -97,6 +97,49 @@ let to_richpp xml = match xml with | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x | x -> raise Serialize.(Marshal_error("richpp",x)) +let of_box (ppb : Pp.block_type) = let open Pp in match ppb with + | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] + | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] + | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] + | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] + +let to_box = let open Pp in + do_match "ppbox" (fun s args -> match s with + | "hbox" -> Pp_hbox (to_int (singleton args)) + | "vbox" -> Pp_vbox (to_int (singleton args)) + | "hvbox" -> Pp_hvbox (to_int (singleton args)) + | "hovbox" -> Pp_hovbox (to_int (singleton args)) + | x -> raise (Marshal_error("*ppbox",PCData x)) + ) + +let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with + | Ppcmd_empty -> constructor "ppdoc" "emtpy" [] + | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] + | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] + | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] + | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair (of_list of_string) of_pp (t,s)] + | Ppcmd_print_break (i,j) + -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] + | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] + | Ppcmd_comment cmd -> constructor "ppdoc" "comment" [of_list of_string cmd] + + +let rec to_pp xpp = let open Pp in + do_match "ppdoc" (fun s args -> match s with + | "empty" -> Ppcmd_empty + | "string" -> Ppcmd_string (to_string (singleton args)) + | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) + | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in + Ppcmd_box(bt,s) + | "tag" -> let (tg,s) = to_pair (to_list to_string) to_pp (singleton args) in + Ppcmd_tag(tg,s) + | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in + Ppcmd_print_break(i, j) + | "newline" -> Ppcmd_force_newline + | "comment" -> Ppcmd_comment (to_list to_string (singleton args)) + | x -> raise (Marshal_error("*ppdoc",PCData x)) + ) xpp + let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) | Fail (id,loc, msg) -> @@ -104,7 +147,7 @@ let of_value f = function | None -> [] | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in let id = of_stateid id in - Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg]) + Element ("value", ["val", "fail"] @ loc, [id; of_pp msg]) let to_value f = function | Element ("value", attrs, l) -> @@ -120,7 +163,7 @@ let to_value f = function 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 + let msg = to_pp msg in Fail (id, loc, msg) else raise (Marshal_error("good or fail",PCData ans)) | x -> raise (Marshal_error("value",x)) @@ -147,15 +190,15 @@ let to_evar = function | x -> raise (Marshal_error("evar",x)) let of_goal g = - let hyp = of_list of_richpp g.goal_hyp in - let ccl = of_richpp g.goal_ccl in + let hyp = of_list of_pp g.goal_hyp in + let ccl = of_pp 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 to_richpp hyp in - let ccl = to_richpp ccl in - let id = to_string id in + let hyp = to_list to_pp hyp in + let ccl = to_pp ccl in + let id = to_string id in { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } | x -> raise (Marshal_error("goal",x)) @@ -344,8 +387,8 @@ end = struct Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals else let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^ - Richpp.raw_print goal ^ "]" in + "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ + Pp.string_of_ppcmds goal ^ "]" in String.concat " " (List.map pr_goal g.fg_goals) let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" let pr_status (s : status) = @@ -701,10 +744,10 @@ let to_call : xml -> unknown_call = let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v - | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]" + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]" | Fail (id,Some(i,j),str) -> "FAIL "^Stateid.to_string id^ - " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]" + " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]" let pr_value v = pr_value_gen (fun _ -> "FIXME") v let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with | Add _ -> pr_value_gen (print add_rty_t ) value @@ -760,7 +803,7 @@ let document to_string_fmt = (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" (to_string_fmt (of_value (fun _ -> PCData "b") - (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message")))); + (Fail (Stateid.initial,Some (15,34), Pp.str "error message")))); document_type_encoding to_string_fmt (* Moved from feedback.mli : This is IDE specific and we don't want to @@ -787,12 +830,12 @@ let to_message_level = let of_message lvl loc msg = let lvl = of_message_level lvl in let xloc = of_option of_loc loc in - let content = of_richpp msg in + let content = of_pp msg in Xml_datatype.Element ("message", [], [lvl; xloc; content]) let to_message xml = match xml with | Xml_datatype.Element ("message", [], [lvl; xloc; content]) -> - Message(to_message_level lvl, to_option to_loc xloc, to_richpp content) + Message(to_message_level lvl, to_option to_loc xloc, to_pp content) | x -> raise (Marshal_error("message",x)) let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index ca911178f5..f6fae24d7c 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -66,5 +66,6 @@ val of_feedback : Feedback.feedback -> xml val to_feedback : xml -> Feedback.feedback val is_feedback : xml -> bool -val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml +val of_message : Feedback.level -> Loc.t option -> Pp.std_ppcmds -> xml +(* val to_message : xml -> Feedback.message *) -- cgit v1.2.3 From 4084ee30293a6013592c0651dfeb1975711f135f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 30 Nov 2016 22:24:17 +0100 Subject: [ide] richpp clenaup We remove the "abstraction breaking" primitives and reduce the file to the used fragment. --- ide/ide_slave.ml | 5 +++-- ide/ideutils.ml | 4 ++-- ide/ideutils.mli | 2 -- ide/richpp.ml | 14 -------------- ide/richpp.mli | 18 ++---------------- ide/xmlprotocol.ml | 5 ----- ide/xmlprotocol.mli | 4 ---- 7 files changed, 7 insertions(+), 45 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 88b61042ed..c77232ad15 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -111,8 +111,9 @@ let annotate phrase = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in Vernac.parse_sentence (pa,None) in - Richpp.repr (Richpp.richpp_of_pp (Ppvernac.pr_vernac ast)) - + (* XXX: Width should be a parameter of annotate... *) + Richpp.richpp_of_pp (Ppvernac.pr_vernac ast) + (** Goal display *) let hyp_next_tac sigma env decl = diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 498a911ee4..101f1a5eee 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -43,7 +43,7 @@ let xml_to_string xml = | Element (_, _, children) -> List.iter iter children in - let () = iter (Richpp.repr xml) in + let () = iter xml in Buffer.contents buf let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = @@ -75,7 +75,7 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let tags = try tag t :: tags with Not_found -> tags in List.iter (fun xml -> insert tags xml) children in - let () = try insert tags (Richpp.repr msg) with _ -> () in + let () = try insert tags msg with _ -> () in buf#delete_mark rmark let set_location = ref (function s -> failwith "not ready") diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 1ae66e23e9..4b4ba72b0b 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -52,8 +52,6 @@ val pop_info : unit -> unit val clear_info : unit -> unit val flash_info : ?delay:int -> string -> unit -val xml_to_string : Richpp.richpp -> string - val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list -> #GText.buffer_skel -> Richpp.richpp -> unit diff --git a/ide/richpp.ml b/ide/richpp.ml index c0128dbc2d..b84c518245 100644 --- a/ide/richpp.ml +++ b/ide/richpp.ml @@ -172,10 +172,6 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = type richpp = xml -let repr xml = xml -let richpp_of_xml xml = xml -let richpp_of_string s = PCData s - let richpp_of_pp pp = let annotate t = Some (Ppstyle.repr t) in let rec drop = function @@ -188,13 +184,3 @@ let richpp_of_pp pp = in let xml = rich_pp annotate pp in Element ("_", [], drop xml) - -let raw_print xml = - let buf = Buffer.create 1024 in - let rec print = function - | PCData s -> Buffer.add_string buf s - | Element (_, _, cs) -> List.iter print cs - in - let () = print xml in - Buffer.contents buf - diff --git a/ide/richpp.mli b/ide/richpp.mli index 2e839e996b..980d27407f 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -42,23 +42,9 @@ val xml_of_rich_pp : (** {5 Enriched text} *) -type richpp +type richpp = Xml_datatype.xml + (** Type of text with style annotations *) val richpp_of_pp : Pp.std_ppcmds -> richpp (** Extract style information from formatted text *) - -val richpp_of_xml : Xml_datatype.xml -> richpp -(** Do not use outside of dedicated areas *) - -val richpp_of_string : string -> richpp -(** Make a styled text out of a normal string *) - -val repr : richpp -> Xml_datatype.xml -(** Observe the styled text as XML *) - -(** {5 Debug/Compat} *) - -(** Represent the semi-structured document as a string, dropping any additional - information. *) -val raw_print : richpp -> string diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 08f23d3d4e..6ed62082d7 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -92,11 +92,6 @@ let to_stateid = function 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_box (ppb : Pp.block_type) = let open Pp in match ppb with | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index f6fae24d7c..43a65dfa85 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -57,10 +57,6 @@ 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 -- cgit v1.2.3 From 6885a398229918865378ea24f07d93d2bcdd2802 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 30 Sep 2016 09:43:31 +0200 Subject: [ide] Dynamic printing width. The IDE now gets core Coq's `std_ppcmds` document format which is width-independent. Thus, we follow [1] and make the `{proof,message}_view` object refresh their contents when the container widget changes size (by listening to GTK's `size_allocated` signal). The practical advantage is that now CoqIDE always renders terms with the proper printing width set and without a roundtrip to Coq. This patch dispenses the need for the `printing width` option, which could be removed altogether. [1] http://stackoverflow.com/questions/40854571/change-gtksourceview-contents-on-resize/ --- ide/coq.ml | 7 ------ ide/coq.mli | 1 - ide/coqOps.ml | 1 - ide/ide_slave.ml | 2 +- ide/richpp.ml | 16 +++++++------- ide/richpp.mli | 11 ++++++---- ide/wg_Command.ml | 5 +++-- ide/wg_MessageView.ml | 59 +++++++++++++++++++++++++++++++++++++++----------- ide/wg_MessageView.mli | 1 + ide/wg_ProofView.ml | 29 ++++++++++++++----------- ide/wg_ProofView.mli | 1 - 11 files changed, 82 insertions(+), 51 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index e2036beee3..bb9d6e5228 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -549,18 +549,11 @@ struct let _ = reset () - (** Integer option *) - - let width = ["Printing"; "Width"] - let width_state = ref None - let set_printing_width w = width_state := Some w - (** Transmitting options to coqtop *) let enforce h k = let mkopt o v acc = (o, Interface.BoolValue v) :: acc in let opts = Hashtbl.fold mkopt current_state [] in - let opts = (width, Interface.IntValue !width_state) :: opts in eval_call (Xmlprotocol.set_options opts) h (function | Interface.Good () -> k () diff --git a/ide/coq.mli b/ide/coq.mli index f2876de246..ab8c12a6f1 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -139,7 +139,6 @@ sig val bool_items : bool_descr list val set : t -> bool -> unit - val set_printing_width : int -> unit (** [enforce] transmits to coq the current option values. It is also called by [goals] and [evars] above. *) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 7982ffc8b8..cee243f91f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -340,7 +340,6 @@ object(self) buffer#get_iter_at_mark `INSERT method private show_goals_aux ?(move_insert=false) () = - Coq.PrintOpt.set_printing_width proof#width; if move_insert then begin let dest = self#get_start_of_input in if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index c77232ad15..e3e1a88903 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -112,7 +112,7 @@ let annotate phrase = Vernac.parse_sentence (pa,None) in (* XXX: Width should be a parameter of annotate... *) - Richpp.richpp_of_pp (Ppvernac.pr_vernac ast) + Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) (** Goal display *) diff --git a/ide/richpp.ml b/ide/richpp.ml index b84c518245..515090f713 100644 --- a/ide/richpp.ml +++ b/ide/richpp.ml @@ -38,7 +38,7 @@ type 'a context = { marking functions. As those functions are called when actually writing to the device, the resulting tree is correct. *) -let rich_pp annotate ppcmds = +let rich_pp width annotate ppcmds = let context = { stack = Leaf; @@ -113,12 +113,12 @@ let rich_pp annotate ppcmds = pp_set_formatter_tag_functions ft tag_functions; pp_set_mark_tags ft true; - (* Set formatter width. This is currently a hack and duplicate code - with Pp_control. Hopefully it will be fixed better in Coq 8.7 *) - let w = pp_get_margin str_formatter () in - let m = max (64 * w / 100) (w-30) in - pp_set_margin ft w; + (* Setting the formatter *) + pp_set_margin ft width; + let m = max (64 * width / 100) (width-30) in pp_set_max_indent ft m; + pp_set_max_boxes ft 50 ; + pp_set_ellipsis_text ft "..."; (** The whole output must be a valid document. To that end, we nest the document inside tags. *) @@ -172,7 +172,7 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = type richpp = xml -let richpp_of_pp pp = +let richpp_of_pp width pp = let annotate t = Some (Ppstyle.repr t) in let rec drop = function | PCData s -> [PCData s] @@ -182,5 +182,5 @@ let richpp_of_pp pp = | None -> cs | Some s -> [Element (String.concat "." s, [], cs)] in - let xml = rich_pp annotate pp in + let xml = rich_pp width annotate pp in Element ("_", [], drop xml) diff --git a/ide/richpp.mli b/ide/richpp.mli index 980d27407f..0ceeeefc29 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -16,12 +16,15 @@ type 'annotation located = { endpos : int } -(** [rich_pp get_annotations ppcmds] returns the interpretation +(* XXX: The width parameter should be moved to a `formatter_property` + record shared with Topfmt *) + +(** [rich_pp width get_annotations ppcmds] returns the interpretation of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired - annotation. *) -val rich_pp : + annotation. [width] sets the printing witdh of the formatter. *) +val rich_pp : int -> (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds -> 'annotation located Xml_datatype.gxml @@ -46,5 +49,5 @@ type richpp = Xml_datatype.xml (** Type of text with style annotations *) -val richpp_of_pp : Pp.std_ppcmds -> richpp +val richpp_of_pp : int -> Pp.std_ppcmds -> richpp (** Extract style information from formatted text *) diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index b83bd107ee..47dad8f196 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -103,11 +103,12 @@ object(self) let process = Coq.bind (Coq.query (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> - Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp str); + let width = Ideutils.textview_width result in + Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str); notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; Coq.return () | Interface.Good res -> - result#buffer#insert res; + result#buffer#insert res; notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce; Coq.return ()) in diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 1cf389c75d..3d0cd46cd4 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -31,6 +31,7 @@ class type message_view = method add : Pp.std_ppcmds -> unit method add_string : string -> unit method set : Pp.std_ppcmds -> unit + method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer @@ -57,31 +58,58 @@ let message_view () : message_view = let () = view#set_left_margin 2 in view#misc#show (); let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed cb in - let _ = view#misc#connect#realize (fun () -> cb background_color#get) in + let _ = background_color#connect#changed ~callback:cb in + let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in stick text_font view cb; - object (self) + + (* Inserts at point, advances the mark *) + let insert_msg (level, msg) = + let tags = match level with + | Feedback.Error -> [Tags.Message.error] + | Feedback.Warning -> [Tags.Message.warning] + | _ -> [] + in + let mark = `MARK mark in + let width = Ideutils.textview_width view in + Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp width msg); + buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n" + in + + let mv = object (self) inherit GObj.widget box#as_widget + (* List of displayed messages *) + val mutable last_width = -1 + val mutable msgs = [] + val push = new GUtil.signal () method connect = new message_view_signals_impl box#as_widget push + method refresh force = + (* We need to block updates here due to the following race: + insertion of messages may create a vertical scrollbar, this + will trigger a width change, calling refresh again and + going into an infinite loop. *) + let width = Ideutils.textview_width view in + (* Could still this method race if the scrollbar changes the + textview_width ?? *) + let needed = force || last_width <> width in + if needed then begin + last_width <- width; + buffer#set_text ""; + buffer#move_mark (`MARK mark) ~where:buffer#start_iter; + List.(iter insert_msg (rev msgs)) + end + method clear = - buffer#set_text ""; - buffer#move_mark (`MARK mark) ~where:buffer#start_iter + msgs <- []; self#refresh true method push level msg = - let tags = match level with - | Feedback.Error -> [Tags.Message.error] - | Feedback.Warning -> [Tags.Message.warning] - | _ -> [] - in - let mark = `MARK mark in - Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp msg); - buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; + msgs <- (level, msg) :: msgs; + insert_msg (level, msg); push#call (level, msg) method add msg = self#push Feedback.Notice msg @@ -93,3 +121,8 @@ let message_view () : message_view = method buffer = text_buffer end + in + (* Is there a better way to connect the signal ? *) + let w_cb (_ : Gtk.rectangle) = mv#refresh false in + ignore (view#misc#connect#size_allocate ~callback:w_cb); + mv diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index a71d345a5f..d065fcbc80 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -21,6 +21,7 @@ class type message_view = method add : Pp.std_ppcmds -> unit method add_string : string -> unit method set : Pp.std_ppcmds -> unit + method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 72aa9051a0..b5405570c9 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -18,7 +18,6 @@ class type proof_view = method clear : unit -> unit method set_goals : Interface.goals option -> unit method set_evars : Interface.evar list option -> unit - method width : int end (* tag is the tag to be hooked, item is the item covered by this tag, make_menu @@ -74,6 +73,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with | None -> [], [] | Some (hl, h) -> (hl, h) in + let width = Ideutils.textview_width proof in let rec insert_hyp hints hs = match hs with | [] -> () | hyp :: hs -> @@ -84,7 +84,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with let () = hook_tag_cb tag hint sel_cb on_hover in [tag], hints in - let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp hyp) in + let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp width hyp) in proof#buffer#insert "\n"; insert_hyp rem_hints hs in @@ -98,13 +98,13 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with else [] in proof#buffer#insert (goal_str 1 goals_cnt); - insert_xml proof#buffer (Richpp.richpp_of_pp cur_goal); + insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) let fold_goal i _ { Interface.goal_ccl = g } = proof#buffer#insert (goal_str i goals_cnt); - insert_xml proof#buffer (Richpp.richpp_of_pp g); + insert_xml proof#buffer (Richpp.richpp_of_pp width g); proof#buffer#insert "\n" in let () = Util.List.fold_left_i fold_goal 2 () rem_goals in @@ -122,6 +122,7 @@ let rec flatten = function let display mode (view : #GText.view_skel) goals hints evars = let () = view#buffer#set_text "" in + let width = Ideutils.textview_width view in match goals with | None -> () (* No proof in progress *) @@ -144,7 +145,7 @@ let display mode (view : #GText.view_skel) goals hints evars = (* The proof is finished, with the exception of given up goals. *) view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n"; let iter goal = - insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl); + insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl); view#buffer#insert "\n" in List.iter iter given_up_goals; @@ -153,7 +154,7 @@ let display mode (view : #GText.view_skel) goals hints evars = (* All the goals have been resolved but those on the shelf. *) view#buffer#insert "All the remaining goals are on the shelf:\n\n"; let iter goal = - insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl); + insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl); view#buffer#insert "\n" in List.iter iter shelved_goals @@ -166,7 +167,7 @@ let display mode (view : #GText.view_skel) goals hints evars = view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n"; let iter i goal = let () = view#buffer#insert (goal_str (succ i)) in - insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl); + insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl); view#buffer#insert "\n" in List.iteri iter bg @@ -192,7 +193,7 @@ let proof_view () = let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in stick text_font view cb; - object + let pf = object inherit GObj.widget view#as_widget val mutable goals = None val mutable evars = None @@ -207,9 +208,11 @@ let proof_view () = method refresh () = let dummy _ () = () in - display (mode_tactic dummy) (view :> GText.view_skel) goals None evars - - method width = Ideutils.textview_width (view :> GText.view_skel) + display (mode_tactic dummy) view goals None evars end - -(* ignore (proof_buffer#add_selection_clipboard cb); *) + in + (* Is there a better way to connect the signal ? *) + (* Can this be done in the object constructor? *) + let w_cb _ = pf#refresh () in + ignore (view#misc#connect#size_allocate w_cb); + pf diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index b6eae48b39..aa01d955d0 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -14,7 +14,6 @@ class type proof_view = method clear : unit -> unit method set_goals : Interface.goals option -> unit method set_evars : Interface.evar list option -> unit - method width : int end val proof_view : unit -> proof_view -- cgit v1.2.3 From a8ec2dc5c330ded1ba400ef202c57e68d2533312 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 5 Dec 2016 18:17:46 +0100 Subject: [pp] Remove special tag type and handler from Pp. For legacy reasons, pretty printing required to provide a "tag" interpretation function `pp_tag`. However such function was not of much use as the backends (richpp and terminal) hooked at the `Format.tag` level. We thus remove this unused indirection layer and annotate expressions with their `Format` tags. This is a step towards moving the last bit of terminal code out of the core system. --- ide/richpp.ml | 29 +++++------------------------ ide/richpp.mli | 4 +--- ide/xmlprotocol.ml | 4 ++-- 3 files changed, 8 insertions(+), 29 deletions(-) (limited to 'ide') diff --git a/ide/richpp.ml b/ide/richpp.ml index 515090f713..ecf1f40211 100644 --- a/ide/richpp.ml +++ b/ide/richpp.ml @@ -24,10 +24,6 @@ type 'a context = { (** Pending opened nodes *) mutable offset : int; (** Quantity of characters printed so far *) - mutable annotations : 'a option Int.Map.t; - (** Map associating annotations to indexes *) - mutable index : int; - (** Current index of annotations *) } (** We use Format to introduce tags inside the pretty-printed document. @@ -38,23 +34,13 @@ type 'a context = { marking functions. As those functions are called when actually writing to the device, the resulting tree is correct. *) -let rich_pp width annotate ppcmds = +let rich_pp width ppcmds = let context = { stack = Leaf; offset = 0; - annotations = Int.Map.empty; - index = (-1); } in - let pp_tag obj = - let index = context.index + 1 in - let () = context.index <- index in - let obj = annotate obj in - let () = context.annotations <- Int.Map.add index obj context.annotations in - string_of_int index - in - let pp_buffer = Buffer.create 180 in let push_pcdata () = @@ -81,12 +67,8 @@ let rich_pp width annotate ppcmds = | Leaf -> assert false | Node (node, child, pos, ctx) -> let () = assert (String.equal tag node) in - let annotation = - try Int.Map.find (int_of_string node) context.annotations - with _ -> None - in let annotation = { - annotation = annotation; + annotation = Some tag; startpos = pos; endpos = context.offset; } in @@ -123,7 +105,7 @@ let rich_pp width annotate ppcmds = (** The whole output must be a valid document. To that end, we nest the document inside tags. *) pp_open_tag ft "pp"; - Pp.(pp_with ~pp_tag ft ppcmds); + Pp.(pp_with ft ppcmds); pp_close_tag ft (); (** Get the resulting XML tree. *) @@ -173,14 +155,13 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = type richpp = xml let richpp_of_pp width pp = - let annotate t = Some (Ppstyle.repr t) in let rec drop = function | PCData s -> [PCData s] | Element (_, annotation, cs) -> let cs = List.concat (List.map drop cs) in match annotation.annotation with | None -> cs - | Some s -> [Element (String.concat "." s, [], cs)] + | Some s -> [Element (s, [], cs)] in - let xml = rich_pp width annotate pp in + let xml = rich_pp width pp in Element ("_", [], drop xml) diff --git a/ide/richpp.mli b/ide/richpp.mli index 0ceeeefc29..0fe4315b7a 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -24,9 +24,7 @@ type 'annotation located = { that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired annotation. [width] sets the printing witdh of the formatter. *) -val rich_pp : int -> - (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds -> - 'annotation located Xml_datatype.gxml +val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 6ed62082d7..1d50aed032 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -112,7 +112,7 @@ let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] - | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair (of_list of_string) of_pp (t,s)] + | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair of_string of_pp (t,s)] | Ppcmd_print_break (i,j) -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] @@ -126,7 +126,7 @@ let rec to_pp xpp = let open Pp in | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in Ppcmd_box(bt,s) - | "tag" -> let (tg,s) = to_pair (to_list to_string) to_pp (singleton args) in + | "tag" -> let (tg,s) = to_pair to_string to_pp (singleton args) in Ppcmd_tag(tg,s) | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in Ppcmd_print_break(i, j) -- cgit v1.2.3 From 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 5 Dec 2016 17:56:22 +0100 Subject: [pp] Move terminal-specific tagging to the toplevel. Previously, tags were associated to terminal styles, which doesn't make sense on terminal-free pretty printing scenarios. This commit moves tag interpretation to the toplevel terminal handling module `Topfmt`. --- ide/richpp.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/richpp.mli b/ide/richpp.mli index 0fe4315b7a..ea4b189ba8 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -19,7 +19,7 @@ type 'annotation located = { (* XXX: The width parameter should be moved to a `formatter_property` record shared with Topfmt *) -(** [rich_pp width get_annotations ppcmds] returns the interpretation +(** [rich_pp width ppcmds] returns the interpretation of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired -- cgit v1.2.3 From 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Dec 2016 12:12:54 +0100 Subject: [pp] [ide] Minor cleanups in pp code. - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics. --- ide/coqOps.ml | 30 +++++++++++++++++------------- ide/ideutils.ml | 2 +- ide/minilib.ml | 6 ++++-- ide/minilib.mli | 3 ++- 4 files changed, 24 insertions(+), 17 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index cee243f91f..1b4c5d3be0 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -128,6 +128,9 @@ end = struct end open SentenceId +let log_pp msg : unit task = + Coq.lift (fun () -> Minilib.log_pp msg) + let log msg : unit task = Coq.lift (fun () -> Minilib.log msg) @@ -308,7 +311,7 @@ object(self) method private print_stack = Minilib.log "document:"; - Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer))) + Minilib.log_pp (Doc.print document (dbg_to_string buffer)) method private enter_focus start stop = let at id id' _ = Stateid.equal id' id in @@ -379,8 +382,7 @@ object(self) Coq.bind (Coq.seq action query) next method private mark_as_needed sentence = - Minilib.log("Marking " ^ - Pp.string_of_ppcmds (dbg_to_string buffer false None sentence)); + Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence); let start = buffer#get_iter_at_mark sentence.start in let stop = buffer#get_iter_at_mark sentence.stop in let to_process = Tags.Script.to_process in @@ -437,9 +439,11 @@ object(self) | _ -> None in try Some (Doc.find_map document finder) with Not_found -> None in - let log s state_id = - Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string - (Option.default Stateid.dummy state_id)) in + let log_pp s state_id = + Minilib.log_pp Pp.(seq + [str "Feedback "; s; str " on "; + str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in + let log s state_id = log_pp (Pp.str s) state_id in begin match msg.contents, sentence with | AddedAxiom, Some (id,sentence) -> log "AddedAxiom" id; @@ -469,24 +473,24 @@ object(self) (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let msg = Pp.string_of_ppcmds msg in - log "ErrorMsg" id; + log_pp Pp.(str "ErrorMsg" ++ msg) id; remove_flag sentence `PROCESSING; - add_flag sentence (`ERROR (loc, msg)); + let rmsg = Pp.string_of_ppcmds msg in + add_flag sentence (`ERROR (loc, rmsg)); self#mark_as_needed sentence; - self#attach_tooltip sentence loc msg; + self#attach_tooltip sentence loc rmsg; if not (Loc.is_ghost loc) then self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) | Message(Warning, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let rmsg = Pp.string_of_ppcmds msg in - log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id; + log_pp Pp.(str "WarningMsg" ++ msg) id; + let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`WARNING (loc, rmsg)); self#attach_tooltip sentence loc rmsg; self#position_warning_tag_at_sentence sentence loc; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> - log ("Msg: " ^ Pp.string_of_ppcmds msg) id; + log_pp Pp.(str "Msg" ++ msg) id; messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 101f1a5eee..da867e689e 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -337,7 +337,7 @@ let default_logger level message = | Feedback.Warning -> `WARNING | Feedback.Error -> `ERROR in - Minilib.log ~level (Pp.string_of_ppcmds message) + Minilib.log_pp ~level message (** {6 File operations} *) diff --git a/ide/minilib.ml b/ide/minilib.ml index d11e8c56b2..2c24e46f8f 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -30,7 +30,7 @@ let debug = ref false print in the response buffer. *) -let log ?(level = `DEBUG) msg = +let log_pp ?(level = `DEBUG) msg = let prefix = match level with | `DEBUG -> "DEBUG" | `INFO -> "INFO" @@ -40,10 +40,12 @@ let log ?(level = `DEBUG) msg = | `FATAL -> "FATAL" in if !debug then begin - try Printf.eprintf "[%s] %s\n%!" prefix msg + try Format.eprintf "[%s] @[%a@]\n%!" prefix Pp.pp_with msg with _ -> () end +let log ?level str = log_pp ?level (Pp.str str) + let coqify d = Filename.concat d "coq" let coqide_config_home () = diff --git a/ide/minilib.mli b/ide/minilib.mli index b7672c9002..4517a23744 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,7 +22,8 @@ type level = [ (** debug printing *) val debug : bool ref -val log : ?level:level -> string -> unit +val log_pp : ?level:level -> Pp.std_ppcmds -> unit +val log : ?level:level -> string -> unit val coqide_config_home : unit -> string val coqide_config_dirs : unit -> string list -- cgit v1.2.3 From 921ea3983d45051ae85b0e20bf13de2eff38e53e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 8 Feb 2017 18:13:25 +0100 Subject: [pp] Remove uses of expensive string_of_ppcmds. In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself. --- ide/ide_slave.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index e3e1a88903..2065a45467 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -255,7 +255,7 @@ let status force = let export_coq_object t = { Interface.coq_object_prefix = t.Search.coq_object_prefix; Interface.coq_object_qualid = t.Search.coq_object_qualid; - Interface.coq_object_object = t.Search.coq_object_object + Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object) } let pattern_of_string ?env s = -- cgit v1.2.3 From 829a8feb3d02da057d39b5029b422e8a45dd1608 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Jan 2017 14:39:29 +0100 Subject: [xml] Restore protocol compatibility with 8.6. By default, we serialize messages to the "rich printing representation" as it was done in 8.6, this ways clients don't have to adapt unless they specifically request the new format using option `--xml_format=Ppcmds` --- ide/coq.ml | 2 +- ide/ide.mllib | 1 + ide/ide_slave.ml | 19 ++++++++++++++----- ide/xmlprotocol.ml | 17 +++++++++++++++++ ide/xmlprotocol.mli | 14 ++++++++------ 5 files changed, 41 insertions(+), 12 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index bb9d6e5228..3a1d877872 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -366,7 +366,7 @@ let bind_self_as f = (** This launches a fresh handle from its command line arguments. *) let spawn_handle args respawner feedback_processor = let prog = coqtop_path () in - let args = Array.of_list ("-async-proofs" :: "on" :: "-ideslave" :: args) in + let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: "on" :: "-ideslave" :: args) in let env = match !Flags.ideslave_coqtop_flags with | None -> None diff --git a/ide/ide.mllib b/ide/ide.mllib index 12170c4621..78b4c01e8c 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -14,6 +14,7 @@ Xml_parser Xml_printer Serialize Richpp +Topfmt Xmlprotocol Ideutils Coq diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 2065a45467..db450b4bc8 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -441,8 +441,8 @@ let print_xml = try Xml_printer.print oc xml; Mutex.unlock m with e -> let e = CErrors.push e in Mutex.unlock m; iraise e -let slave_feeder xml_oc msg = - let xml = Xmlprotocol.of_feedback msg in +let slave_feeder fmt xml_oc msg = + let xml = Xmlprotocol.(of_feedback fmt msg) in print_xml xml_oc xml (** The main loop *) @@ -451,6 +451,11 @@ let slave_feeder xml_oc msg = messages by [handle_exn] above. Otherwise, we die badly, without trying to answer malformed requests. *) +let msg_format = ref (fun () -> + let margin = Option.default 72 (Topfmt.get_margin ()) in + Xmlprotocol.Richpp margin +) + let loop () = init_signal_handler (); catch_break := false; @@ -461,7 +466,7 @@ let loop () = (* SEXP parser make *) let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in - Feedback.add_feeder (slave_feeder xml_oc); + ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc)); (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; Vernacentries.qed_display_script := false; @@ -474,7 +479,7 @@ let loop () = let r = eval_call 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); + print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r); flush out_ch with | Xml_parser.Error (Xml_parser.Empty, _) -> @@ -496,6 +501,8 @@ let loop () = let rec parse = function | "--help-XML-protocol" :: rest -> Xmlprotocol.document Xml_printer.to_string_fmt; exit 0 + | "--xml_format=Ppcmds" :: rest -> + msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest | x :: rest -> x :: parse rest | [] -> [] @@ -507,4 +514,6 @@ let () = Coqtop.toploop_init := (fun args -> let () = Coqtop.toploop_run := loop -let () = Usage.add_to_usage "coqidetop" " --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" +let () = Usage.add_to_usage "coqidetop" +" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format + --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 1d50aed032..b4f2ad0bef 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -12,6 +12,9 @@ let protocol_version = "20150913" +type msg_format = Richpp of int | Ppcmds +let msg_format = ref (Richpp 72) + (** * Interface of calls to Coq by CoqIde *) open Util @@ -135,6 +138,14 @@ let rec to_pp xpp = let open Pp in | x -> raise (Marshal_error("*ppdoc",PCData x)) ) xpp +let of_richpp x = Element ("richpp", [], [x]) + +(* Run-time Selectable *) +let of_pp (pp : Pp.std_ppcmds) = + match !msg_format with + | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) + | Ppcmds -> of_pp pp + let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) | Fail (id,loc, msg) -> @@ -669,6 +680,9 @@ let of_answer : type a. a call -> a value -> xml = function | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) | Annotate _ -> of_value (of_value_type annotate_rty_t ) +let of_answer msg_fmt = + msg_format := msg_fmt; of_answer + let to_answer : type a. a call -> xml -> a value = function | Add _ -> to_value (to_value_type add_rty_t ) | Edit_at _ -> to_value (to_value_type edit_at_rty_t ) @@ -902,6 +916,9 @@ let of_feedback msg = let route = string_of_int msg.route in Element ("feedback", obj @ ["route",route], [id;content]) +let of_feedback msg_fmt = + msg_format := msg_fmt; of_feedback + let to_feedback xml = match xml with | Element ("feedback", ["object","edit";"route",route], [id;content]) -> { id = Edit(to_edit_id id); diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 43a65dfa85..9cefab517f 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -40,12 +40,17 @@ val abstract_eval_call : handler -> 'a call -> 'a value val protocol_version : string +(** By default, we still output messages in Richpp so we are + compatible with 8.6, however, 8.7 aware clients will want to + set this to Ppcmds *) +type msg_format = Richpp of int | Ppcmds + (** * XML data marshalling *) val of_call : 'a call -> xml val to_call : xml -> unknown_call -val of_answer : 'a call -> 'a value -> xml +val of_answer : msg_format -> 'a call -> 'a value -> xml val to_answer : 'a call -> xml -> 'a value (* Prints the documentation of this module *) @@ -58,10 +63,7 @@ val pr_value : 'a value -> string val pr_full_value : 'a call -> 'a value -> string (** * Serializaiton of feedback *) -val of_feedback : Feedback.feedback -> xml +val of_feedback : msg_format -> Feedback.feedback -> xml val to_feedback : xml -> Feedback.feedback -val is_feedback : xml -> bool - -val of_message : Feedback.level -> Loc.t option -> Pp.std_ppcmds -> xml -(* val to_message : xml -> Feedback.message *) +val is_feedback : xml -> bool -- cgit v1.2.3 From 66a245d8055923f8807ae42ed938c1d992051749 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 9 Feb 2017 03:12:18 +0100 Subject: [pp] Fix bug in richpp Format use. Format requires a top-level box to be present, this is similar to the fix done in `Pp.string_of_ppcmds`. --- ide/richpp.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'ide') diff --git a/ide/richpp.ml b/ide/richpp.ml index ecf1f40211..522a3e0b31 100644 --- a/ide/richpp.ml +++ b/ide/richpp.ml @@ -104,9 +104,11 @@ let rich_pp width ppcmds = (** The whole output must be a valid document. To that end, we nest the document inside tags. *) + pp_open_box ft 0; pp_open_tag ft "pp"; Pp.(pp_with ft ppcmds); pp_close_tag ft (); + pp_close_box ft (); (** Get the resulting XML tree. *) let () = pp_print_flush ft () in -- cgit v1.2.3 From fb04bc5cae0d648c379b9eb44f8b515f8e15b854 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 17 Mar 2017 18:12:03 +0100 Subject: [pp] Hide the internal representation of `std_ppcmds`. Following a suggestion by @ppedrot in #390, we require `Pp` clients to be aware that they are using a "view" on the `std_ppcmds` type. This is not extremely useful as people caring about the documents will indeed have to follow changes in the view, but it costs little to play on the safe side here for now. We also introduce a more standard notation, `Pp.t` for the main type. --- ide/coqOps.ml | 2 +- ide/xmlprotocol.ml | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 1b4c5d3be0..4a1d688f51 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -166,7 +166,7 @@ let flags_to_color f = else `NAME Preferences.processed_color#get (* Move to utils? *) -let rec validate (s : Pp.std_ppcmds) = match s with +let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with | Pp.Ppcmd_empty | Pp.Ppcmd_print_break _ | Pp.Ppcmd_force_newline -> true diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index b4f2ad0bef..5f80d68974 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -110,7 +110,7 @@ let to_box = let open Pp in | x -> raise (Marshal_error("*ppbox",PCData x)) ) -let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with +let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with | Ppcmd_empty -> constructor "ppdoc" "emtpy" [] | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] @@ -123,6 +123,7 @@ let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with let rec to_pp xpp = let open Pp in + Pp.unrepr @@ do_match "ppdoc" (fun s args -> match s with | "empty" -> Ppcmd_empty | "string" -> Ppcmd_string (to_string (singleton args)) -- cgit v1.2.3 From aa9e94275ccac92311a6bdac563b61a6c7876cec Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 17 Mar 2017 20:27:44 +0100 Subject: [ide protocol] Add comment about leftover parameter. We try to address @silene 's concerns, which indeed are legitimate. --- ide/ide_slave.ml | 27 +++++++++++++++++++++++++++ ide/interface.mli | 16 ++++++++++++---- 2 files changed, 39 insertions(+), 4 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index db450b4bc8..2ec79dc585 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -97,6 +97,15 @@ let coqide_cmd_checks (loc,ast) = let add ((s,eid),(sid,verbose)) = let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in + (* TODO: the "" parameter is a leftover of the times the protocol + * used to include stderr/stdout output. + * + * Currently, we force all the output meant for the to go via the + * feedback mechanism, and we don't manipulate stderr/stdout, which + * are left to the client's discrection. The parameter is still there + * as not to break the core protocol for this minor change, but it should + * be removed in the next version of the protocol. + *) newid, (rc, "") let edit_at id = @@ -104,6 +113,15 @@ let edit_at id = | `NewTip -> CSig.Inl () | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip)) +(* TODO: the "" parameter is a leftover of the times the protocol + * used to include stderr/stdout output. + * + * Currently, we force all the output meant for the to go via the + * feedback mechanism, and we don't manipulate stderr/stdout, which + * are left to the client's discrection. The parameter is still there + * as not to break the core protocol for this minor change, but it should + * be removed in the next version of the protocol. + *) let query (s,id) = Stm.query ~at:id s; "" let annotate phrase = @@ -379,6 +397,15 @@ let interp ((_raw, verbose), s) = | Some ast -> ast) () in Stm.interp verbose (vernac_parse s); + (* TODO: the "" parameter is a leftover of the times the protocol + * used to include stderr/stdout output. + * + * Currently, we force all the output meant for the to go via the + * feedback mechanism, and we don't manipulate stderr/stdout, which + * are left to the client's discrection. The parameter is still there + * as not to break the core protocol for this minor change, but it should + * be removed in the next version of the protocol. + *) Stm.get_current_state (), CSig.Inl "" (** When receiving the Quit call, we don't directly do an [exit 0], diff --git a/ide/interface.mli b/ide/interface.mli index 43446f3918..9ed6062588 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -127,9 +127,13 @@ type ('a, 'b) union = ('a, 'b) Util.union (** [add ((s,eid),(sid,v))] adds the phrase [s] with edit id [eid] on top of the current edit position (that is asserted to be [sid]) verbosely if [v] is true. The response [(id,(rc,s)] is the new state - [id] assigned to the phrase, some output [s]. [rc] is [Inl] if the new + [id] assigned to the phrase. [rc] is [Inl] if the new state id is the tip of the edit point, or [Inr tip] if the new phrase - closes a focus and [tip] is the new edit tip *) + closes a focus and [tip] is the new edit tip + + [s] used to contain Coq's console output and has been deprecated + in favor of sending feedback, it will be removed in a future + version of the protocol. *) type add_sty = (string * edit_id) * (state_id * verbose) type add_rty = state_id * ((unit, state_id) union * string) @@ -142,8 +146,12 @@ type add_rty = state_id * ((unit, state_id) union * string) type edit_at_sty = state_id type edit_at_rty = (unit, state_id * (state_id * state_id)) union -(** [query s id] executes [s] at state [id] and does not record any state - change but for the printings that are sent in response *) +(** [query s id] executes [s] at state [id]. + + query used to reply with the contents of Coq's console output, and + has been deprecated in favor of sending the query answers as + feedback. It will be removed in a future version of the protocol. +*) type query_sty = string * state_id type query_rty = string -- cgit v1.2.3 From 8c42932d1788c8924844d8fa22419f6fb4401030 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 22 Mar 2017 14:50:23 -0400 Subject: make check not CoqIDE-specific --- ide/ide_slave.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 2ec79dc585..8cadf1a263 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -79,23 +79,23 @@ let is_undo cmd = match cmd with | VernacUndo _ | VernacUndoTo _ -> true | _ -> false -(** Check whether a command is forbidden by CoqIDE *) +(** Check whether a command is forbidden in the IDE *) -let coqide_cmd_checks (loc,ast) = +let ide_cmd_checks (loc,ast) = let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in if is_debug ast then - user_error "Debug mode not available within CoqIDE"; + user_error "Debug mode not available in the IDE"; if is_known_option ast then - Feedback.msg_warning (strbrk"This will not work. Use CoqIDE view menu instead"); + Feedback.msg_warning (strbrk "Set this option from the IDE menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then - Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead"); + Feedback.msg_warning (strbrk "Use IDE navigation instead"); if is_query ast then Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts") (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in + let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. -- cgit v1.2.3