diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 19 | ||||
| -rw-r--r-- | ide/coqide.mli | 2 | ||||
| -rw-r--r-- | ide/coqide_main.ml4 | 1 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 58 | ||||
| -rw-r--r-- | ide/tags.ml | 25 | ||||
| -rw-r--r-- | ide/tags.mli | 1 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 7 |
8 files changed, 50 insertions, 65 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 0dd08293c8..ded28a998e 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -422,7 +422,7 @@ object(self) let rec eat_feedback n = if n = 0 then true else let msg = Queue.pop feedbacks in - let id = msg.id in + let id = msg.span_id in let sentence = let finder _ state_id s = match state_id, id with diff --git a/ide/coqide.ml b/ide/coqide.ml index 2c8ce0049e..842d068592 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1325,25 +1325,6 @@ let main files = Minilib.log "End of Coqide.main" -(** {2 Geoproof } *) - -(** This function check every tenth of second if GeoProof has send - something on his private clipboard *) - -let check_for_geoproof_input () = - let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in - let handler () = match cb_Dr#text with - |None -> true - |Some "Ack" -> true - |Some s -> - on_current_term (fun sn -> sn.buffer#insert (s ^ "\n")); - (* cb_Dr#clear does not work so i use : *) - cb_Dr#set_text "Ack"; - true - in - ignore (GMain.Timeout.add ~ms:100 ~callback:handler) - - (** {2 Argument parsing } *) (** By default, the coqtop we try to launch is exactly the current coqide diff --git a/ide/coqide.mli b/ide/coqide.mli index 39b4d9ae2f..42dab9ec55 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -40,5 +40,3 @@ val set_signal_handlers : unit -> unit (** Emergency saving of opened files as "foo.v.crashcoqide", and exit (if the integer isn't 127). *) val crash_save : int -> unit - -val check_for_geoproof_input : unit -> unit diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 73a30b18f1..8d99cc3e66 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -142,7 +142,6 @@ let () = Coq.check_connection args; Coqide.sup_args := args; Coqide.main files; - if !Coq_config.with_geoproof then Coqide.check_for_geoproof_input (); os_specific_init (); try GMain.main (); diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index f00b1e1421..7cbab56d44 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -76,10 +76,16 @@ let ide_cmd_checks ~id (loc,ast) = (** Interpretation (cf. [Ide_intf.interp]) *) +let ide_doc = ref None +let get_doc () = Option.get !ide_doc +let set_doc doc = ide_doc := Some doc + let add ((s,eid),(sid,verbose)) = + let doc = get_doc () 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 loc_ast = Stm.parse_sentence ~doc sid pa in + let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in + set_doc doc; 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 @@ -94,9 +100,10 @@ let add ((s,eid),(sid,verbose)) = newid, (rc, "") let edit_at id = - match Stm.edit_at id with - | `NewTip -> CSig.Inl () - | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip)) + let doc = get_doc () in + match Stm.edit_at ~doc id with + | doc, `NewTip -> set_doc doc; CSig.Inl () + | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip)) (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. @@ -109,12 +116,14 @@ let edit_at id = *) let query (route, (s,id)) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Stm.query ~at:id ~route pa + let doc = get_doc () in + Stm.query ~at:id ~doc ~route pa let annotate phrase = + let doc = get_doc () in let (loc, ast) = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in - Stm.parse_sentence (Stm.get_current_state ()) pa + Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa in (* XXX: Width should be a parameter of annotate... *) Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) @@ -196,7 +205,8 @@ let export_pre_goals pgs = } let goals () = - Stm.finish (); + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; try let pfts = Proof_global.give_me_the_proof () in Some (export_pre_goals (Proof.map_structured_proof pfts process_goal)) @@ -204,7 +214,8 @@ let goals () = let evars () = try - Stm.finish (); + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in @@ -230,12 +241,17 @@ let hints () = (** Other API calls *) +let wait () = + let doc = get_doc () in + set_doc (Stm.wait ~doc) + let status force = (** We remove the initial part of the current [DirPath.t] (usually Top in an interactive session, cf "coqtop -top"), and display the other parts (opened sections and modules) *) - Stm.finish (); - if force then Stm.join (); + set_doc (Stm.finish ~doc:(get_doc ())); + if force then + set_doc (Stm.join ~doc:(get_doc ())); let path = let l = Names.DirPath.repr (Lib.cwd ()) in List.rev_map Names.Id.to_string l @@ -252,7 +268,7 @@ let status force = Interface.status_path = path; Interface.status_proofname = proof; Interface.status_allproofs = allproofs; - Interface.status_proofnum = Stm.current_proof_depth (); + Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); } let export_coq_object t = { @@ -356,22 +372,23 @@ let init = fun file -> if !initialized then anomaly (str "Already initialized.") else begin - let init_sid = Stm.get_current_state () in + let init_sid = Stm.get_current_state ~doc:(get_doc ()) in initialized := true; match file with | None -> init_sid | Some file -> let dir = Filename.dirname file in let open Loadpath in let open CUnix in - let initial_id, _ = + let doc, initial_id, _ = + let doc = get_doc () 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 + let loc_ast = Stm.parse_sentence ~doc init_sid pa in + Stm.add false ~doc ~ontop:init_sid loc_ast + end else doc, init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; - Stm.finish (); + set_doc (Stm.finish ~doc); initial_id end @@ -413,7 +430,7 @@ let eval_call c = Interface.quit = (fun () -> quit := true); Interface.init = interruptible init; Interface.about = interruptible about; - Interface.wait = interruptible Stm.wait; + Interface.wait = interruptible wait; Interface.interp = interruptible interp; Interface.handle_exn = handle_exn; Interface.stop_worker = Stm.stop_worker; @@ -449,7 +466,8 @@ let msg_format = ref (fun () -> Xmlprotocol.Richpp margin ) -let loop () = +let loop doc = + set_doc doc; init_signal_handler (); catch_break := false; let in_ch, out_ch = Spawned.get_channels () in diff --git a/ide/tags.ml b/ide/tags.ml index 08ca47a842..4020271798 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -15,33 +15,22 @@ let make_tag (tt:GText.tag_table) ~name prop = module Script = struct + (* More recently defined tags have highest priority in case of overlapping *) let table = GText.tag_table () - let comment = make_tag table ~name:"comment" [] - let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"] + let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] let error_bg = make_tag table ~name:"error_bg" [] let to_process = make_tag table ~name:"to_process" [] let processed = make_tag table ~name:"processed" [] - let incomplete = make_tag table ~name:"incomplete" [ - `BACKGROUND_STIPPLE_SET true; - ] + let incomplete = make_tag table ~name:"incomplete" [`BACKGROUND_STIPPLE_SET true] let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"] - let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"] - let sentence = make_tag table ~name:"sentence" [] let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) - let ephemere = [error; warning; error_bg; tooltip; processed; to_process; incomplete; unjustified] - - let all = - comment :: found :: sentence :: ephemere - - let edit_zone = - let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in - t#set_priority (List.length all); - t - let all = edit_zone :: all - + let comment = make_tag table ~name:"comment" [] + let sentence = make_tag table ~name:"sentence" [] + let edit_zone = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] (* for debugging *) + let all = edit_zone :: comment :: sentence :: ephemere end module Proof = struct diff --git a/ide/tags.mli b/ide/tags.mli index 265dfe46e3..15a35185df 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -17,7 +17,6 @@ sig val processed : GText.tag val incomplete : GText.tag val unjustified : GText.tag - val found : GText.tag val sentence : GText.tag val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index b452b0a13f..aaa24a2a95 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -939,7 +939,7 @@ let of_edit_or_state_id id = ["object","state"], of_stateid id let of_feedback msg = let content = of_feedback_content msg.contents in - let obj, id = of_edit_or_state_id msg.id in + let obj, id = of_edit_or_state_id msg.span_id in let route = string_of_int msg.route in Element ("feedback", obj @ ["route",route], [id;content]) @@ -947,8 +947,9 @@ let of_feedback msg_fmt = msg_format := msg_fmt; of_feedback let to_feedback xml = match xml with - | Element ("feedback", ["object","state";"route",route], [id;content]) -> { - id = to_stateid id; + | Element ("feedback", ["object","state";"route",route], [id;content]) -> { + doc_id = 0; + span_id = to_stateid id; route = int_of_string route; contents = to_feedback_content content } | x -> raise (Marshal_error("feedback",x)) |