Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 120 insertions, 111 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 009a1989..61280fd9 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -27,7 +27,6 @@ let safety_tag = function
 class type analyzed_views=
 object
   val mutable act_id : GtkSignal.id option
-  val mutable deact_id : GtkSignal.id option
   val input_buffer : GText.buffer
   val input_view : Undo.undoable_view
   val last_array : string array
@@ -65,7 +64,6 @@ object
   method backtrack_to : GText.iter -> unit
   method backtrack_to_no_lock : GText.iter -> unit
   method clear_message : unit
-  method disconnected_keypress_handler : GdkEvent.Key.t -> bool
   method find_phrase_starting_at :
     GText.iter -> (GText.iter * GText.iter) option
   method get_insert : GText.iter
@@ -84,6 +82,7 @@ object
   method reset_initial : unit
   method force_reset_initial : unit
   method set_message : string -> unit
+  method raw_coq_query : string -> unit
   method show_goals : unit
   method show_goals_full : unit
   method undo_last_step : unit
@@ -889,11 +888,32 @@ object(self)
         raise RestartCoqtop
       | e -> sync display_error (None, Printexc.to_string e); None
 
+  (* This method is intended to perform stateless commands *)
+  method raw_coq_query phrase =
+    let () = prerr_endline "raw_coq_query starting now" in
+    let display_error s =
+      if not (Glib.Utf8.validate s) then
+        flash_info "This error is so nasty that I can't even display it."
+      else begin
+        self#insert_message s;
+        message_view#misc#draw None
+      end
+    in
+    try
+      match Coq.interp !mycoqtop ~raw:true ~verbose:false phrase with
+      | Interface.Fail (_, err) -> sync display_error err
+      | Interface.Good msg -> sync self#insert_message msg
+    with
+    | End_of_file -> raise RestartCoqtop
+    | e -> sync display_error (Printexc.to_string e)
+
   method find_phrase_starting_at (start:GText.iter) =
     try
       let start = grab_sentence_start start self#get_start_of_input in
       let stop = grab_sentence_stop start in
-      if is_sentence_end stop#backward_char then Some (start,stop)
+      (* Is this phrase non-empty and complete ? *)
+      if stop#compare start > 0 && is_sentence_end stop#backward_char
+      then Some (start,stop)
       else None
     with Not_found -> None
 
@@ -1217,22 +1237,6 @@ object(self)
     let state = GdkEvent.Key.state k in
     begin
       match  state with
-        | l when List.mem `MOD1 l ->
-          let k = GdkEvent.Key.keyval k in
-          if GdkKeysyms._Return=k
-          then ignore(
-            if (input_buffer#insert_interactive "\n") then
-              begin
-                let i= self#get_insert#backward_word_start in
-                prerr_endline "active_kp_hf: Placing cursor";
-                self#process_until_iter_or_error i
-              end);
-          true
-        | l when List.mem `CONTROL l ->
-          let k = GdkEvent.Key.keyval k in
-          if GdkKeysyms._Break=k
-          then break ();
-          false
         | l ->
           if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
             prerr_endline "active_kp_handler for Tab";
@@ -1241,18 +1245,6 @@ object(self)
           end else false
     end
 
