coqide: locale iso-8859-1 par defaut si probleme. Interdiction des lemmes locaux. Reparation du Undo avec Section et constantes de meme nom. Decoupe tag modifie

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3793 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 88 insertions, 39 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 0678c16c7..881d27bd5 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -18,10 +18,14 @@ let prerr_endline s = if !debug then prerr_endline s else ()
 
 let output = ref (Format.formatter_of_out_channel stdout)
 
-let msg x = 
-  Format.fprintf !output "%s\n" x;
-  Format.pp_print_flush !output ();;
- 
+let msg m = 
+  let b =  Buffer.create 103 in
+  Pp.msg_with (Format.formatter_of_buffer b) m;
+  Buffer.contents b
+
+let msgnl m = 
+  (msg m)^"\n"
+
 let init () = 
   Options.make_silent true;
   Coqtop.init_ide ()
@@ -53,31 +57,35 @@ let is_in_coq_lib dir =
       Coq_config.theories_dirs
   with _ -> prerr_endline " No(because of a global exn)";false
 
+let is_in_proof_mode () = 
+  try ignore (get_pftreestate ()); true with _ -> false
+
 let interp s = 
-  prerr_endline s;
-  flush stderr;
-  let po = Pcoq.Gram.parsable (Stream.of_string s) in
-  Vernac.raw_do_vernac po;
-  let po = Pcoq.Gram.parsable (Stream.of_string s) in
-  match Pcoq.Gram.Entry.parse Pcoq.main_entry po with
-    (* | Some (_, VernacDefinition _) *)
-    | Some last -> 
-	prerr_endline ("Done with "^s);
-	flush stderr;
-	last
-    | None -> assert false
+  prerr_endline "Starting interp...";
+  let pe = Pcoq.Gram.Entry.parse 
+	     Pcoq.main_entry 
+	     (Pcoq.Gram.parsable (Stream.of_string s)) 
+  in match pe with 
+    | Some (loc,(VernacDefinition _  | VernacStartTheoremProof _ )) 
+      when is_in_proof_mode () 
+	-> 
+	raise (Stdpp.Exc_located (loc, 
+			   Util.UserError
+			     ("CoqIde",
+			      (str "Proof imbrications are forbidden"))
+				 ))
+    | _ -> 
+	Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
+	match pe with
+	  | Some last -> 
+	      prerr_endline ("...Done with interp of : "^s);
+	      last
+	  | None -> assert false
 
 let is_tactic = function
   | VernacSolve _ -> true
   | _ -> false
 
-let msg m = 
-  let b =  Buffer.create 103 in
-  Pp.msg_with (Format.formatter_of_buffer b) m;
-  Buffer.contents b
-
-let msgnl m = 
-  (msg m)^"\n"
 
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
@@ -111,7 +119,7 @@ let print_toplevel_error exc =
 	   ++ str (Printexc.to_string  e)),
 	(if is_pervasive_exn exc then None else loc)
 
-let process_exn e = let s,loc=print_toplevel_error e in (msgnl s,loc)
+let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
 
 let interp_last last = 
   prerr_string "*";
@@ -221,8 +229,11 @@ let reset_initial () =
   Vernacentries.abort_refine Lib.reset_initial ()
 
 let reset_to id = 
-  prerr_endline ("Reset called with "^(string_of_id id)); flush stderr;
+  prerr_endline ("Reset called with "^(string_of_id id));
   Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id)
+let reset_to_mod id = 
+  prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); 
+  Lib.reset_mod (Util.dummy_loc,id)
 
 
 let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
diff --git a/ide/coq.mli b/ide/coq.mli
index faf35e616..b2881a70d 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -33,6 +33,7 @@ type reset_info = NoReset | Reset of Names.identifier * bool ref
 val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
 val reset_initial : unit -> unit
 val reset_to : identifier -> unit
+val reset_to_mod : identifier -> unit
 
 val hyp_menu : hyp -> (string * string) list
 val concl_menu : concl -> (string * string) list
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b6aa92112..570435ce6 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -372,14 +372,6 @@ let break () = Unix.kill pid Sys.sigusr1
 let can_break () = set_break () 
 let cant_break () = unset_break () 
 
