Merge branch 'v8.5'

4 files changed, 55 insertions, 54 deletions

diff --git a/ide/coq.lang b/ide/coq.lang
index 608a4aeaea..38dabda506 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -22,19 +22,19 @@
   </styles>
   
   <definitions>
-    <define-regex id="space">\s</define-regex>
+    <define-regex id="space">\s+</define-regex>
     <define-regex id="first_ident_char">[_\p{L}]</define-regex>
     <define-regex id="ident_char">[_\p{L}'\pN]</define-regex>
     <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex>
     <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
     <define-regex id="undotted_sep">[-+*{}]</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
-    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)</define-regex>
-    <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex>
-    <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex>
-    <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex>
-    <define-regex id="end_proof">(Qed)|(Defined)|(Admitted)|(Abort)</define-regex>
-    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))|(?'gal2'Goal)</define-regex>
+    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex>
+    <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
+    <define-regex id="locality">((Local|Global)\%{space})?</define-regex>
+    <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex>
+    <define-regex id="end_proof">Qed|Defined|Admitted|Abort|Save</define-regex>
+    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex>
 
     <context id="escape-seq" style-ref="escape">
       <match>""</match>
@@ -97,7 +97,6 @@
 	      <keyword>then</keyword>
 	      <keyword>else</keyword>
 	      <keyword>return</keyword>
-	      <keyword>using</keyword>
 	    </context>
 	    <context id="constr-sort" style-ref="constr-sort">
 	      <keyword>Prop</keyword>
@@ -113,7 +112,7 @@
 	  </include>
 	</context>
 	<context id="proof">
-	  <start>Proof(\%{dot_sep}|\%{space}+(using)|\%{space}+(with))</start>
+	  <start>Proof(\%{dot_sep}|\%{space}using|\%{space}with)</start>
 	  <end>\%{end_proof}\%{dot_sep}</end>
 	  <include>
 	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
@@ -157,17 +156,18 @@
 	  <keyword>Eval</keyword>
 	  <keyword>Load</keyword>
 	  <keyword>Undo</keyword>
+	  <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
 	  <keyword>Print</keyword>
-	  <keyword>Save</keyword>
 	  <keyword>Comments</keyword>
-	  <keyword>Solve\%{space}+Obligation</keyword>
-	  <keyword>((Uns)|(S))et(\%{space}+\%{ident})+</keyword>
-	  <keyword>(\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation</keyword>
+	  <keyword>Solve\%{space}Obligation</keyword>
+	  <keyword>(Uns|S)et(\%{space}\%{ident})+</keyword>
+	  <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword>
 	  <keyword>\%{locality}Infix</keyword>
-	  <keyword>(Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)</keyword>
+	  <keyword>Declare\%{space}ML\%{space}Module</keyword>
+	  <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme)</keyword>
 	</context>
 	<context id="hint-command" style-ref="vernac-keyword">
-	  <prefix>\%{locality}Hint\%{space}+</prefix>
+	  <prefix>\%{locality}Hint\%{space}</prefix>
 	  <keyword>Resolve</keyword>
 	  <keyword>Immediate</keyword>
 	  <keyword>Constructors</keyword>
@@ -178,35 +178,40 @@
 	  <keyword>Rewrite</keyword>
 	</context>
 	<context id="scope-command" style-ref="vernac-keyword">
-	  <suffix>\%{space}+Scope</suffix>
+	  <suffix>\%{space}Scope</suffix>
 	  <keyword>\%{locality}Open</keyword>
 	  <keyword>\%{locality}Close</keyword>
 	  <keyword>Bind</keyword>
 	  <keyword>Delimit</keyword>
 	</context>
 	<context id="command-for-qualit">
-	  <suffix>\%{space}+(?'qua'\%{qualit})</suffix>
+	  <suffix>\%{space}(?'qua'\%{qualit})</suffix>
 	  <keyword>Chapter</keyword>
