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.ml78
-rw-r--r--ide/coqide.ml10
-rw-r--r--ide/coqide_ui.ml285
-rw-r--r--ide/ide_slave.ml87
-rw-r--r--ide/ideutils.ml13
-rw-r--r--ide/interface.mli6
-rw-r--r--ide/preferences.ml22
-rw-r--r--ide/session.ml14
-rw-r--r--ide/texmacspp.ml3
-rw-r--r--ide/wg_Command.ml19
-rw-r--r--ide/wg_Command.mli2
-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
-rw-r--r--ide/xmlprotocol.ml10
21 files changed, 316 insertions, 338 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 3d6a2583fe..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 =
@@ -366,6 +363,9 @@ object(self)
(* This method is intended to perform stateless commands *)
method raw_coq_query phrase =
+ let sid = try Document.tip document
+ with Document.Empty -> Stateid.initial
+ in
let action = log "raw_coq_query starting now" in
let display_error s =
if not (validate s) then
@@ -373,11 +373,10 @@ object(self)
else messages#add s;
in
let query =
- Coq.query (phrase,Stateid.dummy) in
+ Coq.query (phrase,sid) in
let next = function
| Fail (_, _, err) -> display_error err; Coq.return ()
- | Good msg ->
- messages#add_string msg; Coq.return ()
+ | Good msg -> Coq.return ()
in
Coq.bind (Coq.seq action query) next
@@ -414,16 +413,9 @@ object(self)
buffer#apply_tag Tags.Script.tooltip ~start ~stop;
add_tooltip sentence pre post markup
- method private is_dummy_id id =
- match id with
- | Edit 0 -> true
- | State id when Stateid.equal id Stateid.dummy -> true
- | _ -> false
-
method private enqueue_feedback msg =
- (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *)
- let id = msg.id in
- if self#is_dummy_id id then () else Queue.add msg feedbacks
+ (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt Xmlprotocol.(of_feedback Ppcmds msg)); *)
+ Queue.add msg feedbacks
method private process_feedback () =
let rec eat_feedback n =
@@ -433,46 +425,45 @@ object(self)
let sentence =
let finder _ state_id s =
match state_id, id with
- | Some id', State id when Stateid.equal id id' -> Some (state_id, s)
- | _, Edit id when id = s.edit_id -> Some (state_id, s)
+ | Some id', id when Stateid.equal id id' -> Some (state_id, s)
| _ -> None in
try Some (Doc.find_map document finder)
with Not_found -> None in
- let log_pp s state_id =
+ let log_pp ?id s=
Minilib.log_pp Pp.(seq
- [str "Feedback "; s; str " on ";
- str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in
- let log s state_id = log_pp (Pp.str s) state_id in
+ [str "Feedback "; s; pr_opt (fun id -> str " on " ++ str (Stateid.to_string id)) id])
+ in
+ let log ?id s = log_pp ?id (Pp.str s) in
begin match msg.contents, sentence with
| AddedAxiom, Some (id,sentence) ->
- log "AddedAxiom" id;
+ log ?id "AddedAxiom";
remove_flag sentence `PROCESSING;
remove_flag sentence `ERROR;
add_flag sentence `UNSAFE;
self#mark_as_needed sentence
| Processed, Some (id,sentence) ->
- log "Processed" id;
+ log ?id "Processed" ;
remove_flag sentence `PROCESSING;
self#mark_as_needed sentence
| ProcessingIn _, Some (id,sentence) ->
- log "ProcessingIn" id;
+ log ?id "ProcessingIn";
add_flag sentence `PROCESSING;
self#mark_as_needed sentence
| Incomplete, Some (id, sentence) ->
- log "Incomplete" id;
+ log ?id "Incomplete";
add_flag sentence `INCOMPLETE;
self#mark_as_needed sentence
| Complete, Some (id, sentence) ->
- log "Complete" id;
+ log ?id "Complete";
remove_flag sentence `INCOMPLETE;
self#mark_as_needed sentence
| GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) ->
- log "GlobRef" id;
+ log ?id "GlobRef";
self#attach_tooltip ~loc sentence
(Printf.sprintf "%s %s %s" filepath ident ty)
| Message(Error, loc, msg), Some (id,sentence) ->
let uloc = Option.default Loc.ghost loc in
- log_pp Pp.(str "ErrorMsg" ++ msg) id;
+ log_pp ?id Pp.(str "ErrorMsg" ++ msg);
remove_flag sentence `PROCESSING;
let rmsg = Pp.string_of_ppcmds msg in
add_flag sentence (`ERROR (uloc, rmsg));
@@ -481,32 +472,33 @@ object(self)
self#position_tag_at_sentence ?loc Tags.Script.error sentence
| Message(Warning, loc, msg), Some (id,sentence) ->
let uloc = Option.default Loc.ghost loc in
- log_pp Pp.(str "WarningMsg" ++ msg) id;
+ log_pp ?id Pp.(str "WarningMsg" ++ msg);
let rmsg = Pp.string_of_ppcmds msg in
add_flag sentence (`WARNING (uloc, rmsg));
self#attach_tooltip sentence ?loc rmsg;
self#position_tag_at_sentence ?loc Tags.Script.warning sentence;
messages#push Warning msg
| Message(lvl, loc, msg), Some (id,sentence) ->
- log_pp Pp.(str "Msg" ++ msg) id;
+ log_pp ?id Pp.(str "Msg" ++ msg);
+ messages#push lvl msg
+ | Message(lvl, loc, msg), None ->
+ log_pp Pp.(str "Msg" ++ msg);
messages#push lvl msg
| InProgress n, _ ->
if n < 0 then processed <- processed + abs n
else to_process <- to_process + n
| WorkerStatus(id,status), _ ->
- log "WorkerStatus" None;
+ log "WorkerStatus";
slaves_status <- CString.Map.add id status slaves_status
-
| _ ->
if sentence <> None then Minilib.log "Unsupported feedback message"
else if Doc.is_empty document then ()
else
try
match id, Doc.tip document with
- | Edit _, _ -> ()
- | State id1, id2 when Stateid.newer_than id2 id1 -> ()
+ | id1, id2 when Stateid.newer_than id2 id1 -> ()
| _ -> Queue.add msg feedbacks
- with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks
+ with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks
end;
eat_feedback (n-1)
in
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/ide_slave.ml b/ide/ide_slave.ml
index 0dfa03cca0..56ada9d132 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -8,6 +8,7 @@
(************************************************************************)
open Vernacexpr
+open Vernacprop
open CErrors
open Util
open Pp
@@ -53,50 +54,36 @@ 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)
| VernacUnsetOption o -> coqide_known_option o
| _ -> false
-let is_debug cmd = match cmd with
- | VernacSetOption (["Ltac";"Debug"], _) -> true
- | _ -> false
-
-let is_query cmd = match cmd with
- | VernacChdir None
- | VernacMemOption _
- | VernacPrintOption _
- | VernacCheckMayEval _
- | VernacGlobalCheck _
- | VernacPrint _
- | VernacSearch _
- | VernacLocate _ -> true
- | _ -> false
-
-let is_undo cmd = match cmd with
- | VernacUndo _ | VernacUndoTo _ -> true
- | _ -> false
-
(** Check whether a command is forbidden in the IDE *)
-let ide_cmd_checks (loc,ast) =
+let ide_cmd_checks ~id (loc,ast) =
let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in
+ let warn msg = Feedback.(feedback ~id (Message (Warning, Some loc, strbrk msg))) in
if is_debug ast then
user_error "Debug mode not available in the IDE";
if is_known_option ast then
- Feedback.msg_warning (strbrk "Set this option from the IDE menu instead");
- if Vernac.is_navigation_vernac ast || is_undo ast then
- Feedback.msg_warning (strbrk "Use IDE navigation instead");
+ warn "Set this option from the IDE menu instead";
+ if is_navigation_vernac ast || is_undo ast then
+ warn "Use IDE navigation instead";
if is_query ast then
- Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts")
+ warn "Query commands should not be inserted in scripts"
(** Interpretation (cf. [Ide_intf.interp]) *)
let add ((s,eid),(sid,verbose)) =
- let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in
+ let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+ 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 ~id:newid loc_ast;
(* TODO: the "" parameter is a leftover of the times the protocol
* used to include stderr/stdout output.
*
@@ -122,12 +109,14 @@ let edit_at id =
* as not to break the core protocol for this minor change, but it should
* be removed in the next version of the protocol.
*)
-let query (s,id) = Stm.query ~at:id s; ""
+let query (s,id) =
+ let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+ Stm.query ~at:id pa; ""
let annotate phrase =
let (loc, ast) =
let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
- Vernac.parse_sentence (pa,None)
+ Stm.parse_sentence (Stm.get_current_state ()) pa
in
(* XXX: Width should be a parameter of annotate... *)
Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
@@ -370,43 +359,28 @@ let init =
fun file ->
if !initialized then anomaly (str "Already initialized")
else begin
+ let init_sid = Stm.get_current_state () in
initialized := true;
match file with
- | None -> Stm.get_current_state ()
+ | None -> init_sid
| Some file ->
let dir = Filename.dirname file in
let open Loadpath in let open CUnix in
let initial_id, _ =
- if not (is_in_load_paths (physical_path_of_string dir)) then
- Stm.add false ~ontop:(Stm.get_current_state ())
- 0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
- else Stm.get_current_state (), `NewTip in
+ if not (is_in_load_paths (physical_path_of_string dir)) then begin
+ let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in
+ let loc_ast = Stm.parse_sentence init_sid pa in
+ Stm.add false ~ontop:init_sid loc_ast
+ end else init_sid, `NewTip in
if Filename.check_suffix file ".v" then
Stm.set_compilation_hints file;
Stm.finish ();
initial_id
end
-(* Retrocompatibility stuff *)
+(* Retrocompatibility stuff, disabled since 8.7 *)
let interp ((_raw, verbose), s) =
- let vernac_parse s =
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
- Flags.with_option Flags.we_are_parsing (fun () ->
- match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
- | None -> raise (Invalid_argument "vernac_parse")
- | Some ast -> ast)
- () in
- Stm.interp verbose (vernac_parse s);
- (* TODO: the "" parameter is a leftover of the times the protocol
- * used to include stderr/stdout output.
- *
- * Currently, we force all the output meant for the to go via the
- * feedback mechanism, and we don't manipulate stderr/stdout, which
- * are left to the client's discrection. The parameter is still there
- * as not to break the core protocol for this minor change, but it should
- * be removed in the next version of the protocol.
- *)
- Stm.get_current_state (), CSig.Inl ""
+ Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add."
(** 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
@@ -494,9 +468,6 @@ let loop () =
let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
let () = Xml_parser.check_eof xml_ic false in
ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));
- (* We'll handle goal fetching and display in our own way *)
- Vernacentries.enable_goal_printing := false;
- Vernacentries.qed_display_script := false;
while not !quit do
try
let xml_query = Xml_parser.parse xml_ic in
@@ -535,12 +506,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/interface.mli b/ide/interface.mli
index 9ed6062588..62f63aefb9 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -111,8 +111,10 @@ type coq_info = {
(** Calls result *)
type location = (int * int) option (* start and end of the error *)
-type state_id = Feedback.state_id
-type edit_id = Feedback.edit_id
+type state_id = Stateid.t
+
+(* Obsolete *)
+type edit_id = int
(* The fail case carries the current state_id of the prover, the GUI
should probably retract to that point *)
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 fc6340d283..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
@@ -386,12 +386,12 @@ let create file coqtop_args =
let proof = create_proof () in
let messages = create_messages () in
let segment = new Wg_Segment.segment () in
- let command = new Wg_Command.command_window basename coqtop in
let finder = new Wg_Find.finder basename (script :> GText.view) in
let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
let _ = fops#update_stats in
let cops =
new CoqOps.coqops script proof messages segment coqtop (fun () -> fops#filename) in
+ let command = new Wg_Command.command_window basename coqtop cops in
let errpage = create_errpage script in
let jobpage = create_jobpage coqtop cops in
let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e787e48bf1..05f1820cf2 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -504,7 +504,6 @@ let rec tmpp v loc =
xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
[tmpp e loc])
| VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
- | VernacError _ -> xmlWithLoc loc "error" [] []
(* Syntax *)
| VernacSyntaxExtension (_, ((_, name), sml)) ->
@@ -553,7 +552,7 @@ let rec tmpp v loc =
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) ->
+ | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement) ], 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])
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 47dad8f196..621c46b94a 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -8,7 +8,7 @@
open Preferences
-class command_window name coqtop =
+class command_window name coqtop coqops =
let frame = Wg_Detachable.detachable
~title:(Printf.sprintf "Query pane (%s)" name) () in
let _ = frame#hide in
@@ -26,6 +26,11 @@ object(self)
val notebook = notebook
+ (* We need access to coqops in order to place queries in the proper
+ document stint. This should remove access from this module to the
+ low-level Coq one. *)
+ val coqops = coqops
+
method pack_in (f : GObj.widget -> unit) = f frame#coerce
val mutable new_page : GObj.widget = (GMisc.label ())#coerce
@@ -86,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 *)
@@ -101,7 +106,10 @@ object(self)
else com ^ " " ^ arg ^" . "
in
let process =
- Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
+ (* We need to adapt this to route_id and redirect to the result buffer below *)
+ coqops#raw_coq_query phrase
+ (*
+ Coq.bind (Coq.query (phrase,sid)) (function
| Interface.Fail (_,l,str) ->
let width = Ideutils.textview_width result in
Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str);
@@ -111,6 +119,7 @@ object(self)
result#buffer#insert res;
notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
Coq.return ())
+ *)
in
result#buffer#set_text ("Result for command " ^ phrase ^ ":\n");
Coq.try_grab coqtop process ignore
@@ -156,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_Command.mli b/ide/wg_Command.mli
index fa50ba5fdd..341322be1b 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-class command_window : string -> Coq.coqtop ->
+class command_window : string -> Coq.coqtop -> CoqOps.coqops ->
object
method new_query : ?command:string -> ?term:string -> unit -> unit
method pack_in : (GObj.widget -> unit) -> unit
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 -> ()
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d7950e5fd5..bf52b0b52b 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -907,9 +907,7 @@ let of_feedback_content = function
of_string filename ]
| Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ]
-let of_edit_or_state_id = function
- | Edit id -> ["object","edit"], of_edit_id id
- | State id -> ["object","state"], of_stateid id
+let of_edit_or_state_id id = ["object","state"], of_stateid id
let of_feedback msg =
let content = of_feedback_content msg.contents in
@@ -921,12 +919,8 @@ let of_feedback msg_fmt =
msg_format := msg_fmt; of_feedback
let to_feedback xml = match xml with
- | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
- id = Edit(to_edit_id id);
- route = int_of_string route;
- contents = to_feedback_content content }
| Element ("feedback", ["object","state";"route",route], [id;content]) -> {
- id = State(to_stateid id);
+ id = to_stateid id;
route = int_of_string route;
contents = to_feedback_content content }
| x -> raise (Marshal_error("feedback",x))
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 01:02:44 +0000