-
-  method disconnected_keypress_handler k =
-    match GdkEvent.Key.state k with
-      | l when List.mem `CONTROL l ->
-        let k = GdkEvent.Key.keyval k in
-        if GdkKeysyms._c=k
-        then break ();
-        false
-      | l -> false
-
-
-  val mutable deact_id = None
   val mutable act_id = None
 
   method activate () = if not is_active then begin
@@ -1523,9 +1515,15 @@ let create_session file =
   script#buffer#place_cursor ~where:(script#buffer#start_iter);
   proof#misc#set_can_focus true;
   message#misc#set_can_focus true;
+  (* setting fonts *)
   script#misc#modify_font !current.text_font;
   proof#misc#modify_font !current.text_font;
   message#misc#modify_font !current.text_font;
+  (* setting colors *)
+  script#misc#modify_base [`NORMAL, `NAME !current.background_color];
+  proof#misc#modify_base [`NORMAL, `NAME !current.background_color];
+  message#misc#modify_base [`NORMAL, `NAME !current.background_color];
+
   { tab_label=basename;
     filename=begin match file with None -> "" |Some f -> f end;
     script=script;
@@ -1798,12 +1796,6 @@ let forbid_quit_to_save () =
 	else false)
 
 let main files =
-  (* Statup preferences *)
-  begin
-    try load_pref ()
-    with e ->
-      flash_info ("Could not load preferences ("^Printexc.to_string e^").");
-  end;
 
   (* Main window *)
   let w = GWindow.window
@@ -1823,9 +1815,9 @@ let main files =
   let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
 
   let new_f _ =
-    match select_file_for_save ~title:"Create file" () with
-      | None -> ()
-      | Some f -> do_load f
+    let session = create_session None in
+    let index = session_notebook#append_term session in
+    session_notebook#goto_page index
   in
   let load_f _ =
     match select_file_for_open ~title:"Load file" () with
@@ -2181,6 +2173,7 @@ let main files =
 	     true))
   in reset_auto_save_timer (); (* to enable statup preferences timer *)
 (* end Preferences *)
+
   let do_or_activate f () =
     do_if_not_computing "do_or_activate"
       (fun current ->
@@ -2327,13 +2320,13 @@ let main files =
   in
 
   let file_actions = GAction.action_group ~name:"File" () in
-  let export_actions = GAction.action_group ~name:"Export" () in
   let edit_actions = GAction.action_group ~name:"Edit" () in
+  let view_actions = GAction.action_group ~name:"View" () in
+  let export_actions = GAction.action_group ~name:"Export" () in
   let navigation_actions = GAction.action_group ~name:"Navigation" () in
   let tactics_actions = GAction.action_group ~name:"Tactics" () in
   let templates_actions = GAction.action_group ~name:"Templates" () in
   let queries_actions = GAction.action_group ~name:"Queries" () in
-  let display_actions = GAction.action_group ~name:"Display" () in
   let compile_actions = GAction.action_group ~name:"Compile" () in
   let windows_actions = GAction.action_group ~name:"Windows" () in
   let help_actions = GAction.action_group ~name:"Help" () in
@@ -2362,10 +2355,18 @@ let main files =
     ~accel:(!current.modifier_for_tactics^sc)
     ~callback:(do_if_active (fun a -> a#insert_command
 			       ("progress "^s^".\n") (s^".\n"))) in
-  let query_shortcut s accel = GAction.add_action s ~label:("_"^s) ?accel
-    ~callback:(fun _ -> let term = get_current_word () in
-		 session_notebook#current_term.command#new_command ~command:s ~term ())
-  in let add_complex_template (name, label, text, offset, len, key) =
+  let query_callback command _ =
+    let word = get_current_word () in
+    if not (word = "") then
+      let term = session_notebook#current_term in
+      let query = command ^ " " ^ word ^ "." in
+      term.message_view#buffer#set_text "";
+      term.analyzed_view#raw_coq_query query
+  in
+  let query_shortcut s accel =
+    GAction.add_action s ~label:("_"^s) ?accel ~callback:(query_callback s)
+  in
+  let add_complex_template (name, label, text, offset, len, key) =
     (* Templates/Lemma *)
     let callback _ =
       let {script = view } = session_notebook#current_term in
@@ -2450,6 +2451,31 @@ let main files =
 	end;
 	reset_revert_timer ()) ~stock:`PREFERENCES;
       (* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
+    GAction.add_actions view_actions [
+      GAction.add_action "View" ~label:"_View";
+      GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("<SHIFT>Left") ~stock:`GO_BACK
+        ~callback:(fun _ -> session_notebook#previous_page ());
+      GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<SHIFT>Right") ~stock:`GO_FORWARD
+        ~callback:(fun _ -> session_notebook#next_page ());
+      GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar"
+        ~active:(!current.show_toolbar) ~callback:
+        (fun _ -> !current.show_toolbar <- not !current.show_toolbar;
+           !refresh_toolbar_hook ());
+      GAction.add_toggle_action "Show Query Pane" ~label:"Show _Query Pane"
+        ~callback:(fun _ -> let ccw = session_notebook#current_term.command in
+                     if ccw#frame#misc#visible
+                     then ccw#frame#misc#hide ()
+                     else ccw#frame#misc#show ())
+        ~accel:"Escape";
+    ];
+    List.iter
+      (fun (opts,name,label,key,dflt) ->
+         GAction.add_toggle_action name ~active:dflt ~label
+           ~accel:(!current.modifier_for_display^key)
+          ~callback:(fun v -> do_or_activate (fun a ->
+            let () = setopts !(session_notebook#current_term.toplvl) opts v#get_active in
+            a#show_goals) ()) view_actions)
+      print_items;
     GAction.add_actions navigation_actions [
       GAction.add_action "Navigation" ~label:"_Navigation";
       GAction.add_action "Forward" ~label:"_Forward" ~stock:`GO_DOWN
@@ -2532,15 +2558,6 @@ let main files =
       query_shortcut "Locate" None;
       query_shortcut "Whelp Locate" None;
     ];
-    GAction.add_action "Display" ~label:"_Display" display_actions;
-    List.iter
-      (fun (opts,name,label,key,dflt) ->
-         GAction.add_toggle_action name ~active:dflt ~label
-	   ~accel:(!current.modifier_for_display^key)
-          ~callback:(fun v -> do_or_activate (fun a ->
-            let () = setopts !(session_notebook#current_term.toplvl) opts v#get_active in
-            a#show_goals) ()) display_actions)
-      print_items;
     GAction.add_actions compile_actions [
       GAction.add_action "Compile" ~label:"_Compile";
       GAction.add_action "Compile buffer" ~label:"_Compile buffer" ~callback:compile_f;
@@ -2551,16 +2568,6 @@ let main files =
     ];
     GAction.add_actions windows_actions [
       GAction.add_action "Windows" ~label:"_Windows";
-      GAction.add_toggle_action "Show/Hide Query Pane" ~label:"Show/Hide _Query Pane"
-	~callback:(fun _ -> let ccw = session_notebook#current_term.command in
-		     if ccw#frame#misc#visible
-		     then ccw#frame#misc#hide ()
-		     else ccw#frame#misc#show ())
-	~accel:"Escape";
-      GAction.add_toggle_action "Show/Hide Toolbar" ~label:"Show/Hide _Toolbar"
-	~active:(!current.show_toolbar) ~callback:
-	(fun _ -> !current.show_toolbar <- not !current.show_toolbar;
-	   !show_toolbar !current.show_toolbar);
       GAction.add_action "Detach View" ~label:"Detach _View"
 	~callback:(fun _ -> do_if_not_computing "detach view"
 		     (function {script=v;analyzed_view=av} ->
@@ -2608,11 +2615,11 @@ let main files =
     Coqide_ui.ui_m#insert_action_group file_actions 0;
     Coqide_ui.ui_m#insert_action_group export_actions 0;
     Coqide_ui.ui_m#insert_action_group edit_actions 0;
+    Coqide_ui.ui_m#insert_action_group view_actions 0;
     Coqide_ui.ui_m#insert_action_group navigation_actions 0;
     Coqide_ui.ui_m#insert_action_group tactics_actions 0;
     Coqide_ui.ui_m#insert_action_group templates_actions 0;
     Coqide_ui.ui_m#insert_action_group queries_actions 0;
-    Coqide_ui.ui_m#insert_action_group display_actions 0;
     Coqide_ui.ui_m#insert_action_group compile_actions 0;
     Coqide_ui.ui_m#insert_action_group windows_actions 0;
     Coqide_ui.ui_m#insert_action_group help_actions 0;
@@ -2625,9 +2632,6 @@ let main files =
     let toolbar = new GObj.widget tbar in
     vbox#pack toolbar;
 
-    show_toolbar :=
-      (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ());
-
     ignore (w#event#connect#delete ~callback:(fun _ -> quit_f (); true));
 
   (* The vertical Separator between Scripts and Goals *)
@@ -2790,17 +2794,39 @@ let main files =
   (* Progress Bar *)
   lower_hbox#pack pbar#coerce;
   pbar#set_text "CoqIde started";
-  (* XXX *)
-  change_font :=
-    (fun fd ->
-      List.iter
-	(fun {script=view; proof_view=prf_v; message_view=msg_v} ->
-          view#misc#modify_font fd;
-          prf_v#misc#modify_font fd;
-          msg_v#misc#modify_font fd
-        )
-	session_notebook#pages;
+
+  (* Initializing hooks *)
+
+  refresh_toolbar_hook :=
+    (fun () -> if !current.show_toolbar then toolbar#misc#show () else toolbar#misc#hide ());
+  refresh_font_hook :=
+    (fun () ->
+      let fd = !current.text_font in
+      let iter_page p =
+        p.script#misc#modify_font fd;
+        p.proof_view#misc#modify_font fd;
+        p.message_view#misc#modify_font fd;
+        p.command#refresh_font ()
+      in
+      List.iter iter_page session_notebook#pages;
     );
+  refresh_background_color_hook :=
+    (fun () ->
+      let clr = Tags.color_of_string !current.background_color in
+      let iter_page p =
+        p.script#misc#modify_base [`NORMAL, `COLOR clr];
+        p.proof_view#misc#modify_base [`NORMAL, `COLOR clr];
+        p.message_view#misc#modify_base [`NORMAL, `COLOR clr];
+        p.command#refresh_color ()
+      in
+      List.iter iter_page session_notebook#pages;
+    );
+  resize_window_hook := (fun () ->
+    w#resize
+      ~width:!current.window_width
+      ~height:!current.window_height);
+  refresh_tabs_hook := update_notebook_pos;
+
   let about_full_string =
     "\nCoq is developed by the Coq Development Team\
      \n(INRIA - CNRS - LIX - LRI - PPS)\
@@ -2865,10 +2891,12 @@ let main files =
   (*
 
   *)
-  resize_window := (fun () ->
-    w#resize
-      ~width:!current.window_width
-      ~height:!current.window_height);
+(* Begin Color configuration *)
+
+  Tags.set_processing_color (Tags.color_of_string !current.processing_color);
+  Tags.set_processed_color (Tags.color_of_string !current.processed_color);
+
+(* End of color configuration *)
   ignore(nb#connect#switch_page
 	   ~callback:
 	   (fun i ->
@@ -2892,7 +2920,7 @@ let main files =
       session_notebook#goto_page index;
     end;
   initial_about session_notebook#current_term.proof_view#buffer;
-  !show_toolbar !current.show_toolbar;
+  !refresh_toolbar_hook ();
   session_notebook#current_term.script#misc#grab_focus ();;
 
 (* This function check every half of second if GeoProof has send
@@ -2921,43 +2949,24 @@ let rec check_for_geoproof_input () =
     in the path. Note that the -coqtop option to coqide allows to override
     this default coqtop path *)
 
-let default_coqtop_path () =
-  let prog = Sys.executable_name in
-  try
-    let pos = String.length prog - 6 in
-    let i = Str.search_backward (Str.regexp_string "coqide") prog pos in
-    String.blit "coqtop" 0 prog i 6;
-    prog
-  with _ -> "coqtop"
-
 let read_coqide_args argv =
   let rec filter_coqtop coqtop project_files out = function
     | "-coqtop" :: prog :: args ->
-      if coqtop = "" then filter_coqtop prog project_files out args
+      if coqtop = None then filter_coqtop (Some prog) project_files out args
       else
-	(output_string stderr "Error: multiple -coqtop options"; exit 1)
+       (output_string stderr "Error: multiple -coqtop options"; exit 1)
     | "-f" :: file :: args ->
 	filter_coqtop coqtop
 	  ((Minilib.canonical_path_name (Filename.dirname file),
 	    Project_file.read_project_file file) :: project_files) out args
     | "-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1
+    | "-coqtop" :: [] -> output_string stderr "Error: missing argument after -coqtop"; exit 1
+    | "-debug"::args -> Ideutils.debug := true;
+      filter_coqtop coqtop project_files ("-debug"::out) args
     | arg::args -> filter_coqtop coqtop project_files (arg::out) args
-    | [] -> ((if coqtop = "" then default_coqtop_path () else coqtop),
-	     List.rev project_files,List.rev out)
+    | [] -> (coqtop,List.rev project_files,List.rev out)
   in
-  let coqtop,project_files,argv = filter_coqtop "" [] [] argv in
-    Minilib.coqtop_path := coqtop;
+  let coqtop,project_files,argv = filter_coqtop None [] [] argv in
+    Ideutils.custom_coqtop := coqtop;
     custom_project_files := project_files;
   argv
-
-let process_argv argv =
-  try
-    let continue,filtered = Coq.filter_coq_opts (List.tl argv) in
-    if not continue then
-      (List.iter Minilib.safe_prerr_endline filtered; exit 0);
-    let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in
-    if opts <> [] then
-      (Minilib.safe_prerr_endline ("Illegal option: "^List.hd opts); exit 1);
-    filtered
-  with _ ->
-    (Minilib.safe_prerr_endline "coqtop choked on one of your option"; exit 1)