diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 24 | ||||
| -rw-r--r-- | ide/coqide_WIN32.ml.in | 3 | ||||
| -rw-r--r-- | ide/idetop.ml | 20 | ||||
| -rw-r--r-- | ide/ideutils.ml | 69 | ||||
| -rw-r--r-- | ide/ideutils.mli | 16 | ||||
| -rw-r--r-- | ide/session.ml | 2 | ||||
| -rw-r--r-- | ide/wg_MessageView.ml | 6 | ||||
| -rw-r--r-- | ide/wg_MessageView.mli | 1 | ||||
| -rw-r--r-- | ide/wg_ProofView.ml | 6 | ||||
| -rw-r--r-- | ide/wg_ProofView.mli | 1 |
10 files changed, 125 insertions, 23 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index fddc294f68..ab2a17798e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -787,25 +787,28 @@ let coqtop_arguments sn = let dialog = GWindow.dialog ~title:"Coqtop arguments" () in let coqtop = sn.coqtop in (* Text entry *) - let args = Coq.get_arguments coqtop in - let text = String.concat " " args in + let text = Ideutils.encode_string_list (Coq.get_arguments coqtop) in let entry = GEdit.entry ~text ~packing:dialog#vbox#add () in (* Buttons *) let box = dialog#action_area in let ok = GButton.button ~stock:`OK ~packing:box#add () in + let fail s = + let msg = Printf.sprintf "Invalid arguments: %s" s in + let () = sn.messages#default_route#clear in + sn.messages#default_route#push Feedback.Error (Pp.str msg) in let ok_cb () = - let nargs = String.split_on_char ' ' entry#text in - if nargs <> args then + let ntext = entry#text in + if ntext <> text then + match try Util.Inr (Ideutils.decode_string_list ntext) with Failure s -> Util.Inl s with + | Util.Inl s -> fail s + | Util.Inr nargs -> let failed = Coq.filter_coq_opts nargs in match failed with | [] -> let () = Coq.set_arguments coqtop nargs in dialog#destroy () | args -> - let args = String.concat " " args in - let msg = Printf.sprintf "Invalid arguments: %s" args in - let () = sn.messages#default_route#clear in - sn.messages#default_route#push Feedback.Error (Pp.str msg) + fail (String.concat " " args) else dialog#destroy () in let _ = entry#connect#activate ~callback:ok_cb in @@ -1290,7 +1293,10 @@ let build_ui () = (* Initializing hooks *) let refresh_style style = let style = style_manager#style_scheme style in - let iter_session v = v.script#source_buffer#set_style_scheme style in + let iter_session v = + v.script#source_buffer#set_style_scheme style; + v.proof#source_buffer#set_style_scheme style; + v.messages#default_route#source_buffer#set_style_scheme style in List.iter iter_session notebook#pages in let refresh_language lang = diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in index 2d3964f210..be8aab9e49 100644 --- a/ide/coqide_WIN32.ml.in +++ b/ide/coqide_WIN32.ml.in @@ -44,6 +44,7 @@ let () = Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; set_win32_path (); Coq.interrupter := win32_interrupt; - reroute_stdout_stderr () + reroute_stdout_stderr (); + try ignore (Unix.getenv "GTK_CSD") with Not_found -> Unix.putenv "GTK_CSD" "0" let init () = () diff --git a/ide/idetop.ml b/ide/idetop.ml index 0ef7fca41f..fa458e7c6e 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -232,32 +232,32 @@ let goals () = let doc = get_doc () in set_doc @@ Stm.finish ~doc; try - let newp = Vernacstate.Proof_global.give_me_the_proof () in + let newp = Vernacstate.Declare.give_me_the_proof () in if Proof_diffs.show_diffs () then begin let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in let diff_goal_map = Proof_diffs.make_goal_map oldp newp in Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp)) end else Some (export_pre_goals Proof.(data newp) process_goal) - with Vernacstate.Proof_global.NoCurrentProof -> None + with Vernacstate.Declare.NoCurrentProof -> None [@@ocaml.warning "-3"];; let evars () = try let doc = get_doc () in set_doc @@ Stm.finish ~doc; - let pfts = Vernacstate.Proof_global.give_me_the_proof () in + let pfts = Vernacstate.Declare.give_me_the_proof () in let Proof.{ sigma } = Proof.data pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in Some el - with Vernacstate.Proof_global.NoCurrentProof -> None + with Vernacstate.Declare.NoCurrentProof -> None [@@ocaml.warning "-3"] let hints () = try - let pfts = Vernacstate.Proof_global.give_me_the_proof () in + let pfts = Vernacstate.Declare.give_me_the_proof () in let Proof.{ goals; sigma } = Proof.data pfts in match goals with | [] -> None @@ -266,7 +266,7 @@ let hints () = let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in Some (hint_hyps, concl_next_tac) - with Vernacstate.Proof_global.NoCurrentProof -> None + with Vernacstate.Declare.NoCurrentProof -> None [@@ocaml.warning "-3"] (** Other API calls *) @@ -287,11 +287,11 @@ let status force = List.rev_map Names.Id.to_string l in let proof = - try Some (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ())) - with Vernacstate.Proof_global.NoCurrentProof -> None + try Some (Names.Id.to_string (Vernacstate.Declare.get_current_proof_name ())) + with Vernacstate.Declare.NoCurrentProof -> None in let allproofs = - let l = Vernacstate.Proof_global.get_all_proof_names () in + let l = Vernacstate.Declare.get_all_proof_names () in List.map Names.Id.to_string l in { @@ -340,7 +340,7 @@ let import_search_constraint = function | Interface.Include_Blacklist -> Search.Include_Blacklist let search flags = - let pstate = Vernacstate.Proof_global.get_pstate () in + let pstate = Vernacstate.Declare.get_pstate () in List.map export_coq_object (Search.interface_search ?pstate ( List.map (fun (c, b) -> (import_search_constraint c, b)) flags) ) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index eeb818ce5f..482cecc1f8 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -536,3 +536,72 @@ let rec is_valid (s : Pp.t) = match Pp.repr s with | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s let validate s = if is_valid s then s else Pp.str "This error massage can't be printed." + +(** encoding list of strings as a string in a shell-like compatible way: + string with spaces and no ' -> '...' + string with spaces and ' -> split string into substrings separated with \' + ' -> \' + \ -> \\ + *) + +let decode_string_list s = + let l = String.length s in + let fail_backslash () = + failwith "Backslash is used to quote single quotes in quoted strings; it should otherwise be doubled" in + let rec find_word quoted b i = + if i = l then + if quoted then failwith "Unmatched single quote" + else i + else + let c = s.[i] in + if c = ' ' && not quoted then i+1 + else if c = '\'' then find_word (not quoted) b (i+1) + else if c = '\\' && not quoted then + if i = l-1 then fail_backslash () + else + let c = s.[i+1] in + if c = '\'' || c = '\\' then + (Buffer.add_char b c; find_word quoted b (i+2)) + else fail_backslash () + else + (Buffer.add_char b c; + find_word quoted b (i+1)) in + let rec collect_words i = + if i = l then [] else + let b = Buffer.create l in + let i = find_word false b i in + Buffer.contents b :: collect_words i in + collect_words 0 + +let needs_quote s i = + (* Tells if there is a space and if a space, before the next single quote *) + match CString.index_from_opt s i ' ', CString.index_from_opt s i '\'' with + | Some _, None -> true + | Some i, Some j -> i < j + | _ -> false + +let encode_string s = + (* Could be optimized so that "a b'c" is "'a b'\'c" rather than "'a b'\''c'" *) + let l = String.length s in + let b = Buffer.create (l + 10) in + let close quoted = if quoted then Buffer.add_char b '\'' in + let rec aux quoted i = + if i = l then close quoted + else + let c = s.[i] in + if c = '\'' then + (close quoted; + Buffer.add_string b "\\'"; + start (i+1)) + else if c = '\\' && not quoted then + (Buffer.add_string b "\\\\"; aux quoted (i+1)) + else + (Buffer.add_char b c; aux quoted (i+1)) + and start i = + let q = needs_quote s i in + if q then Buffer.add_char b '\''; + aux q i in + start 0; + Buffer.contents b + +let encode_string_list l = String.concat " " (List.map encode_string l) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index b080f5b8ed..9a17eb1402 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -102,3 +102,19 @@ val run_command : (* Checks if an error message is printable, it not replaces it with * a printable error *) val validate : Pp.t -> Pp.t + +(** [encode_string_list l] encodes a list of strings into a single + string using a "shell"-like encoding: it quotes strings + containing space by surrounding them with single quotes, and, + outside quoted strings, quotes both single quote and backslash + by prefixing them with backslash; the encoding tries to be + minimalistic. *) + +val encode_string_list : string list -> string + +(** [decode_string_list l] decodes the encoding of a string list as + a string; it fails with a Failure if a single quote is unmatched + or if a backslash in unquoted part is not followed by a single + quote or another backslash. *) + +val decode_string_list : string -> string list diff --git a/ide/session.ml b/ide/session.ml index b16af9c317..09391b7f50 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -151,7 +151,7 @@ let set_buffer_handlers else if it#has_tag Tags.Script.processed then Some old else if it#has_tag Tags.Script.error_bg then aux it it#backward_char else None in - aux it it in + aux it it#copy in let insert_cb it s = if String.length s = 0 then () else begin Minilib.log ("insert_cb " ^ string_of_int it#offset); let text_mark = add_mark it in diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index b99e5f8069..6e22172d05 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -28,6 +28,7 @@ end class type message_view = object inherit GObj.widget + method source_buffer : GSourceView3.source_buffer method connect : message_view_signals method clear : unit method add : Pp.t -> unit @@ -44,7 +45,8 @@ class type message_view = let message_view () : message_view = let buffer = GSourceView3.source_buffer ~highlight_matching_brackets:true - ~tag_table:Tags.Message.table () + ~tag_table:Tags.Message.table + ?style_scheme:(style_manager#style_scheme source_style#get) () in let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in let box = GPack.vbox () in @@ -88,6 +90,8 @@ let message_view () : message_view = val push = new GUtil.signal () + method source_buffer = buffer + method connect = new message_view_signals_impl box#as_widget push diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 21c11b2754..054dd0e571 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -18,6 +18,7 @@ end class type message_view = object inherit GObj.widget + method source_buffer : GSourceView3.source_buffer method connect : message_view_signals method clear : unit method add : Pp.t -> unit diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 3e03ef11f7..1de63953af 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -15,6 +15,7 @@ open Ideutils class type proof_view = object inherit GObj.widget + method source_buffer : GSourceView3.source_buffer method buffer : GText.buffer method refresh : force:bool -> unit method clear : unit -> unit @@ -195,7 +196,8 @@ let display mode (view : #GText.view_skel) goals hints evars = let proof_view () = let buffer = GSourceView3.source_buffer ~highlight_matching_brackets:true - ~tag_table:Tags.Proof.table () + ~tag_table:Tags.Proof.table + ?style_scheme:(style_manager#style_scheme source_style#get) () in let text_buffer = new GText.buffer buffer#as_buffer in let view = GSourceView3.source_view @@ -217,6 +219,8 @@ let proof_view () = val mutable evars = None val mutable last_width = -1 + method source_buffer = buffer + method buffer = text_buffer method clear () = buffer#set_text "" diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index db6fb9e9cd..8217f72066 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -11,6 +11,7 @@ class type proof_view = object inherit GObj.widget + method source_buffer : GSourceView3.source_buffer method buffer : GText.buffer method refresh : force:bool -> unit method clear : unit -> unit |