aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/coqide.ml5
-rw-r--r--ide/tags.ml1
-rw-r--r--toplevel/coqtop.ml4
3 files changed, 6 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 4b08f4b9b..fb7b92d71 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1515,8 +1515,7 @@ object(self)
ignore (input_buffer#add_selection_clipboard cb);
ignore (proof_buffer#add_selection_clipboard cb);
ignore (message_buffer#add_selection_clipboard cb);
- let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "purple"] in
- self#electric_paren paren_highlight_tag;
+ self#electric_paren Tags.Script.paren;
ignore (input_buffer#connect#after#mark_set
~callback:(fun it (m:Gtk.text_mark) ->
!set_location
@@ -1528,7 +1527,7 @@ object(self)
input_buffer#remove_tag
~start:input_buffer#start_iter
~stop:input_buffer#end_iter
- paren_highlight_tag;
+ Tags.Script.paren;
| Some s ->
prerr_endline (s^" moved")
| None -> () )
diff --git a/ide/tags.ml b/ide/tags.ml
index b0b9dc6fb..826fcd962 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -30,6 +30,7 @@ struct
let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false]
let locked = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"]
+ let paren = make_tag table ~name:"paren" [`BACKGROUND "purple"]
end
module Proof =
struct
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e00c56a14..a88ee3ba6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -374,10 +374,12 @@ let init is_ide =
exit 0);
Lib.declare_initial_state ()
+let init_toplevel () = init false
+
let init_ide () = init true; List.rev !ide_args
let start () =
- init false;
+ init_toplevel ();
Toplevel.loop();
(* Initialise and launch the Ocaml toplevel *)
Coqinit.init_ocaml_path();