-	  <keyword>Combined\%{space}+Scheme</keyword>
+	  <keyword>Combined\%{space}Scheme</keyword>
+	  <keyword>Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for</keyword>
 	  <keyword>End</keyword>
 	  <keyword>Section</keyword>
+	  <keyword>Module(\%{space}Type)?</keyword>
+	  <keyword>Declare\%{space}Module(\%{space}(Import|Export))?</keyword>
+	  <keyword>About</keyword>
 	  <keyword>Arguments</keyword>
-	  <keyword>Implicit\%{space}+Arguments</keyword>
-	  <keyword>Import</keyword>
+	  <keyword>Implicit\%{space}Arguments</keyword>
 	  <keyword>Include</keyword>
-	  <keyword>Export</keyword>
-	  <keyword>Require(\%{space}+((Import)|(Export)))?</keyword>
-	  <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword>
-	  <keyword>Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive)</keyword>
+	  <keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword>
 	  <include>
 	    <context sub-pattern="1" style-ref="vernac-keyword"/>
 	    <context sub-pattern="qua" style-ref="identifier"/>
 	  </include>
 	</context>
-	<context id="command-for-qualit-list" style-ref="vernac-keyword">
-	  <suffix>(?'qua_list'(\%{space}+\%{qualit})+)</suffix>
-	  <keyword>Typeclasses (Transparent)|(Opaque)</keyword>
+	<context id="command-for-qualit-list">
+	  <suffix>(?'qua_list'(\%{space}\%{qualit})+)</suffix>
+	  <keyword>Typeclasses (Transparent|Opaque)</keyword>
+	  <keyword>Require(\%{space}(Import|Export))?</keyword>
+	  <keyword>Import</keyword>
+	  <keyword>Export</keyword>
+	  <keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword>
 	  <include>
+	    <context sub-pattern="1" style-ref="vernac-keyword"/>
 	    <context sub-pattern="qua_list" style-ref="identifier"/>
 	  </include>
 	</context>
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1800cb8fe8..c6073d599d 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -363,7 +363,7 @@ object(self)
        else if has_flag sentence `ERROR then [error_bg]
        else if has_flag sentence `INCOMPLETE then [incomplete]
        else [processed]) @
