aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml6
-rw-r--r--ide/coq.mli2
-rw-r--r--ide/coqOps.ml19
-rw-r--r--ide/coqide.ml10
-rw-r--r--ide/coqide_ui.ml285
-rw-r--r--ide/coqidetop.mllib1
-rw-r--r--ide/ide_slave.ml21
-rw-r--r--ide/ideutils.ml13
-rw-r--r--ide/preferences.ml22
-rw-r--r--ide/session.ml12
-rw-r--r--ide/texmacspp.ml766
-rw-r--r--ide/texmacspp.mli12
-rw-r--r--ide/wg_Command.ml6
-rw-r--r--ide/wg_Completion.ml26
-rw-r--r--ide/wg_Detachable.ml4
-rw-r--r--ide/wg_Find.ml6
-rw-r--r--ide/wg_Notebook.ml2
-rw-r--r--ide/wg_ProofView.ml41
-rw-r--r--ide/wg_ScriptView.ml12
-rw-r--r--ide/wg_Segment.ml6
20 files changed, 248 insertions, 1024 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 3a1d877872..cd45e2fcdc 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -519,6 +519,7 @@ struct
let all_basic = ["Printing"; "All"]
let existential = ["Printing"; "Existential"; "Instances"]
let universes = ["Printing"; "Universes"]
+ let unfocused = ["Printing"; "Unfocused"]
type bool_descr = { opts : t list; init : bool; label : string }
@@ -534,7 +535,8 @@ struct
label = "Display _existential variable instances" };
{ opts = [universes]; init = false; label = "Display _universe levels" };
{ opts = [all_basic;existential;universes]; init = false;
- label = "Display all _low-level contents" }
+ label = "Display all _low-level contents" };
+ { opts = [unfocused]; init = false; label = "Display _unfocused goals" }
]
(** The current status of the boolean options *)
@@ -549,6 +551,8 @@ struct
let _ = reset ()
+ let printing_unfocused () = Hashtbl.find current_state unfocused
+
(** Transmitting options to coqtop *)
let enforce h k =
diff --git a/ide/coq.mli b/ide/coq.mli
index ab8c12a6f1..e8e2f5239e 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -140,6 +140,8 @@ sig
val set : t -> bool -> unit
+ val printing_unfocused: unit -> bool
+
(** [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 222b9eed9f..b180aa5569 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -117,7 +117,7 @@ end = struct
(b#get_iter_at_mark s.start)#offset
(b#get_iter_at_mark s.stop)#offset
(ellipsize
- ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop)))
+ ((b#get_iter_at_mark s.start)#get_slice ~stop:(b#get_iter_at_mark s.stop)))
(String.concat "," (List.map str_of_flag s.flags))
(ellipsize
(String.concat ","
@@ -128,9 +128,6 @@ 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)
@@ -207,7 +204,7 @@ object (self)
in
List.iter (fun s -> set_index s (s.index + 1)) after;
set_index s (document_length - List.length after);
- ignore ((SentenceId.connect s)#changed self#on_changed);
+ ignore ((SentenceId.connect s)#changed ~callback:self#on_changed);
document_length <- document_length + 1;
List.iter (fun f -> f `INSERT) cbs
@@ -221,8 +218,8 @@ object (self)
List.iter (fun f -> f `REMOVE) cbs
initializer
- let _ = (Doc.connect doc)#pushed self#on_push in
- let _ = (Doc.connect doc)#popped self#on_pop in
+ let _ = (Doc.connect doc)#pushed ~callback:self#on_push in
+ let _ = (Doc.connect doc)#popped ~callback:self#on_pop in
()
end
@@ -273,15 +270,15 @@ object(self)
else iter
in
let iter = sentence_start iter in
- script#buffer#place_cursor iter;
+ script#buffer#place_cursor ~where:iter;
ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
in
- let _ = segment#connect#clicked on_click in
+ let _ = segment#connect#clicked ~callback:on_click in
()
method private tooltip_callback ~x ~y ~kbd tooltip =
- let x, y = script#window_to_buffer_coords `WIDGET x y in
- let iter = script#get_iter_at_location x y in
+ let x, y = script#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
+ let iter = script#get_iter_at_location ~x ~y in
if iter#has_tag Tags.Script.tooltip then begin
let s =
let rec aux iter =
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 25858acced..0b7567a5ae 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -792,11 +792,11 @@ let coqtop_arguments sn =
sn.messages#push Feedback.Error (Pp.str msg)
else dialog#destroy ()
in
- let _ = entry#connect#activate ok_cb in
- let _ = ok#connect#clicked ok_cb in
+ let _ = entry#connect#activate ~callback:ok_cb in
+ let _ = ok#connect#clicked ~callback:ok_cb in
let cancel = GButton.button ~stock:`CANCEL ~packing:box#add () in
let cancel_cb () = dialog#destroy () in
- let _ = cancel#connect#clicked cancel_cb in
+ let _ = cancel#connect#clicked ~callback:cancel_cb in
dialog#show ()
let coqtop_arguments = cb_on_current_term coqtop_arguments
@@ -1274,8 +1274,8 @@ let build_ui () =
if b then toolbar#misc#show () else toolbar#misc#hide ()
in
stick show_toolbar toolbar refresh_toolbar;
- let _ = source_style#connect#changed refresh_style in
- let _ = source_language#connect#changed refresh_language in
+ let _ = source_style#connect#changed ~callback:refresh_style in
+ let _ = source_language#connect#changed ~callback:refresh_language in
(* Color configuration *)
Tags.Script.incomplete#set_property
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 2ae18593ac..717c4000f5 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -28,148 +28,149 @@ let list_queries menu li =
res_buf
let init () =
- let theui = Printf.sprintf "<ui>
-<menubar name='CoqIde MenuBar'>
- <menu action='File'>
- <menuitem action='New' />
- <menuitem action='Open' />
- <menuitem action='Save' />
- <menuitem action='Save as' />
- <menuitem action='Save all' />
- <menuitem action='Revert all buffers' />
- <menuitem action='Close buffer' />
- <menuitem action='Print...' />
- <menu action='Export to'>
- <menuitem action='Html' />
- <menuitem action='Latex' />
- <menuitem action='Dvi' />
- <menuitem action='Pdf' />
- <menuitem action='Ps' />
- </menu>
- <menuitem action='Rehighlight' />
- %s
- </menu>
- <menu name='Edit' action='Edit'>
- <menuitem action='Undo' />
- <menuitem action='Redo' />
- <separator />
- <menuitem action='Cut' />
- <menuitem action='Copy' />
- <menuitem action='Paste' />
- <separator />
- <menuitem action='Find' />
- <menuitem action='Find Next' />
- <menuitem action='Find Previous' />
- <menuitem action='Complete Word' />
- <separator />
- <menuitem action='External editor' />
- <separator />
- <menuitem name='Prefs' action='Preferences' />
- </menu>
- <menu name='View' action='View'>
- <menuitem action='Previous tab' />
- <menuitem action='Next tab' />
- <separator/>
- <menuitem action='Zoom in' />
- <menuitem action='Zoom out' />
- <menuitem action='Zoom fit' />
- <separator/>
- <menuitem action='Show Toolbar' />
- <menuitem action='Query Pane' />
- <separator/>
- <menuitem action='Display implicit arguments' />
- <menuitem action='Display coercions' />
- <menuitem action='Display raw matching expressions' />
- <menuitem action='Display notations' />
- <menuitem action='Display all basic low-level contents' />
- <menuitem action='Display existential variable instances' />
- <menuitem action='Display universe levels' />
- <menuitem action='Display all low-level contents' />
- </menu>
- <menu action='Navigation'>
- <menuitem action='Forward' />
- <menuitem action='Backward' />
- <menuitem action='Go to' />
- <menuitem action='Start' />
- <menuitem action='End' />
- <menuitem action='Interrupt' />
- <menuitem action='Previous' />
- <menuitem action='Next' />
- </menu>
- <menu action='Try Tactics'>
- <menuitem action='auto' />
- <menuitem action='auto with *' />
- <menuitem action='eauto' />
- <menuitem action='eauto with *' />
- <menuitem action='intuition' />
- <menuitem action='omega' />
- <menuitem action='simpl' />
- <menuitem action='tauto' />
- <menuitem action='trivial' />
- <menuitem action='Wizard' />
- <separator />
- %s
- </menu>
- <menu action='Templates'>
- <menuitem action='Lemma' />
- <menuitem action='Theorem' />
- <menuitem action='Definition' />
- <menuitem action='Inductive' />
- <menuitem action='Fixpoint' />
- <menuitem action='Scheme' />
- <menuitem action='match' />
- <separator />
- %s
- </menu>
- <menu action='Queries'>
- <menuitem action='Search' />
- <menuitem action='Check' />
- <menuitem action='Print' />
- <menuitem action='About' />
- <menuitem action='Locate' />
- <menuitem action='Print Assumptions' />
- <separator />
- %s
- </menu>
- <menu name='Tools' action='Tools'>
- <menuitem action='Comment' />
- <menuitem action='Uncomment' />
- <separator />
- <menuitem action='Coqtop arguments' />
- </menu>
- <menu action='Compile'>
- <menuitem action='Compile buffer' />
- <menuitem action='Make' />
- <menuitem action='Next error' />
- <menuitem action='Make makefile' />
- </menu>
- <menu action='Windows'>
- <menuitem action='Detach View' />
- </menu>
- <menu name='Help' action='Help'>
- <menuitem action='Browse Coq Manual' />
- <menuitem action='Browse Coq Library' />
- <menuitem action='Help for keyword' />
- <menuitem action='Help for μPG mode' />
- <separator />
- <menuitem name='Abt' action='About Coq' />
- </menu>
-</menubar>
-<toolbar name='CoqIde ToolBar'>
- <toolitem action='Save' />
- <toolitem action='Close buffer' />
- <toolitem action='Forward' />
- <toolitem action='Backward' />
- <toolitem action='Go to' />
- <toolitem action='Start' />
- <toolitem action='End' />
- <toolitem action='Force' />
- <toolitem action='Interrupt' />
- <toolitem action='Previous' />
- <toolitem action='Next' />
- <toolitem action='Wizard' />
-</toolbar>
-</ui>"
+ let theui = Printf.sprintf "<ui>\
+\n<menubar name='CoqIde MenuBar'>\
+\n <menu action='File'>\
+\n <menuitem action='New' />\
+\n <menuitem action='Open' />\
+\n <menuitem action='Save' />\
+\n <menuitem action='Save as' />\
+\n <menuitem action='Save all' />\
+\n <menuitem action='Revert all buffers' />\
+\n <menuitem action='Close buffer' />\
+\n <menuitem action='Print...' />\
+\n <menu action='Export to'>\
+\n <menuitem action='Html' />\
+\n <menuitem action='Latex' />\
+\n <menuitem action='Dvi' />\
+\n <menuitem action='Pdf' />\
+\n <menuitem action='Ps' />\
+\n </menu>\
+\n <menuitem action='Rehighlight' />\
+\n %s\
+\n </menu>\
+\n <menu name='Edit' action='Edit'>\
+\n <menuitem action='Undo' />\
+\n <menuitem action='Redo' />\
+\n <separator />\
+\n <menuitem action='Cut' />\
+\n <menuitem action='Copy' />\
+\n <menuitem action='Paste' />\
+\n <separator />\
+\n <menuitem action='Find' />\
+\n <menuitem action='Find Next' />\
+\n <menuitem action='Find Previous' />\
+\n <menuitem action='Complete Word' />\
+\n <separator />\
+\n <menuitem action='External editor' />\
+\n <separator />\
+\n <menuitem name='Prefs' action='Preferences' />\
+\n </menu>\
+\n <menu name='View' action='View'>\
+\n <menuitem action='Previous tab' />\
+\n <menuitem action='Next tab' />\
+\n <separator/>\
+\n <menuitem action='Zoom in' />\
+\n <menuitem action='Zoom out' />\
+\n <menuitem action='Zoom fit' />\
+\n <separator/>\
+\n <menuitem action='Show Toolbar' />\
+\n <menuitem action='Query Pane' />\
+\n <separator/>\
+\n <menuitem action='Display implicit arguments' />\
+\n <menuitem action='Display coercions' />\
+\n <menuitem action='Display raw matching expressions' />\
+\n <menuitem action='Display notations' />\
+\n <menuitem action='Display all basic low-level contents' />\
+\n <menuitem action='Display existential variable instances' />\
+\n <menuitem action='Display universe levels' />\
+\n <menuitem action='Display all low-level contents' />\
+\n <menuitem action='Display unfocused goals' />\
+\n </menu>\
+\n <menu action='Navigation'>\
+\n <menuitem action='Forward' />\
+\n <menuitem action='Backward' />\
+\n <menuitem action='Go to' />\
+\n <menuitem action='Start' />\
+\n <menuitem action='End' />\
+\n <menuitem action='Interrupt' />\
+\n <menuitem action='Previous' />\
+\n <menuitem action='Next' />\
+\n </menu>\
+\n <menu action='Try Tactics'>\
+\n <menuitem action='auto' />\
+\n <menuitem action='auto with *' />\
+\n <menuitem action='eauto' />\
+\n <menuitem action='eauto with *' />\
+\n <menuitem action='intuition' />\
+\n <menuitem action='omega' />\
+\n <menuitem action='simpl' />\
+\n <menuitem action='tauto' />\
+\n <menuitem action='trivial' />\
+\n <menuitem action='Wizard' />\
+\n <separator />\
+\n %s\
+\n </menu>\
+\n <menu action='Templates'>\
+\n <menuitem action='Lemma' />\
+\n <menuitem action='Theorem' />\
+\n <menuitem action='Definition' />\
+\n <menuitem action='Inductive' />\
+\n <menuitem action='Fixpoint' />\
+\n <menuitem action='Scheme' />\
+\n <menuitem action='match' />\
+\n <separator />\
+\n %s\
+\n </menu>\
+\n <menu action='Queries'>\
+\n <menuitem action='Search' />\
+\n <menuitem action='Check' />\
+\n <menuitem action='Print' />\
+\n <menuitem action='About' />\
+\n <menuitem action='Locate' />\
+\n <menuitem action='Print Assumptions' />\
+\n <separator />\
+\n %s\
+\n </menu>\
+\n <menu name='Tools' action='Tools'>\
+\n <menuitem action='Comment' />\
+\n <menuitem action='Uncomment' />\
+\n <separator />\
+\n <menuitem action='Coqtop arguments' />\
+\n </menu>\
+\n <menu action='Compile'>\
+\n <menuitem action='Compile buffer' />\
+\n <menuitem action='Make' />\
+\n <menuitem action='Next error' />\
+\n <menuitem action='Make makefile' />\
+\n </menu>\
+\n <menu action='Windows'>\
+\n <menuitem action='Detach View' />\
+\n </menu>\
+\n <menu name='Help' action='Help'>\
+\n <menuitem action='Browse Coq Manual' />\
+\n <menuitem action='Browse Coq Library' />\
+\n <menuitem action='Help for keyword' />\
+\n <menuitem action='Help for μPG mode' />\
+\n <separator />\
+\n <menuitem name='Abt' action='About Coq' />\
+\n </menu>\
+\n</menubar>\
+\n<toolbar name='CoqIde ToolBar'>\
+\n <toolitem action='Save' />\
+\n <toolitem action='Close buffer' />\
+\n <toolitem action='Forward' />\
+\n <toolitem action='Backward' />\
+\n <toolitem action='Go to' />\
+\n <toolitem action='Start' />\
+\n <toolitem action='End' />\
+\n <toolitem action='Force' />\
+\n <toolitem action='Interrupt' />\
+\n <toolitem action='Previous' />\
+\n <toolitem action='Next' />\
+\n <toolitem action='Wizard' />\
+\n</toolbar>\
+\n</ui>"
(if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "")
(Buffer.contents (list_items "Tactic" Coq_commands.tactics))
(Buffer.contents (list_items "Template" Coq_commands.commands))
diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib
index 043ad6008b..df988d8f11 100644
--- a/ide/coqidetop.mllib
+++ b/ide/coqidetop.mllib
@@ -4,6 +4,5 @@ Xml_printer
Serialize
Richpp
Xmlprotocol
-Texmacspp
Document
Ide_slave
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index bf86db08ff..dbca959eae 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -54,7 +54,8 @@ let coqide_known_option table = List.mem table [
["Printing";"All"];
["Printing";"Records"];
["Printing";"Existential";"Instances"];
- ["Printing";"Universes"]]
+ ["Printing";"Universes"];
+ ["Printing";"Unfocused"]]
let is_known_option cmd = match cmd with
| VernacSetOption (o,BoolValue true)
@@ -82,7 +83,7 @@ let add ((s,eid),(sid,verbose)) =
let loc_ast = Stm.parse_sentence sid pa in
let newid, rc = Stm.add ~ontop:sid verbose loc_ast in
let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
- ide_cmd_checks newid loc_ast;
+ ide_cmd_checks ~id:newid loc_ast;
(* TODO: the "" parameter is a leftover of the times the protocol
* used to include stderr/stdout output.
*
@@ -387,14 +388,8 @@ let interp ((_raw, verbose), s) =
let quit = ref false
-(** Serializes the output of Stm.get_ast *)
-let print_ast id =
- match Stm.get_ast id with
- | Some (expr, loc) -> begin
- try Texmacspp.tmpp expr loc
- with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e)
- end
- | None -> Xml_datatype.PCData "ERROR"
+(** Disabled *)
+let print_ast id = Xml_datatype.PCData "ERROR"
(** Grouping all call handlers together + error handling *)
@@ -505,12 +500,12 @@ let rec parse = function
let () = Coqtop.toploop_init := (fun args ->
let args = parse args in
- Flags.make_silent true;
+ Flags.quiet := true;
CoqworkmgrApi.(init Flags.High);
args)
let () = Coqtop.toploop_run := loop
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"
+" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\
+\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n"
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index da867e689e..a08ab07b5f 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -35,17 +35,6 @@ let flash_info =
let flash_context = status#new_context ~name:"Flash" in
(fun ?(delay=5000) s -> flash_context#flash ~delay s)
-let xml_to_string xml =
- let open Xml_datatype in
- let buf = Buffer.create 1024 in
- let rec iter = function
- | PCData s -> Buffer.add_string buf s
- | Element (_, _, children) ->
- List.iter iter children
- in
- let () = iter xml in
- Buffer.contents buf
-
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
@@ -58,7 +47,7 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in
let start = buf#get_iter_at_mark mark in
let stop = buf#get_iter_at_mark rmark in
- let iter tag = buf#apply_tag tag start stop in
+ let iter tag = buf#apply_tag tag ~start ~stop in
List.iter iter tags
let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
diff --git a/ide/preferences.ml b/ide/preferences.ml
index f0fd45d77f..9fe9c6337d 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -73,8 +73,8 @@ end
let stick (pref : 'a preference) (obj : #GObj.widget as 'obj)
(cb : 'a -> unit) =
let _ = cb pref#get in
- let p_id = pref#connect#changed (fun v -> cb v) in
- let _ = obj#misc#connect#destroy (fun () -> pref#connect#disconnect p_id) in
+ let p_id = pref#connect#changed ~callback:(fun v -> cb v) in
+ let _ = obj#misc#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in
()
(** Useful marshallers *)
@@ -314,7 +314,7 @@ let attach_modifiers (pref : string preference) prefix =
in
GtkData.AccelMap.foreach change
in
- pref#connect#changed cb
+ pref#connect#changed ~callback:cb
let modifier_for_navigation =
new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string)
@@ -360,7 +360,7 @@ object
~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string)
as super
- method set v =
+ method! set v =
if not (Flags.is_standard_doc_url v) &&
v <> use_default_doc_url &&
(* Extra hack to support links to last released doc version *)
@@ -408,10 +408,10 @@ let background_color =
new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string)
let attach_bg (pref : string preference) (tag : GText.tag) =
- pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c))
+ pref#connect#changed ~callback:(fun c -> tag#set_property (`BACKGROUND c))
let attach_fg (pref : string preference) (tag : GText.tag) =
- pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c))
+ pref#connect#changed ~callback:(fun c -> tag#set_property (`FOREGROUND c))
let processing_color =
new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string)
@@ -468,7 +468,7 @@ let create_tag name default =
let iter table =
let tag = GText.tag ~name () in
table#add tag#as_tag;
- ignore (pref#connect#changed (fun _ -> set_tag tag));
+ ignore (pref#connect#changed ~callback:(fun _ -> set_tag tag));
set_tag tag;
in
List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
@@ -601,8 +601,8 @@ object (self)
box#pack italic#coerce;
box#pack underline#coerce;
let cb but obj = obj#set_sensitive (not but#active) in
- let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in
- let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in
+ let _ = fg_unset#connect#toggled ~callback:(fun () -> cb fg_unset fg_color#misc) in
+ let _ = bg_unset#connect#toggled ~callback:(fun () -> cb bg_unset bg_color#misc) in
()
end
@@ -692,7 +692,7 @@ let configure ?(apply=(fun () -> ())) () =
~color:(Tags.color_of_string pref#get)
~packing:(table#attach ~left:1 ~top:i) ()
in
- let _ = button#connect#color_set begin fun () ->
+ let _ = button#connect#color_set ~callback:begin fun () ->
pref#set (Tags.string_of_color button#color)
end in
let reset _ =
@@ -754,7 +754,7 @@ let configure ?(apply=(fun () -> ())) () =
let button text (pref : bool preference) =
let active = pref#get in
let but = GButton.check_button ~label:text ~active ~packing:box#pack () in
- ignore (but#connect#toggled (fun () -> pref#set but#active))
+ ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active))
in
let () = button "Dynamic word wrap" dynamic_word_wrap in
let () = button "Show line number" show_line_number in
diff --git a/ide/session.ml b/ide/session.ml
index 6262820e7b..7aea75ac84 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -249,8 +249,8 @@ let make_table_widget ?sort cd cb =
let () = data#set_headers_visible true in
let () = data#set_headers_clickable true in
let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in
- let _ = background_color#connect#changed refresh in
- let _ = data#misc#connect#realize (fun () -> refresh background_color#get) in
+ let _ = background_color#connect#changed ~callback:refresh in
+ let _ = data#misc#connect#realize ~callback:(fun () -> refresh background_color#get) in
let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
let cols =
List.map2 (fun (_,c) (_,n,v) ->
@@ -308,8 +308,8 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
!callback errs;
List.iter (fun (lno, msg) -> access (fun columns store ->
let line = store#append () in
- store#set line (find_int_col "Line" columns) lno;
- store#set line (find_string_col "Error message" columns) msg))
+ store#set ~row:line ~column:(find_int_col "Line" columns) lno;
+ store#set ~row:line ~column:(find_string_col "Error message" columns) msg))
errs
end
method on_update ~callback:cb = callback := cb
@@ -348,8 +348,8 @@ let create_jobpage coqtop coqops : jobpage =
else false)
else
let line = store#append () in
- store#set line column id;
- store#set line (find_string_col "Job name" columns) job))
+ store#set ~row:line ~column id;
+ store#set ~row:line ~column:(find_string_col "Job name" columns) job))
jobs
end
method on_update ~callback:cb = callback := cb
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
deleted file mode 100644
index e20704b7fb..0000000000
--- a/ide/texmacspp.ml
+++ /dev/null
@@ -1,766 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-open Constrexpr
-open Names
-open Misctypes
-open Bigint
-open Decl_kinds
-open Extend
-open Libnames
-open Constrexpr_ops
-
-let unlock loc =
- let start, stop = Loc.unloc loc in
- (string_of_int start, string_of_int stop)
-
-let xmlWithLoc loc ename attr xml =
- let start, stop = unlock loc in
- Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
-
-let get_fst_attr_in_xml_list attr xml_list =
- let attrs_list =
- List.map (function
- | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
- | _ -> [])
- xml_list in
- match List.flatten attrs_list with
- | [] -> (attr, "")
- | l -> (List.hd l)
-
-let backstep_loc xmllist =
- let start_att = get_fst_attr_in_xml_list "begin" xmllist in
- let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in
- [start_att ; stop_att]
-
-let compare_begin_att xml1 xml2 =
- let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
- let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
- match att1, att2 with
- | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
- | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
- | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
- | _ -> 0
-
-let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] []
-
-let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] []
-
-let xmlThm typ name loc xml =
- xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
-
-let xmlDef typ name loc xml =
- xmlWithLoc loc "definition" ["type", typ; "name", name] xml
-
-let xmlNotation attr name loc xml =
- xmlWithLoc loc "notation" (("name", name) :: attr) xml
-
-let xmlReservedNotation attr name loc =
- xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
-
-let xmlCst name ?(attr=[]) loc =
- xmlWithLoc loc "constant" (("name", name) :: attr) []
-
-let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
- xmlWithLoc loc "operator"
- (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
-
-let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml
-
-let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml
-
-let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
-
-let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
-
-let xmlCase xml = Element("case", [], xml)
-
-let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
-
-let xmlWith xml = Element("with", [], xml)
-
-let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
-
-let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml
-
-let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
-
-let xmlFixpoint xml = Element("fixpoint", [], xml)
-
-let xmlCheck loc xml = xmlWithLoc loc "check" [] xml
-
-let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
-
-let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
-
-let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
-
-let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
-
-let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
-
-let xmlReference ref =
- let name = Libnames.string_of_reference ref in
- let i, j = Loc.unloc (Libnames.loc_of_reference ref) in
- let b, e = string_of_int i, string_of_int j in
- Element("reference",["name", name; "begin", b; "end", e] ,[])
-
-let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
-let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
-
-let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
-let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
-let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
-
-let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
-
-let xmlScope loc action ?(attr=[]) name xml =
- xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml
-
-let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
-
-let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
-
-let xmlSectionSubsetDescr name ssd =
- Element("sectionsubsetdescr",["name",name],
- [PCData (Proof_using.to_string ssd)])
-
-let xmlDeclareMLModule loc s =
- xmlWithLoc loc "declarexmlmodule" []
- (List.map (fun x -> Element("path",["value",x],[])) s)
-
-(* tactics *)
-let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml
-
-(* toplevel commands *)
-let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml
-
-let xmlTODO loc x =
- xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-let string_of_name n =
- match n with
- | Anonymous -> "_"
- | Name id -> Id.to_string id
-
-let string_of_glob_sort s =
- match s with
- | GProp -> "Prop"
- | GSet -> "Set"
- | GType _ -> "Type"
-
-let string_of_cast_sort c =
- match c with
- | CastConv _ -> "CastConv"
- | CastVM _ -> "CastVM"
- | CastNative _ -> "CastNative"
- | CastCoerce -> "CastCoerce"
-
-let string_of_case_style s =
- match s with
- | LetStyle -> "Let"
- | IfStyle -> "If"
- | LetPatternStyle -> "LetPattern"
- | MatchStyle -> "Match"
- | RegularStyle -> "Regular"
-
-let attribute_of_syntax_modifier sm =
-match sm with
- | SetItemLevel (sl, NumLevel n) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
- | SetItemLevel (sl, NextLevel) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
- | SetLevel i -> ["level", string_of_int i]
- | SetAssoc a ->
- begin match a with
- | NonA -> ["",""]
- | RightA -> ["associativity", "right"]
- | LeftA -> ["associativity", "left"]
- end
- | SetEntryType (s, _) -> ["entrytype", s]
- | SetOnlyPrinting -> ["onlyprinting", ""]
- | SetOnlyParsing -> ["onlyparsing", ""]
- | SetCompatVersion v -> ["compat", Flags.pr_version v]
- | SetFormat (system, (loc, s)) ->
- let start, stop = unlock loc in
- ["format-"^system, s; "begin", start; "end", stop]
-
-let string_of_assumption_kind l a many =
- match l, a, many with
- | (Discharge, Logical, true) -> "Hypotheses"
- | (Discharge, Logical, false) -> "Hypothesis"
- | (Discharge, Definitional, true) -> "Variables"
- | (Discharge, Definitional, false) -> "Variable"
- | (Global, Logical, true) -> "Axioms"
- | (Global, Logical, false) -> "Axiom"
- | (Global, Definitional, true) -> "Parameters"
- | (Global, Definitional, false) -> "Parameter"
- | (Local, Logical, true) -> "Local Axioms"
- | (Local, Logical, false) -> "Local Axiom"
- | (Local, Definitional, true) -> "Local Parameters"
- | (Local, Definitional, false) -> "Local Parameter"
- | (Global, Conjectural, _) -> "Conjecture"
- | ((Discharge | Local), Conjectural, _) -> assert false
-
-let rec pp_bindlist bl =
- let tlist =
- List.flatten
- (List.map
- (fun (loc_names, _, e) ->
- let names =
- (List.map
- (fun (loc, name) ->
- xmlCst (string_of_name name) loc) loc_names) in
- match e with
- | CHole _ -> names
- | _ -> names @ [pp_expr e])
- bl) in
- match tlist with
- | [e] -> e
- | l -> xmlTyped l
-and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
- Element ("decl_notation", ["name", s], [pp_expr ce])
-and pp_local_binder lb = (* don't know what it is for now *)
- match lb with
- | CLocalDef ((loc, nam), ce, ty) ->
- let attrs = ["name", string_of_name nam] in
- let value = match ty with Some t -> CCast (Loc.merge (constr_loc ce) (constr_loc t),ce, CastConv t) | None -> ce in
- pp_expr ~attr:attrs value
- | CLocalAssum (namll, _, ce) ->
- let ppl =
- List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
- xmlTyped (ppl @ [pp_expr ce])
- | CLocalPattern _ ->
- assert false
-and pp_local_decl_expr lde = (* don't know what it is for now *)
- match lde with
- | AssumExpr (_, ce) -> pp_expr ce
- | DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
- (* inductive_expr *)
- let b,e = Loc.unloc l in
- let location = ["begin", string_of_int b; "end", string_of_int e] in
- [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
- begin match cl_or_rdexpr with
- | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
- | RecordDecl (_, ldewwwl) ->
- List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
- end @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end @
- (List.map pp_local_binder lbl)
-and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
- let attrs =
- match optid with
- | None -> []
- | Some (loc, id) ->
- let start, stop = unlock loc in
- ["begin", start; "end", stop ; "name", Id.to_string id] in
- let kind, expr =
- match roe with
- | CStructRec -> "struct", []
- | CWfRec e -> "rec", [pp_expr e]
- | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
- | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
- Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
- (* fixpoint_expr *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* fixpoint name *)
- [pp_recursion_order_expr optid roe] @
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
- (* Nota: it is like fixpoint_expr without (optid, roe)
- * so could be merged if there is no more differences *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* cofixpoint name *)
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
-and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr cpe =
- match cpe with
- | CPatAlias (loc, cpe, id) ->
- xmlApply loc
- (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
- [pp_cases_pattern_expr cpe])
- | CPatCstr (loc, ref, None, cpel2) ->
- xmlApply loc
- (xmlOperator "reference"
- ~attr:["name", Libnames.string_of_reference ref] loc ::
- [Element ("impargs", [], []);
- Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatCstr (loc, ref, Some cpel1, cpel2) ->
- xmlApply loc
- (xmlOperator "reference"
- ~attr:["name", Libnames.string_of_reference ref] loc ::
- [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
- Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatAtom (loc, optr) ->
- let attrs = match optr with
- | None -> []
- | Some r -> ["name", Libnames.string_of_reference r] in
- xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
- | CPatOr (loc, cpel) ->
- xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
- | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
- xmlApply loc
- (xmlOperator "notation" loc ::
- [xmlOperator n loc;
- Element ("subst", [],
- [Element ("subterms", [],
- List.map pp_cases_pattern_expr subst_constr);
- Element ("recsubterms", [],
- List.map
- (fun (cpel) ->
- Element ("recsubterm", [],
- List.map pp_cases_pattern_expr cpel))
- subst_rec)]);
- Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
- | CPatPrim (loc, tok) -> pp_token loc tok
- | CPatRecord (loc, rcl) ->
- xmlApply loc
- (xmlOperator "record" loc ::
- List.map (fun (r, cpe) ->
- Element ("field",
- ["reference", Libnames.string_of_reference r],
- [pp_cases_pattern_expr cpe]))
- rcl)
- | CPatDelimiters (loc, delim, cpe) ->
- xmlApply loc
- (xmlOperator "delimiter" ~attr:["name", delim] loc ::
- [pp_cases_pattern_expr cpe])
- | CPatCast _ -> assert false
-and pp_case_expr (e, name, pat) =
- match name, pat with
- | None, None -> xmlScrutinee [pp_expr e]
- | Some (loc, name), None ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop] [pp_expr e]
- | Some (loc, name), Some p ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop]
- [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
- | None, Some p ->
- xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
-and pp_branch_expr_list bel =
- xmlWith
- (List.map
- (fun (_, cpel, e) ->
- let ppcepl =
- List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
- let ppe = [pp_expr e] in
- xmlCase (ppcepl @ ppe))
- bel)
-and pp_token loc tok =
- let tokstr =
- match tok with
- | String s -> PCData s
- | Numeral n -> PCData (to_string n) in
- xmlToken loc [tokstr]
-and pp_local_binder_list lbl =
- let l = (List.map pp_local_binder lbl) in
- Element ("recurse", (backstep_loc l), l)
-and pp_const_expr_list cel =
- let l = List.map pp_expr cel in
- Element ("recurse", (backstep_loc l), l)
-and pp_expr ?(attr=[]) e =
- match e with
- | CRef (r, _) ->
- xmlCst ~attr
- (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
- | CProdN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CApp (loc, (_, hd), args) ->
- xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
- | CAppExpl (loc, (_, r, _), args) ->
- xmlApply ~attr loc
- (xmlCst (Libnames.string_of_reference r)
- (Libnames.loc_of_reference r) :: List.map pp_expr args)
- | CNotation (loc, notation, ([],[],[])) ->
- xmlOperator notation loc
- | CNotation (loc, notation, (args, cell, lbll)) ->
- let fmts = Notation.find_notation_extra_printing_rules notation in
- let oper = xmlOperator notation loc ~pprules:fmts in
- let cels = List.map pp_const_expr_list cell in
- let lbls = List.map pp_local_binder_list lbll in
- let args = List.map pp_expr args in
- xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
- | CSort(loc, s) ->
- xmlOperator (string_of_glob_sort s) loc
- | CDelimiters (loc, scope, ce) ->
- xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
- [pp_expr ce])
- | CPrim (loc, tok) -> pp_token loc tok
- | CGeneralization (loc, kind, _, e) ->
- let kind= match kind with
- | Explicit -> "explicit"
- | Implicit -> "implicit" in
- xmlApply loc
- (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
- | CCast (loc, e, tc) ->
- begin match tc with
- | CastConv t | CastVM t |CastNative t ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] ::
- [pp_expr e; pp_expr t])
- | CastCoerce ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
- [pp_expr e])
- end
- | CEvar (loc, ek, cel) ->
- let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
- xmlApply loc
- (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
- ppcel)
- | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
- | CHole (loc, _, _, _) -> xmlCst ~attr "_" loc
- | CIf (loc, test, (_, ret), th, el) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "if" loc ::
- return @ [pp_expr th] @ [pp_expr el])
- | CLetTuple (loc, names, (_, ret), value, body) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "lettuple" loc ::
- return @
- (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
- [pp_expr value; pp_expr body])
- | CCases (loc, sty, ret, cel, bel) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "match" loc ~attr:["style", (string_of_case_style sty)] ::
- (return @
- [Element ("scrutinees", [], List.map pp_case_expr cel)] @
- [pp_branch_expr_list bel]))
- | CRecord (_, _) -> assert false
- | CLetIn (loc, (varloc, var), value, typ, body) ->
- let value = match typ with Some t -> CCast (Loc.merge (constr_loc value) (constr_loc t),value, CastConv t) | None -> value in
- xmlApply loc
- (xmlOperator "let" loc ::
- [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
- | CLambdaN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CCoFix (_, _, _) -> assert false
- | CFix (loc, lid, fel) ->
- xmlApply loc
- (xmlOperator "fix" loc ::
- List.flatten (List.map
- (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
- fel))
-
-let pp_comment (c) =
- match c with
- | CommentConstr e -> [pp_expr e]
- | CommentString s -> [Element ("string", [], [PCData s])]
- | CommentInt i -> [PCData (string_of_int i)]
-
-let rec tmpp v loc =
- match v with
- (* Control *)
- | VernacLoad (verbose,f) ->
- xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
- | VernacTime (loc,e) ->
- xmlApply loc (Element("time",[],[]) ::
- [tmpp e loc])
- | VernacRedirect (s, (loc,e)) ->
- xmlApply loc (Element("redirect",["path", s],[]) ::
- [tmpp e loc])
- | VernacTimeout (s,e) ->
- xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
- [tmpp e loc])
- | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
-
- (* Syntax *)
- | VernacSyntaxExtension (_, ((_, name), sml)) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- xmlReservedNotation attrs name loc
-
- | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
- | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
- | VernacDelimiters (name,Some tag) ->
- xmlScope loc "delimit" name ~attr:["delimiter",tag] []
- | VernacDelimiters (name,None) ->
- xmlScope loc "undelimit" name ~attr:[] []
- | VernacInfix (_,((_,name),sml),ce,sn) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacNotation (_, ce, (lstr, sml), sn) ->
- let name = snd lstr in
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacBindScope _ as x -> xmlTODO loc x
- | VernacNotationAddFormat _ as x -> xmlTODO loc x
- | VernacUniverse _
- | VernacConstraint _
- | VernacPolymorphic (_, _) as x -> xmlTODO loc x
- (* Gallina *)
- | VernacDefinition (ldk, ((_,id),_), de) ->
- let l, dk =
- match ldk with
- | Some l, dk -> (l, dk)
- | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
- let e =
- match de with
- | ProveBody (_, ce) -> ce
- | DefineBody (_, Some _, ce, None) -> ce
- | DefineBody (_, None , ce, None) -> ce
- | DefineBody (_, Some _, ce, Some _) -> ce
- | DefineBody (_, None , ce, Some _) -> ce in
- let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
- let str_id = Id.to_string id in
- (xmlDef str_dk str_id loc [pp_expr e])
- | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
- let str_tk = Kindops.string_of_theorem_kind tk in
- let str_id = Id.to_string id in
- (xmlThm str_tk str_id loc [pp_expr statement])
- | VernacStartTheoremProof _ as x -> xmlTODO loc x
- | VernacEndProof pe ->
- begin
- match pe with
- | Admitted -> xmlQed loc
- | Proved (_, Some ((_, id), Some tk)) ->
- let nam = Id.to_string id in
- let typ = Kindops.string_of_theorem_kind tk in
- xmlQed ~attr:["name", nam; "type", typ] loc
- | Proved (_, Some ((_, id), None)) ->
- let nam = Id.to_string id in
- xmlQed ~attr:["name", nam] loc
- | Proved _ -> xmlQed loc
- end
- | VernacExactProof _ as x -> xmlTODO loc x
- | VernacAssumption ((l, a), _, sbwcl) ->
- let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
- let many =
- List.length (List.flatten (List.map fst binders)) > 1 in
- let exprs =
- List.flatten (List.map pp_simple_binder binders) in
- let l = match l with Some x -> x | None -> Decl_kinds.Global in
- let kind = string_of_assumption_kind l a many in
- xmlAssumption kind loc exprs
- | VernacInductive (_, _, iednll) ->
- let kind =
- let (_, _, _, k, _),_ = List.hd iednll in
- begin
- match k with
- | Record -> "Record"
- | Structure -> "Structure"
- | Inductive_kw -> "Inductive"
- | CoInductive -> "CoInductive"
- | Class _ -> "Class"
- | Variant -> "Variant"
- end in
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (ie, dnl) -> (pp_inductive_expr ie) @
- (List.map pp_decl_notation dnl)) iednll) in
- xmlInductive kind loc exprs
- | VernacFixpoint (_, fednll) ->
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
- (List.map pp_decl_notation dnl)) fednll) in
- xmlFixpoint exprs
- | VernacCoFixpoint (_, cfednll) ->
- (* Nota: it is like VernacFixpoint without so could be merged *)
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
- (List.map pp_decl_notation dnl)) cfednll) in
- xmlCoFixpoint exprs
- | VernacScheme _ as x -> xmlTODO loc x
- | VernacCombinedScheme _ as x -> xmlTODO loc x
-
- (* Gallina extensions *)
- | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
- | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
- | VernacNameSectionHypSet _ as x -> xmlTODO loc x
- | VernacRequire (from, import, l) ->
- let import = match import with
- | None -> []
- | Some true -> ["export","true"]
- | Some false -> ["import","true"]
- in
- let from = match from with
- | None -> []
- | Some r -> ["from", Libnames.string_of_reference r]
- in
- xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (true,l) ->
- xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (false,l) ->
- xmlImport loc (List.map (fun ref ->
- xmlReference ref) l)
- | VernacCanonical r ->
- let attr =
- match r with
- | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
- | AN (Ident (_, id)) -> ["id", Id.to_string id]
- | ByNotation (_, s, _) -> ["notation", s] in
- xmlCanonicalStructure attr loc
- | VernacCoercion _ as x -> xmlTODO loc x
- | VernacIdentityCoercion _ as x -> xmlTODO loc x
-
- (* Type classes *)
- | VernacInstance _ as x -> xmlTODO loc x
-
- | VernacContext _ as x -> xmlTODO loc x
-
- | VernacDeclareInstances _ as x -> xmlTODO loc x
-
- | VernacDeclareClass _ as x -> xmlTODO loc x
-
- (* Modules and Module Types *)
- | VernacDeclareModule _ as x -> xmlTODO loc x
- | VernacDefineModule _ as x -> xmlTODO loc x
- | VernacDeclareModuleType _ as x -> xmlTODO loc x
- | VernacInclude _ as x -> xmlTODO loc x
-
- (* Solving *)
-
- | (VernacSolveExistential _) as x ->
- xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Auxiliary file and library management *)
- | VernacAddLoadPath (recf,name,None) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacAddLoadPath (recf,name,Some dp) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name]
- [PCData (Names.DirPath.to_string dp)]
- | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] []
- | VernacAddMLPath (recf,name) ->
- xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
- | VernacChdir _ as x -> xmlTODO loc x
-
- (* State management *)
- | VernacWriteState _ as x -> xmlTODO loc x
- | VernacRestoreState _ as x -> xmlTODO loc x
-
- (* Resetting *)
- | VernacResetName _ as x -> xmlTODO loc x
- | VernacResetInitial as x -> xmlTODO loc x
- | VernacBack _ as x -> xmlTODO loc x
- | VernacBackTo _ -> PCData "VernacBackTo"
-
- (* Commands *)
- | VernacCreateHintDb _ as x -> xmlTODO loc x
- | VernacRemoveHints _ as x -> xmlTODO loc x
- | VernacHints _ as x -> xmlTODO loc x
- | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
- let name = Id.to_string name in
- let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
- xmlNotation attrs name loc [pp_expr ce]
- | VernacDeclareImplicits _ as x -> xmlTODO loc x
- | VernacArguments _ as x -> xmlTODO loc x
- | VernacArgumentsScope _ as x -> xmlTODO loc x
- | VernacReserve _ as x -> xmlTODO loc x
- | VernacGeneralizable _ as x -> xmlTODO loc x
- | VernacSetOpacity _ as x -> xmlTODO loc x
- | VernacSetStrategy _ as x -> xmlTODO loc x
- | VernacUnsetOption _ as x -> xmlTODO loc x
- | VernacSetOption _ as x -> xmlTODO loc x
- | VernacSetAppendOption _ as x -> xmlTODO loc x
- | VernacAddOption _ as x -> xmlTODO loc x
- | VernacRemoveOption _ as x -> xmlTODO loc x
- | VernacMemOption _ as x -> xmlTODO loc x
- | VernacPrintOption _ as x -> xmlTODO loc x
- | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e]
- | VernacGlobalCheck _ as x -> xmlTODO loc x
- | VernacDeclareReduction _ as x -> xmlTODO loc x
- | VernacPrint _ as x -> xmlTODO loc x
- | VernacSearch _ as x -> xmlTODO loc x
- | VernacLocate _ as x -> xmlTODO loc x
- | VernacRegister _ as x -> xmlTODO loc x
- | VernacComments (cl) ->
- xmlComment loc (List.flatten (List.map pp_comment cl))
-
- (* Stm backdoor *)
- | VernacStm _ as x -> xmlTODO loc x
-
- (* Proof management *)
- | VernacGoal _ as x -> xmlTODO loc x
- | VernacAbort _ as x -> xmlTODO loc x
- | VernacAbortAll -> PCData "VernacAbortAll"
- | VernacRestart as x -> xmlTODO loc x
- | VernacUndo _ as x -> xmlTODO loc x
- | VernacUndoTo _ as x -> xmlTODO loc x
- | VernacBacktrack _ as x -> xmlTODO loc x
- | VernacFocus _ as x -> xmlTODO loc x
- | VernacUnfocus as x -> xmlTODO loc x
- | VernacUnfocused as x -> xmlTODO loc x
- | VernacBullet _ as x -> xmlTODO loc x
- | VernacSubproof _ as x -> xmlTODO loc x
- | VernacEndSubproof as x -> xmlTODO loc x
- | VernacShow _ as x -> xmlTODO loc x
- | VernacCheckGuard as x -> xmlTODO loc x
- | VernacProof (tac,using) ->
- let tac = None (** FIXME *) in
- let using = Option.map (xmlSectionSubsetDescr "using") using in
- xmlProof loc (Option.List.(cons tac (cons using [])))
- | VernacProofMode name -> xmlProofMode loc name
-
- (* Toplevel control *)
- | VernacToplevelControl _ as x -> xmlTODO loc x
-
- (* For extension *)
- | VernacExtend _ as x ->
- xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Flags *)
- | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc])
- | VernacLocal (b,e) ->
- xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
- [tmpp e loc])
-
-let tmpp v loc =
- match tmpp v loc with
- | Element("ltac",_,_) as x -> x
- | xml -> xmlGallina loc [xml]
diff --git a/ide/texmacspp.mli b/ide/texmacspp.mli
deleted file mode 100644
index 858847fb6a..0000000000
--- a/ide/texmacspp.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-
-val tmpp : vernac_expr -> Loc.t -> xml
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 3fcb7ce49e..621c46b94a 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -91,8 +91,8 @@ object(self)
let result = GText.view ~packing:r_bin#add () in
views <- (frame#coerce, result, combo#entry) :: views;
let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
- let _ = background_color#connect#changed cb in
- let _ = result#misc#connect#realize (fun () -> cb background_color#get) in
+ let _ = background_color#connect#changed ~callback:cb in
+ let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in
stick text_font result cb;
result#misc#set_can_focus true; (* false causes problems for selection *)
@@ -165,7 +165,7 @@ object(self)
self#new_page_maker;
self#new_query_aux ~grab_now:false ();
frame#misc#hide ();
- let _ = background_color#connect#changed self#refresh_color in
+ let _ = background_color#connect#changed ~callback:self#refresh_color in
self#refresh_color background_color#get;
ignore(notebook#event#connect#key_press ~callback:(fun ev ->
if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true)
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index aeae3e1fdb..3bb6b780e6 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -154,7 +154,7 @@ object (self)
let () = store#clear () in
let iter prop =
let iter = store#append () in
- store#set iter column prop
+ store#set ~row:iter ~column prop
in
let () = current_completion <- (pref, props) in
Proposals.iter iter props
@@ -267,7 +267,7 @@ object (self)
(** Position of view w.r.t. window *)
let (ux, uy) = Gdk.Window.get_position view#misc#window in
(** Relative buffer position to view *)
- let (dx, dy) = view#window_to_buffer_coords `WIDGET 0 0 in
+ let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in
(** Iter position *)
let iter = view#buffer#get_iter pos in
let coords = view#get_iter_location iter in
@@ -397,11 +397,11 @@ object (self)
let () = self#select_first () in
let () = obj#misc#show () in
let () = self#manage_scrollbar () in
- obj#resize 1 1
+ obj#resize ~width:1 ~height:1
method private start_callback off =
let (x, y, w, h) = self#coordinates (`OFFSET off) in
- let () = obj#move x (y + 3 * h / 2) in
+ let () = obj#move ~x ~y:(y + 3 * h / 2) in
()
method private update_callback (off, word, props) =
@@ -433,21 +433,21 @@ object (self)
else false
in
(** Style handling *)
- let _ = view#misc#connect#style_set self#refresh_style in
+ 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 *)
- let _ = model#connect#start_completion self#start_callback in
- let _ = model#connect#update_completion self#update_callback in
- let _ = model#connect#end_completion self#end_callback in
+ 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 *)
- let _ = view#event#connect#key_press key_cb in
+ let _ = view#event#connect#key_press ~callback:key_cb in
(** Hiding the popup when necessary*)
- let _ = view#misc#connect#hide obj#misc#hide in
- let _ = view#event#connect#button_press (fun _ -> self#hide (); false) in
- let _ = view#connect#move_cursor move_cb in
- let _ = view#event#connect#focus_out (fun _ -> self#hide (); false) in
+ 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
+ let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in
()
end
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml
index 3d1b63dfae..cbc34462e2 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/wg_Detachable.ml
@@ -26,8 +26,8 @@ class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) =
val mutable attached_cb = (fun _ -> ())
method child = frame#child
- method add = frame#add
- method pack ?from ?expand ?fill ?padding w =
+ method! add = frame#add
+ method! pack ?from ?expand ?fill ?padding w =
if frame#all_children = [] then self#add w
else raise (Invalid_argument "detachable#pack")
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 3d847ddcc1..f84b9063bf 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -186,8 +186,8 @@ class finder name (view : GText.view) =
in
let find_cb = generic_cb self#hide self#find_forward in
let replace_cb = generic_cb self#hide self#replace in
- let _ = find_entry#event#connect#key_press find_cb in
- let _ = replace_entry#event#connect#key_press replace_cb in
+ let _ = find_entry#event#connect#key_press ~callback:find_cb in
+ let _ = replace_entry#event#connect#key_press ~callback:replace_cb in
(** TextView interaction *)
let view_cb ev =
@@ -197,7 +197,7 @@ class finder name (view : GText.view) =
else false
else false
in
- let _ = view#event#connect#key_press view_cb in
+ let _ = view#event#connect#key_press ~callback:view_cb in
()
end
diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index 08d7d19833..0e5284c2f9 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/wg_Notebook.ml
@@ -50,7 +50,7 @@ object(self)
method pages = term_list
- method remove_page index =
+ method! remove_page index =
term_list <- Util.List.filteri (fun i x -> if i = index then kill_page x; i <> index) term_list;
super#remove_page index
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 3cbe583881..0bf5afbfdb 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -47,7 +47,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb =
hover_cb start stop; false
| _ -> false))
-let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
+let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = match goals with
| [] -> assert false
| { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: rem_goals ->
let on_hover sel_start sel_stop =
@@ -65,8 +65,11 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
let head_str = Printf.sprintf
"%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "")
in
- let goal_str index total = Printf.sprintf
- "______________________________________(%d/%d)\n" index total
+ let goal_str ?(shownum=false) index total =
+ if shownum then Printf.sprintf
+ "______________________________________(%d/%d)\n" index total
+ else Printf.sprintf
+ "______________________________________\n"
in
(* Insert current goal and its hypotheses *)
let hyps_hints, goal_hints = match hints with
@@ -97,18 +100,29 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
[tag]
else []
in
- proof#buffer#insert (goal_str 1 goals_cnt);
+ proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt);
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);
+ let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g } =
+ proof#buffer#insert (goal_str ~shownum i goals_cnt);
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
-
+ let () = Util.List.fold_left_i (fold_goal ~shownum:true) 2 () rem_goals in
+ (* show unfocused goal if option set *)
+ (* Insert remaining goals (no hypotheses) *)
+ if Coq.PrintOpt.printing_unfocused () then
+ begin
+ ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter));
+ let unfoc = List.flatten (List.rev (List.map (fun (x,y) -> x@y) unfoc_goals)) in
+ if unfoc<>[] then
+ begin
+ proof#buffer#insert "\nUnfocused Goals:\n";
+ Util.List.fold_left_i (fold_goal ~shownum:false) 0 () unfoc
+ end
+ end;
ignore(proof#buffer#place_cursor
~where:(proof#buffer#end_iter#backward_to_tag_toggle
(Some Tags.Proof.goal)));
@@ -172,8 +186,9 @@ let display mode (view : #GText.view_skel) goals hints evars =
in
List.iteri iter bg
end
- | Some { Interface.fg_goals = fg } ->
- mode view fg hints
+ | Some { Interface.fg_goals = fg; bg_goals = bg } ->
+ mode view fg ~unfoc_goals:bg hints
+
let proof_view () =
let buffer = GSourceView2.source_buffer
@@ -188,8 +203,8 @@ let proof_view () =
let default_clipboard = GData.clipboard Gdk.Atom.primary in
let _ = buffer#add_selection_clipboard default_clipboard in
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;
@@ -226,5 +241,5 @@ let proof_view () =
(* Is there a better way to connect the signal ? *)
(* Can this be done in the object constructor? *)
let w_cb _ = pf#refresh ~force:false in
- ignore (view#misc#connect#size_allocate w_cb);
+ ignore (view#misc#connect#size_allocate ~callback:w_cb);
pf
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 218cedb363..7430f07d47 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -301,28 +301,28 @@ object (self)
~use_align:false ~yalign:0.75 ~within_margin:0.25 `INSERT
(* HACK: missing gtksourceview features *)
- method right_margin_position =
+ method! right_margin_position =
let prop = {
Gobject.name = "right-margin-position";
conv = Gobject.Data.int;
} in
Gobject.get prop obj
- method set_right_margin_position pos =
+ method! set_right_margin_position pos =
let prop = {
Gobject.name = "right-margin-position";
conv = Gobject.Data.int;
} in
Gobject.set prop obj pos
- method show_right_margin =
+ method! show_right_margin =
let prop = {
Gobject.name = "show-right-margin";
conv = Gobject.Data.boolean;
} in
Gobject.get prop obj
- method set_show_right_margin show =
+ method! set_show_right_margin show =
let prop = {
Gobject.name = "show-right-margin";
conv = Gobject.Data.boolean;
@@ -460,8 +460,8 @@ object (self)
let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in
(** Plug on preferences *)
let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in
- let _ = background_color#connect#changed cb in
- let _ = self#misc#connect#realize (fun () -> cb background_color#get) in
+ let _ = background_color#connect#changed ~callback:cb in
+ let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
let cb b = self#set_wrap_mode (if b then `WORD else `NONE) in
stick dynamic_word_wrap self cb;
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index dbc1740ef6..d527a0d13a 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -75,7 +75,7 @@ object (self)
self#redraw ();
end
in
- let _ = box#misc#connect#size_allocate cb in
+ let _ = box#misc#connect#size_allocate ~callback:cb in
let clicked_cb ev = match model with
| None -> true
| Some md ->
@@ -86,7 +86,7 @@ object (self)
let () = clicked#call idx in
true
in
- let _ = eventbox#event#connect#button_press clicked_cb in
+ 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 *)
@@ -102,7 +102,7 @@ object (self)
| `SET (i, color) ->
if self#misc#visible then self#fill_range color i (i + 1)
in
- md#changed changed_cb
+ md#changed ~callback:changed_cb
method private fill_range color i j = match model with
| None -> ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 05:50:17 +0000