From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Sat, 18 Aug 2007 20:34:57 +0000
Subject: Imported Upstream version 8.1.pl1+dfsg

---
 ide/coq_commands.ml        | 17 +++++++++++++----
 ide/highlight.mll          | 11 +++++++----
 ide/utils/configwin_ihm.ml |  6 +-----
 3 files changed, 21 insertions(+), 13 deletions(-)

(limited to 'ide')

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 30d99f5b..677c5eff 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_commands.ml 7102 2005-06-03 13:14:27Z coq $ *)
+(* $Id: coq_commands.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 let commands = [
   [(* "Abort"; *)
@@ -77,10 +77,17 @@ let commands = [
   ["Module";
    "Module Type";
    "Mutual Inductive";];
-  ["Notation";];
-  ["Opaque";];
+  ["Notation";
+   "Next Obligation";];
+  ["Opaque";
+   "Obligations Tactic";];
   ["Parameter";
-   "Proof."];
+   "Proof.";
+   "Program Definition";
+   "Program Fixpoint";     
+   "Program Lemma";
+   "Program Theorem";
+  ];
   ["Qed.";
    ];
   ["Read Module";
@@ -155,6 +162,8 @@ let state_preserving = [
   "Extraction Module";
   "Inspect";
   "Locate";
+  
+  "Obligations";
   "Print";
   "Print All.";
   "Print Classes";
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 27ead696..2f099208 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: highlight.mll 8880 2006-05-31 10:52:08Z notin $ *)
+(* $Id: highlight.mll 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 {
 
@@ -28,7 +28,8 @@
 	 "Notation"; "Proof" ; "Print"; "Qed" ;
 	 "Require" ; "Reset"; "Undo"; "Save" ;
 	 "Section" ; "Unset" ;
-	 "Set" ; "Notation"
+	 "Set" ; "Notation";
+	 "Implicit"; "Arguments"; "Unfold"; "Resolve"
       ];
     Hashtbl.mem h
 
@@ -36,7 +37,7 @@
     let h = Hashtbl.create 97 in
       List.iter (fun s -> Hashtbl.add h s ())
 	[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; 
-	  "end"; "as"; "let"; "if"; "then"; "else"; "return";
+	  "end"; "as"; "let"; "in"; "dest"; "if"; "then"; "else"; "return";
 	  "Prop"; "Set"; "Type"]; 
       Hashtbl.mem h
 
@@ -45,7 +46,7 @@
       List.iter (fun s -> Hashtbl.add h s ())
 	[ "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ; "Proposition" ; "Property" ;
 	  "Definition" ; "Let" ; "Example" ; "SubClass" ; "Inductive" ; "CoInductive" ; 
-	  "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint";  
+	  "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint"; 
 	  "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ;
 	  "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters"
 	];
@@ -74,12 +75,14 @@ let declaration =
   "Inductive" | "CoInductive" | 
   "Record" | "Structure" |
   "Fixpoint" | "CoFixpoint"
+       
 
 rule next_order = parse
   | "(*" 
       { comment_start := lexeme_start lexbuf; comment lexbuf }
   | "Module Type"
       { lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
+  | "Program" space+ ident as id { lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
   | ident as id 
       { if is_keyword id then 
 	    lexeme_start lexbuf, lexeme_end lexbuf, "kwd" 
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index e9ba9789..240fd829 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1108,10 +1108,6 @@ let edit ?(with_apply=true)
       List.iter (fun param_box -> param_box#apply) list_param_box  ;
       apply ()
     in
-    let f_ok () =
-      List.iter (fun param_box -> param_box#apply) list_param_box  ;
-      Return_ok
-    in
     let destroy () =
       tooltips#destroy () ;
       dialog#destroy ();
@@ -1120,7 +1116,7 @@ let edit ?(with_apply=true)
       try
 	match dialog#run () with
 	  | `APPLY  -> f_apply (); iter Return_apply
-	  | `OK -> destroy (); f_ok ()
+	  | `OK -> f_apply (); destroy (); Return_ok
 	  | _ -> destroy (); rep
       with
 	  Failure s ->
-- 
cgit v1.2.3