plus de syntaxe v8

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

3 files changed, 54 insertions, 21 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index d8e0a04c2..54a0e4736 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -103,24 +103,42 @@ let user_error_loc l s =
 let interp s = 
   prerr_endline "Starting interp...";
   prerr_endline s;
-  let pe = Pcoq.Gram.Entry.parse 
-	     Pcoq.main_entry 
-	     (Pcoq.Gram.parsable (Stream.of_string s)) 
-  in match pe with 
-    | Some (loc,( VernacDefinition _  | VernacStartTheoremProof _ 
-		| VernacBeginSection _ | VernacGoal _
-		| VernacDefineModule _ | VernacDeclareModuleType _))
-      when is_in_proof_mode () -> 
-	user_error_loc loc (str "cannot do that while in proof mode.")
-    | Some (loc, VernacDebug _ ) ->
-	user_error_loc loc (str "cannot do that within CoqIDE")
-    | _ -> 
-	Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
-	match pe with
-	  | Some last -> 
+  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
+  match pe with 
+    | None -> assert false
+    | Some((loc,vernac) as last) ->
+	match vernac with
+	  | VernacDefinition _  | VernacStartTheoremProof _ 
+	  | VernacBeginSection _ | VernacGoal _
+	  | VernacDefineModule _ | VernacDeclareModuleType _
+		when is_in_proof_mode () -> 
+		  user_error_loc loc (str "CoqIDE do not support nested goals")
+	  | VernacDebug _ ->
+	      user_error_loc loc (str "Debug mode not available within CoqIDE")
+	  | VernacResetName _
+	  | VernacResetInitial 
+	  | VernacBack _ 
+	  | VernacAbort _ 
+	  | VernacAbortAll
+	  | VernacRestart
+	  | VernacSuspend
+	  | VernacResume _
+	  | VernacUndo _ ->
+	      user_error_loc loc (str "Use CoqIDE navigation instead") 
+	  | _ ->
+	      begin
+		match vernac with
+		  | VernacPrintOption _ 
+		  | VernacCheckMayEval _
+		  | VernacGlobalCheck _
+		  | VernacPrint _
+		  | VernacSearch _ ->   ()
+		  | _ -> ()
+	      end;
+	      Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
 	      prerr_endline ("...Done with interp of : "^s);
 	      last
-	  | None -> assert false
 
 let interp_and_replace s = 
   let result = interp s in
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index aefae8fbb..7173bfc2f 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -60,12 +60,11 @@ let commands = [
    "Grammar";];
   ["Hint";
    "Hint Constructors";
-   "Hint Unfold";
+   "Hint Extern";
+   "Hint Immediate";
+   "Hint Resolve";
    "Hint Rewrite";
-   "Hints Extern";
-   "Hints Immediate";
-   "Hints Resolve";
-   "Hints Unfold";
+   "Hint Unfold";
    "Hypothesis";];
   ["Identity Coercion";
    "Implicit Arguments Off.";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index dcb3228fb..890a38bf5 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1717,6 +1717,9 @@ let create_input_tab filename =
 	    ~name:"processed" 
 	    [`BACKGROUND "light green" ;`EDITABLE false]);
   tv1
+
+
+let last_make = ref "";;
  
 let main files = 
   (* Statup preferences *)
@@ -2549,10 +2552,23 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
     save_f ();
     av#insert_message "Command output:\n";
     let s,res = run_command av#insert_message !current.cmd_make in
+    last_make := res;
     !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
   in
   let make_m = externals_factory#add_item "_Make" ~callback:make_f in
   
+
+  (* Compile/Next Error *)
+  let next_error () = ()
+(*
+    let file,line,start,stop = search_next_error () in
+    av#insert_message 
+      ("Error in " ^ file ^ "," ^ (string_of_int line)
+*)
+  in
+  let next_error_m = externals_factory#add_item "_Next error" ~callback:next_error in
+  
+
   (* Command/CoqMakefile Menu*)
   let coq_makefile_f () =
     let v = get_active_view () in