diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/configwin_ihm.ml | 17 | ||||
| -rw-r--r-- | ide/coq.ml | 6 | ||||
| -rw-r--r-- | ide/coqOps.ml | 4 | ||||
| -rw-r--r-- | ide/coqide.ml | 12 | ||||
| -rw-r--r-- | ide/idetop.ml | 8 | ||||
| -rw-r--r-- | ide/ideutils.ml | 8 | ||||
| -rw-r--r-- | ide/protocol/interface.ml | 14 | ||||
| -rw-r--r-- | ide/protocol/richpp.ml | 10 | ||||
| -rw-r--r-- | ide/sentence.ml | 4 | ||||
| -rw-r--r-- | ide/session.ml | 12 | ||||
| -rw-r--r-- | ide/wg_Completion.ml | 32 | ||||
| -rw-r--r-- | ide/wg_Find.ml | 6 | ||||
| -rw-r--r-- | ide/wg_MessageView.ml | 1 | ||||
| -rw-r--r-- | ide/wg_MessageView.mli | 1 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 20 | ||||
| -rw-r--r-- | ide/wg_Segment.ml | 4 |
16 files changed, 88 insertions, 71 deletions
diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml index 91695e944e..8420d930d5 100644 --- a/ide/configwin_ihm.ml +++ b/ide/configwin_ihm.ml @@ -209,7 +209,8 @@ class ['a] list_selection_box () initializer - (** create the functions called when the buttons are clicked *) + + (* create the functions called when the buttons are clicked *) let f_add () = (* get the files to add with the function provided *) let l = add_function () in @@ -300,8 +301,10 @@ class string_param_box param (tt:GData.tooltips) = let _ = we#set_text (param.string_to_string param.string_value) in object (self) + (** This method returns the main box ready to be packed. *) method box = hbox#coerce + (** This method applies the new value of the parameter. *) method apply = let new_value = param.string_of_string we#text in @@ -347,9 +350,11 @@ class combo_param_box param (tt:GData.tooltips) = fun () -> wc#entry#text in object (self) + (** This method returns the main box ready to be packed. *) method box = hbox#coerce - (** This method applies the new value of the parameter. *) + + (** This method applies the new value of the parameter. *) method apply = let new_value = get_value () in if new_value <> param.combo_value then @@ -404,8 +409,10 @@ class text_param_box param (tt:GData.tooltips) = let _ = dbg "text_param_box: object(self)" in object (self) val wview = wview + (** This method returns the main box ready to be packed. *) method box = wf#coerce + (** This method applies the new value of the parameter. *) method apply = let v = param.string_of_string (buffer#get_text ()) in @@ -435,8 +442,10 @@ class bool_param_box param (tt:GData.tooltips) = let _ = wchk#misc#set_sensitive param.bool_editable in object (self) + (** This method returns the check button ready to be packed. *) method box = wchk#coerce + (** This method applies the new value of the parameter. *) method apply = let new_value = wchk#active in @@ -471,8 +480,10 @@ class modifiers_param_box param = tooltips#set_tip wev#coerce ~text: help ~privat: help in object (self) + (** This method returns the main box ready to be packed. *) method box = hbox#coerce + (** This method applies the new value of the parameter. *) method apply = let new_value = !value in @@ -500,8 +511,10 @@ class ['a] list_param_box (param : 'a list_param) (tt:GData.tooltips) = in object (self) + (** This method returns the main box ready to be packed. *) method box = frame_selection#box#coerce + (** This method applies the new value of the parameter. *) method apply = param.list_f_apply !listref ; diff --git a/ide/coq.ml b/ide/coq.ml index 88ffb4f0b7..91cd448eda 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -334,8 +334,8 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = (* Parsing error at the end of s : we have only received a part of an xml answer. We store the current fragment for later *) let l_end = Lexing.lexeme_end lex in - (** Heuristic hack not to reimplement the lexer: if ever the lexer dies - twice at the same place, then this is a non-recoverable error *) + (* Heuristic hack not to reimplement the lexer: if ever the lexer dies + twice at the same place, then this is a non-recoverable error *) if state.lexerror = Some l_end then raise e; state.lexerror <- Some l_end @@ -496,7 +496,7 @@ let init_coqtop coqtop task = type 'a query = 'a Interface.value task let eval_call call handle k = - (** Send messages to coqtop and prepare the decoding of the answer *) + (* 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)); diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 6c3438a4b0..8da9900724 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -255,8 +255,8 @@ object(self) let sentence = Doc.find document find in let mark = sentence.start in let iter = script#buffer#get_iter_at_mark mark in - (** Sentence starts tend to be at the end of a line, so we rather choose - the first non-line-ending position. *) + (* Sentence starts tend to be at the end of a line, so we rather choose + the first non-line-ending position. *) let rec sentence_start iter = if iter#ends_line then sentence_start iter#forward_line else iter diff --git a/ide/coqide.ml b/ide/coqide.ml index 40b8d2f484..48c08899e0 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -566,7 +566,7 @@ let update_status sn = Coq.bind (Coq.status false) next let find_next_occurrence ~backward sn = - (** go to the next occurrence of the current word, forward or backward *) + (* go to the next occurrence of the current word, forward or backward *) let b = sn.buffer in let start = find_word_start (b#get_iter_at_mark `INSERT) in let stop = find_word_end start in @@ -613,11 +613,11 @@ let printopts_callback opts v = (** Templates menu *) let get_current_word term = - (** First look to find if autocompleting *) + (* First look to find if autocompleting *) match term.script#complete_popup#proposal with | Some p -> p | None -> - (** Then look at the current selected word *) + (* Then look at the current selected word *) let buf1 = term.script#buffer in let buf2 = term.proof#buffer in if buf1#has_selection then @@ -628,7 +628,7 @@ let get_current_word term = buf2#get_text ~slice:true ~start ~stop () else if term.messages#has_selection then term.messages#get_selected_text - (** Otherwise try to find the word around the cursor *) + (* Otherwise try to find the word around the cursor *) else let it = term.script#buffer#get_iter_at_mark `INSERT in let start = find_word_start it in @@ -772,11 +772,11 @@ let uncomment = cb_on_current_term (fun t -> t.script#uncomment ()) let coqtop_arguments sn = let dialog = GWindow.dialog ~title:"Coqtop arguments" () in let coqtop = sn.coqtop in - (** Text entry *) + (* Text entry *) let args = Coq.get_arguments coqtop in let text = String.concat " " args in let entry = GEdit.entry ~text ~packing:dialog#vbox#add () in - (** Buttons *) + (* Buttons *) let box = dialog#action_area in let ok = GButton.button ~stock:`OK ~packing:box#add () in let ok_cb () = diff --git a/ide/idetop.ml b/ide/idetop.ml index a2b85041e8..8b3b566f9c 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -263,9 +263,9 @@ let wait () = set_doc (Stm.wait ~doc) let status force = - (** We remove the initial part of the current [DirPath.t] - (usually Top in an interactive session, cf "coqtop -top"), - and display the other parts (opened sections and modules) *) + (* We remove the initial part of the current [DirPath.t] + (usually Top in an interactive session, cf "coqtop -top"), + and display the other parts (opened sections and modules) *) set_doc (Stm.finish ~doc:(get_doc ())); if force then set_doc (Stm.join ~doc:(get_doc ())); @@ -408,14 +408,12 @@ let interp ((_raw, verbose), s) = (** 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 before exiting. *) - let quit = ref false (** Disabled *) let print_ast id = Xml_datatype.PCData "ERROR" (** Grouping all call handlers together + error handling *) - let eval_call c = let interruptible f x = catch_break := true; diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 7044263b94..c14af7d21d 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -43,10 +43,10 @@ color on Windows. A clean fix, if ever needed, would be to combine the attribut of the tags into a single composite tag before applying. This is left as an exercise for the reader. *) let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = - (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that - it has to reimplement its own helper function. Unluckily, it relies on - a slow algorithm, so that we have to have our own quicker version here. - Alas, it is still much slower than the native version... *) + (* FIXME: LablGTK2 does not export the C insert_with_tags function, so that + it has to reimplement its own helper function. Unluckily, it relies on + a slow algorithm, so that we have to have our own quicker version here. + Alas, it is still much slower than the native version... *) if CList.is_empty tags then buf#insert ~iter:(buf#get_iter_at_mark mark) text else let it = buf#get_iter_at_mark mark in diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml index debbc8301e..ccb6bedaf6 100644 --- a/ide/protocol/interface.ml +++ b/ide/protocol/interface.ml @@ -78,16 +78,20 @@ type option_state = { } type search_constraint = -(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) | Name_Pattern of string -(** Whether the object type satisfies a pattern *) +(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) + | Type_Pattern of string -(** Whether some subtype of object type satisfies a pattern *) +(** Whether the object type satisfies a pattern *) + | SubType_Pattern of string -(** Whether the object pertains to a module *) +(** Whether some subtype of object type satisfies a pattern *) + | In_Module of string list -(** Bypass the Search blacklist *) +(** Whether the object pertains to a module *) + | Include_Blacklist +(** Bypass the Search blacklist *) (** A list of search constraints; the boolean flag is set to [false] whenever the flag should be negated. *) diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml index 19e9799c19..b2ce55e89a 100644 --- a/ide/protocol/richpp.ml +++ b/ide/protocol/richpp.ml @@ -46,7 +46,7 @@ let rich_pp width ppcmds = let pp_buffer = Buffer.create 180 in let push_pcdata () = - (** Push the optional PCData on the above node *) + (* Push the optional PCData on the above node *) let len = Buffer.length pp_buffer in if len = 0 then () else match context.stack with @@ -77,7 +77,7 @@ let rich_pp width ppcmds = let xml = Element (node, annotation, List.rev child) in match ctx with | Leaf -> - (** Final node: we keep the result in a dummy context *) + (* 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) @@ -104,15 +104,15 @@ let rich_pp width ppcmds = 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 <pp> tags. *) + (* The whole output must be a valid document. To that + end, we nest the document inside <pp> 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. *) + (* Get the resulting XML tree. *) let () = pp_print_flush ft () in let () = assert (Buffer.length pp_buffer = 0) in match context.stack with diff --git a/ide/sentence.ml b/ide/sentence.ml index 2f7820a77c..2e508969aa 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -91,8 +91,8 @@ let tag_on_insert buffer = in try let start = grab_sentence_start prev soi in - (** The status of "{" "}" as sentence delimiters is too fragile. - We retag up to the next "." instead. *) + (* The status of "{" "}" as sentence delimiters is too fragile. + We retag up to the next "." instead. *) let stop = grab_ending_dot insert in try split_slice_lax buffer start#backward_char stop with Coq_lex.Unterminated -> diff --git a/ide/session.ml b/ide/session.ml index be2bfe060c..805e1d38a7 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -217,7 +217,7 @@ let set_buffer_handlers | Some s -> Minilib.log (s^" moved") | None -> () in - (** Pluging callbacks *) + (* Pluging callbacks *) let _ = buffer#connect#insert_text ~callback:insert_cb in let _ = buffer#connect#delete_range ~callback:delete_cb in let _ = buffer#connect#begin_user_action ~callback:begin_action_cb in @@ -427,7 +427,7 @@ let build_layout (sn:session) = GPack.vbox ~packing:(session_paned#pack1 ~shrink:false ~resize:true) () in - (** Right part of the window. *) + (* Right part of the window. *) let eval_paned = GPack.paned `HORIZONTAL ~border_width:5 ~packing:(session_box#pack ~expand:true) () in @@ -438,7 +438,7 @@ let build_layout (sn:session) = let state_paned = GPack.paned `VERTICAL ~packing:eval_paned#add2 () in - (** Proof buffer. *) + (* Proof buffer. *) let title = Printf.sprintf "Proof (%s)" sn.tab_label#text in let proof_detachable = Wg_Detachable.detachable ~title () in @@ -454,7 +454,7 @@ let build_layout (sn:session) = let proof_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_detachable#pack () in - (** Message buffer. *) + (* Message buffer. *) let message_frame = GPack.notebook ~packing:state_paned#add () in let add_msg_page pos name text (w : GObj.widget) = @@ -514,14 +514,14 @@ let build_layout (sn:session) = let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#default_route#coerce in let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in - (** When a message is received, focus on the message pane *) + (* When a message is received, focus on the message pane *) let _ = sn.messages#default_route#connect#pushed ~callback:(fun _ _ -> let num = message_frame#page_num detach#coerce in if 0 <= num then message_frame#goto_page num ) in - (** When an error occurs, paint the error label in red *) + (* When an error occurs, paint the error label in red *) let txt = label#text in let red s = "<span foreground=\"#FF0000\">" ^ s ^ "</span>" in sn.errpage#on_update ~callback:(fun l -> diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 6a9317bc2f..c39d6d0563 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -40,7 +40,7 @@ let get_syntactic_completion (buffer : GText.buffer) pattern accu = (** Retrieve completion proposals in Coq libraries *) let get_semantic_completion pattern accu = let flags = [Interface.Name_Pattern ("^" ^ pattern), true] in - (** Only get the last part of the qualified name *) + (* Only get the last part of the qualified name *) let rec last accu = function | [] -> accu | [basename] -> Proposals.add basename accu @@ -199,15 +199,15 @@ object (self) let () = self#init_proposals w props in update_completion_signal#call (start_offset, w, props) in - (** If not in the cache, we recompute it: first syntactic *) + (* If not in the cache, we recompute it: first syntactic *) let synt = get_syntactic_completion buffer w Proposals.empty in - (** Then semantic *) + (* Then semantic *) let next prop = let () = update prop in Coq.lift k in let query = Coq.bind (get_semantic_completion w synt) next in - (** If coqtop is computing, do the syntactic completion altogether *) + (* If coqtop is computing, do the syntactic completion altogether *) let occupied () = let () = update synt in k () @@ -264,20 +264,20 @@ object (self) renderer#set_properties [`FONT_DESC font; `XPAD 10] method private coordinates pos = - (** Toplevel position w.r.t. screen *) + (* Toplevel position w.r.t. screen *) let (x, y) = Gdk.Window.get_position view#misc#toplevel#misc#window in - (** Position of view w.r.t. window *) + (* Position of view w.r.t. window *) let (ux, uy) = Gdk.Window.get_position view#misc#window in - (** Relative buffer position to view *) + (* Relative buffer position to view *) let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in - (** Iter position *) + (* Iter position *) let iter = view#buffer#get_iter pos in let coords = view#get_iter_location iter in let lx = Gdk.Rectangle.x coords in let ly = Gdk.Rectangle.y coords in let w = Gdk.Rectangle.width coords in let h = Gdk.Rectangle.height coords in - (** Absolute position *) + (* Absolute position *) (x + lx + ux - dx, y + ly + uy - dy, w, h) method private select_any f = @@ -374,9 +374,9 @@ object (self) else None method private manage_scrollbar () = - (** HACK: we don't have access to the treeview size because of the lack of - LablGTK binding for certain functions, so we bypass it by approximating - it through the size of the proposals *) + (* HACK: we don't have access to the treeview size because of the lack of + LablGTK binding for certain functions, so we bypass it by approximating + it through the size of the proposals *) let height = match model#store#get_iter_first with | None -> -1 | Some iter -> @@ -434,18 +434,18 @@ object (self) else false else false in - (** Style handling *) + (* Style handling *) let _ = view#misc#connect#style_set ~callback:self#refresh_style in let _ = self#refresh_style () in let _ = data#set_resize_mode `PARENT in let _ = frame#set_resize_mode `PARENT in - (** Callback to model *) + (* Callback to model *) let _ = model#connect#start_completion ~callback:self#start_callback in let _ = model#connect#update_completion ~callback:self#update_callback in let _ = model#connect#end_completion ~callback:self#end_callback in - (** Popup interaction *) + (* Popup interaction *) let _ = view#event#connect#key_press ~callback:key_cb in - (** Hiding the popup when necessary*) + (* Hiding the popup when necessary*) let _ = view#misc#connect#hide ~callback:obj#misc#hide in let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in let _ = view#connect#move_cursor ~callback:move_cb in diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index 296a942321..7d2d7da570 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -212,13 +212,13 @@ class finder name (view : GText.view) = initializer let _ = self#hide () in - (** Widget button interaction *) + (* Widget button interaction *) let _ = next_button#connect#clicked ~callback:self#find_forward in let _ = previous_button#connect#clicked ~callback:self#find_backward in let _ = replace_button#connect#clicked ~callback:self#replace in let _ = replace_all_button#connect#clicked ~callback:self#replace_all in - (** Keypress interaction *) + (* Keypress interaction *) let generic_cb esc_cb ret_cb ev = let ev_key = GdkEvent.Key.keyval ev in let (return, _) = GtkData.AccelGroup.parse "Return" in @@ -232,7 +232,7 @@ class finder name (view : GText.view) = let _ = find_entry#event#connect#key_press ~callback:find_cb in let _ = replace_entry#event#connect#key_press ~callback:replace_cb in - (** TextView interaction *) + (* TextView interaction *) let view_cb ev = if widget#visible then let ev_key = GdkEvent.Key.keyval ev in diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index a79a093e32..6b09b344b5 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -36,6 +36,7 @@ class type message_view = method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) + method has_selection : bool method get_selected_text : string end diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 472aaf5ed4..613f1b4190 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -26,6 +26,7 @@ class type message_view = method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) + method has_selection : bool method get_selected_text : string end diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 74bc0b8d53..5e26c50797 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -152,11 +152,11 @@ object(self) if self#process_delete_action del then (`OK, `WRITE) else (`FAIL, `NOOP) | Action lst -> let fold accu action = match accu with - | (`FAIL, _) -> accu (** we stop now! *) + | (`FAIL, _) -> accu (* we stop now! *) | (`OK, status) -> let (res, nstatus) = self#process_action action in let merge op1 op2 = match op1, op2 with - | `NOOP, `NOOP -> `NOOP (** only a noop when both are *) + | `NOOP, `NOOP -> `NOOP (* only a noop when both are *) | _ -> `WRITE in (res, merge status nstatus) @@ -172,8 +172,8 @@ object(self) | (`OK, _) -> history <- rem; redo <- (negate_action action) :: redo - | (`FAIL, `NOOP) -> () (** we do nothing *) - | (`FAIL, `WRITE) -> self#clear_undo () (** we don't know how we failed, so start off *) + | (`FAIL, `NOOP) -> () (* we do nothing *) + | (`FAIL, `WRITE) -> self#clear_undo () (* we don't know how we failed, so start off *) end method perform_redo () = match redo with @@ -184,8 +184,8 @@ object(self) | (`OK, _) -> redo <- rem; history <- (negate_action action) :: history; - | (`FAIL, `NOOP) -> () (** we do nothing *) - | (`FAIL, `WRITE) -> self#clear_undo () (** we don't know how we failed *) + | (`FAIL, `NOOP) -> () (* we do nothing *) + | (`FAIL, `WRITE) -> self#clear_undo () (* we don't know how we failed *) end method undo () = @@ -212,9 +212,9 @@ object(self) self#with_lock_undo self#process_begin_user_action () method process_end_user_action () = - (** Search for the pending action *) + (* Search for the pending action *) let rec split accu = function - | [] -> raise Not_found (** no pending begin action! *) + | [] -> raise Not_found (* no pending begin action! *) | EndGrp :: rem -> let grp = List.rev accu in let rec flatten = function @@ -240,7 +240,7 @@ object(self) (* Save the insert action *) let len = Glib.Utf8.length s in let mergeable = - (** heuristic: split at newline and atomic pastes *) + (* heuristic: split at newline and atomic pastes *) len = 1 && (s <> "\n") in let ins = { @@ -460,7 +460,7 @@ object (self) if not proceed then GtkSignal.stop_emit () in let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in - (** Plug on preferences *) + (* Plug on preferences *) let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in let _ = background_color#connect#changed ~callback:cb in let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index 0f5ed8d896..3b2572f9d2 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -70,7 +70,7 @@ object (self) let cb rect = let w = rect.Gtk.width in let h = rect.Gtk.height in - (** Only refresh when size actually changed, otherwise loops *) + (* Only refresh when size actually changed, otherwise loops *) if self#misc#visible && (width <> w || height <> h) then begin width <- w; height <- h; @@ -91,7 +91,7 @@ object (self) let _ = eventbox#event#connect#button_press ~callback:clicked_cb in let cb show = if show then self#misc#show () else self#misc#hide () in stick show_progress_bar self cb; - (** Initial pixmap *) + (* Initial pixmap *) draw#set_pixmap pixmap; refresh_timer.Ideutils.run ~ms:300 ~callback:(fun () -> if need_refresh then self#refresh (); true) |