-      (if [ `UNSAFE ] = sentence.flags then [unjustified] else [])
+      (if has_flag sentence `UNSAFE then [unjustified] else [])
     in
     List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags;
     List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags
@@ -589,7 +589,7 @@ object(self)
                   Doc.assign_tip_id document id;
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
-                  self#cleanup (Doc.cut_at document tip);
+                  self#cleanup ~all:true (Doc.cut_at document tip);
                   logger Pp.Notice msg;
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
@@ -651,7 +651,7 @@ object(self)
       Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
     with Not_found -> initial_state, Doc.focused document 
 
-  method private cleanup seg =
+  method private cleanup ~all seg =
     if seg <> [] then begin
       let start = buffer#get_iter_at_mark (CList.last seg).start in
       let stop = buffer#get_iter_at_mark (CList.hd seg).stop in
@@ -662,7 +662,7 @@ object(self)
       buffer#remove_tag Tags.Script.unjustified ~start ~stop;
       buffer#remove_tag Tags.Script.tooltip ~start ~stop;
       buffer#remove_tag Tags.Script.to_process ~start ~stop;
-      buffer#remove_tag Tags.Script.read_only ~start ~stop;
+      if all then buffer#remove_tag Tags.Script.read_only ~start ~stop;
       buffer#remove_tag Tags.Script.error ~start ~stop;
       buffer#remove_tag Tags.Script.error_bg ~start ~stop;
       buffer#move_mark ~where:start (`NAME "start_of_input")
@@ -694,13 +694,13 @@ object(self)
       Coq.bind (Coq.edit_at to_id) (function
       | Good (CSig.Inl (* NewTip *) ()) ->
           if unfocus_needed then self#exit_focus;
-          self#cleanup (Doc.cut_at document to_id);
+          self#cleanup ~all:true (Doc.cut_at document to_id);
           conclusion ()
       | Good (CSig.Inr (* Focus  *) (stop_id,(start_id,tip))) ->
           if unfocus_needed then self#exit_focus;
-          self#cleanup (Doc.cut_at document tip);
+          self#cleanup ~all:true (Doc.cut_at document tip);
           self#enter_focus start_id stop_id;
-          self#cleanup (Doc.cut_at document to_id);
+          self#cleanup ~all:false (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
           if loc <> None then messages#push Pp.Error "Fixme LOC";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index c977879a7b..87efd17d22 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -84,14 +84,15 @@ let pr_exit_status = function
   | _ -> " failed"
 
 let make_coqtop_args = function
-  |None -> !sup_args
+  |None -> "", !sup_args
   |Some the_file ->
     let get_args f = Project_file.args_from_project f
       !custom_project_files prefs.project_file_name
     in
     match prefs.read_project with
-      |Ignore_args -> !sup_args
-      |Append_args -> get_args the_file @ !sup_args
+      |Ignore_args -> "", !sup_args
+      |Append_args ->
+         let fname, args = get_args the_file in fname, args @ !sup_args
       |Subst_args -> get_args the_file
 
 (** Setting drag & drop on widgets *)
@@ -120,7 +121,10 @@ let set_drag (w : GObj.drag_ops) =
 (** Session management *)
 
 let create_session f =
-  let ans = Session.create f (make_coqtop_args f) in
+  let project_file, args = make_coqtop_args f in
+  if project_file <> "" then
+    flash_info (Printf.sprintf "Reading options from %s" project_file);
+  let ans = Session.create f args in
   let _ = set_drag ans.script#drag in
   ans
 
@@ -530,7 +534,7 @@ let update_status sn =
       | None -> ""
       | Some n -> ", proving " ^ n
     in
-    display ("Ready"^ if current.nanoPG then ", [μPG]" else "" ^ path ^ name);
+    display ("Ready"^ (if current.nanoPG then ", [μPG]" else "") ^ path ^ name);
     Coq.return ()
   in
   Coq.bind (Coq.status ~logger:sn.messages#push false) next
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 41dc1befa2..f7279f9cfe 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -182,29 +182,21 @@ let read_project_file f =
     (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f)))
 
 let args_from_project file project_files default_name =
-  let is_f = CUnix.same_file file in
-  let contains_file dir =
-      List.exists (fun x -> is_f (CUnix.correct_path x dir))
-  in
   let build_cmd_line ml_inc i_inc r_inc args =
     List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc
       (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc
         (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc
 	  (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args [])))
   in try
-      let (_,(_,(ml_inc,i_inc,r_inc),(args,_))) =
-	List.find (fun (dir,((v_files,_,_,_),_,_)) ->
-		     contains_file dir v_files) project_files in
-	build_cmd_line ml_inc i_inc r_inc args
-    with Not_found ->
+      let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in
+	fname, build_cmd_line ml_inc i_inc r_inc args
+    with Failure _ ->
       let rec find_project_file dir = try
+	let fname = Filename.concat dir default_name in
 	let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) =
-	  read_project_file (Filename.concat dir default_name) in
-	  if contains_file dir v_files
-	  then build_cmd_line ml_inc i_inc r_inc args
-	  else let newdir = Filename.dirname dir in
-	    if dir = newdir then [] else find_project_file newdir
+          read_project_file fname in
+	fname, build_cmd_line ml_inc i_inc r_inc args
       with Sys_error s ->
 	let newdir = Filename.dirname dir in
-	  if dir = newdir then [] else find_project_file newdir
+	  if dir = newdir then "",[] else find_project_file newdir
       in find_project_file (Filename.dirname file)