-let find_tag_limits (tag :GText.tag) (it:GText.iter) = 
-    (if not (it#begins_tag (Some tag)) 
-     then it#backward_to_tag_toggle (Some tag)
-     else it#copy),
-    (if not (it#ends_tag (Some tag))
-     then it#forward_to_tag_toggle (Some tag)
-     else it#copy)
-
 let activate_input i = 
   (match !active_view with
      | None -> () 
@@ -824,7 +816,13 @@ object(self)
       else begin
 	let t = pop () in
 	begin match t.reset_info with
-	  | Reset (id, ({contents=true} as v)) -> v:=false; reset_to id
+	  | Reset (id, ({contents=true} as v)) -> v:=false; 
+	      (match snd t.ast with 
+		 | VernacBeginSection _ | VernacDefineModule _ 
+		 | VernacDeclareModule _ | VernacDeclareModuleType _
+		 | VernacEndSegment _ 
+		   -> reset_to_mod id
+		 | _ ->  reset_to id)
 	  | _ -> synchro ()
 	end;
 	interp_last t.ast;
@@ -891,9 +889,14 @@ object(self)
 	      try Pfedit.undo 1; ignore (pop ()); update_input () 
 	      with _ -> self#backtrack_to start
 	    end
-	| {reset_info=Reset (id, {contents=true})} ->
+	| {ast=_,t;reset_info=Reset (id, {contents=true})} ->
 	    ignore (pop ());
-	    reset_to id;
+	    (match t with 
+	      | VernacBeginSection _ | VernacDefineModule _ 
+	      | VernacDeclareModule _ | VernacDeclareModuleType _
+	      | VernacEndSegment _ 
+		  -> reset_to_mod id
+	      | _ ->  reset_to id);
 	    update_input ()
 	| { ast = _, ( VernacStartTheoremProof _ 
 		     | VernacDefinition (_,_,ProveBody _,_,_));
@@ -1166,7 +1169,7 @@ let main files =
 	!input_views;
       let b = Buffer.create 1024 in
       with_file f ~f:(input_channel b);
-      let s = try_convert (Buffer.contents b) in
+      let s = do_convert (Buffer.contents b) in
       let view = create_input_tab (Filename.basename f) in
       (match !manual_monospace_font with
 	 | None -> ()
@@ -1192,7 +1195,7 @@ let main files =
       av#view#clear_undo
     with       
       | Vector.Found i -> set_current_view i
-      | e -> !flash_info "Load failed"
+      | e -> !flash_info ("Load failed: "^(Printexc.to_string e))
   in
   let load_m = file_factory#add_item "_Open/Create" ~key:GdkKeysyms._O in
   let load_f () = 	  
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index cb018e842..7f05d0d2f 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -52,6 +52,17 @@ let try_convert s =
     "(* Fatal error: wrong encoding in input.
 Please set your locale according to your file encoding.*)"
 
+let do_convert s = 
+  if Glib.Utf8.validate s then s else
+    try 
+      (prerr_endline 
+	 "Coqide warning: input is not UTF-8 encoded. Trying to convert from locale.";
+       Glib.Convert.locale_to_utf8 s)
+    with _ -> 
+      (prerr_endline 
+	 "Coqide warning: input is not even LOCALE encoded. Trying to convert from fr_FR.";
+       Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:"ISO-8859-1")
+
 let try_export file_name s = 
   try 
     let s = 
@@ -59,7 +70,12 @@ let try_export file_name s =
 	s 
       else
 	(try Glib.Convert.locale_from_utf8 s 
-	 with _ -> prerr_endline "Warning: exporting to utf8";s)
+	 with _ -> 
+	   try 
+	     prerr_endline "Warning: exporting to ISO8859-1";
+	     Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:"ISO-8859-1"
+	   with _ -> 
+	     prerr_endline "Warning: exporting to utf8";s)
     in
     let oc = open_out file_name in
     output_string oc s;
@@ -156,3 +172,21 @@ let select_file ~title ?(dir = last_dir) ?(filename="") () =
   fs # show ();
   GMain.Main.main ();
   !file
+
+
+let find_tag_start (tag :GText.tag) (it:GText.iter) =
+  let it = it#copy in
+  let tag = Some tag in
+  while not (it#begins_tag tag) && it#nocopy#backward_char do
+    ()
+  done;
+  it
+let find_tag_stop (tag :GText.tag) (it:GText.iter) =
+  let it = it#copy in
+  let tag = Some tag in
+  while not (it#ends_tag tag) && it#nocopy#forward_char do
+    ()
+  done;
+  it
+let find_tag_limits (tag :GText.tag) (it:GText.iter) = 
+ (find_tag_start tag it , find_tag_stop tag it)