Imported Upstream version 8.5~beta3+dfsg

15 files changed, 286 insertions, 214 deletions

diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 87cc6d06..36715356 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -17,7 +17,7 @@
 
 let space = [' ' '\010' '\013' '\009' '\012']
 let char = ['A'-'Z' 'a'-'z' '_' '0'-'9']
-let ident = char+
+let ident = (char | '.')+
 let ignore = space | ('#' [^ '\n']*)
 
 rule prefs m = parse
diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang
index 4c488ae8..7cfc1670 100644
--- a/ide/coq-ssreflect.lang
+++ b/ide/coq-ssreflect.lang
@@ -190,6 +190,7 @@
 	  <keyword>Eval</keyword>
 	  <keyword>Load</keyword>
 	  <keyword>Undo</keyword>
+          <keyword>Restart</keyword>
 	  <keyword>Goal</keyword>
 	  <keyword>Print</keyword>
 	  <keyword>Save</keyword>
diff --git a/ide/coq.lang b/ide/coq.lang
index 65150d6a..e25eedbc 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -5,7 +5,7 @@
     <property name="block-comment-start">\(\*</property>
     <property name="block-comment-stop">\*\)</property>
   </metadata>
-  
+
   <styles>
     <style id="comment" _name="Comment" map-to="def:comment"/>
     <style id="coqdoc" _name="Coqdoc text" map-to="def:note"/>
@@ -20,201 +20,214 @@
     <style id="safe" _name="Checked Part"/>
     <style id="sentence" _name="Sentence terminator"/>
   </styles>
-  
+
   <definitions>
     <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|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex>
+    <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</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|Universe</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>
-    </context>
-    <context id="string" style-ref="string">
+    <!-- Strings, with '""' an escape sequence -->
+    <context id="string" style-ref="string" class="string">
       <start>"</start>
       <end>"</end>
       <include>
-	<context ref="escape-seq"/>
+        <context id="string-escape" style-ref="escape">
+          <match>""</match>
+        </context>
+      </include>
+    </context>
+
+    <!-- Coqdoc comments -->
+    <context id="coqdoc" style-ref="coqdoc" class="comment" class-disabled="no-spell-check">
+      <start>\(\*\*(\s|\z)</start>
+      <end>\*\)</end>
+      <include>
+        <context ref="comment"/>
+        <context ref="string"/>
+        <context ref="def:in-comment"/>
       </include>
     </context>
+
+    <!-- Regular comments, possibly nested -->
+    <context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
+      <start>\(\*</start>
+      <end>\*\)</end>
+      <include>
+        <context ref="comment"/>
+        <context ref="string"/>
+        <context ref="def:in-comment"/>
+      </include>
+    </context>
+
+    <!-- Keywords for constr -->
+    <context id="constr-keyword" style-ref="constr-keyword">
+      <keyword>forall</keyword>
+      <keyword>fun</keyword>
+      <keyword>match</keyword>
+      <keyword>fix</keyword>
+      <keyword>cofix</keyword>
+      <keyword>with</keyword>
+      <keyword>for</keyword>
+      <keyword>end</keyword>
+      <keyword>as</keyword>
+      <keyword>let</keyword>
+      <keyword>in</keyword>
+      <keyword>if</keyword>
+      <keyword>then</keyword>
+      <keyword>else</keyword>
+      <keyword>return</keyword>
+    </context>
+
+    <!-- Sort keywords -->
+    <context id="constr-sort" style-ref="constr-sort">
+      <keyword>Prop</keyword>
+      <keyword>Set</keyword>
+      <keyword>Type</keyword>
+    </context>
+
     <context id="coq" class="no-spell-check">
       <include>
         <context ref="string"/>
-	<context id="coqdoc" style-ref="coqdoc" class-disabled="no-spell-check">
-	  <start>\(\*\*(\s|\z)</start>
-	  <end>\*\)</end>
-	  <include>
-	    <context ref="comment-in-comment"/>
-	    <context ref="string"/>
-	  </include>
-	</context>
-	<context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
-	  <start>\(\*</start>
-	  <end>\*\)</end>
-	  <include>
-	    <context id="comment-in-comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
-	      <start>\(\*</start>
-	      <end>\*\)</end>
-	      <include>
-		<context ref="comment-in-comment"/>
-		<context ref="string"/>
-	      </include>
-	    </context>
-	    <context ref="string"/>
-	  </include>
-	</context>
-	<context id="declaration">
-	  <start>\%{decl_head}</start>
-	  <end>\%{dot_sep}</end>
-	  <include>
-	    <context sub-pattern="id" where="start" style-ref="identifier"/>
-	    <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/>
-	    <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/>
-	    <context sub-pattern="id_list" where="start" style-ref="identifier"/>
-	    <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
-	    <context id="constr-keyword" style-ref="constr-keyword">
-	      <keyword>forall</keyword>
-	      <keyword>fun</keyword>
-	      <keyword>match</keyword>
-	      <keyword>fix</keyword>
-	      <keyword>cofix</keyword>
-	      <keyword>with</keyword>
-	      <keyword>for</keyword>
-	      <keyword>end</keyword>
-	      <keyword>as</keyword>
-	      <keyword>let</keyword>
-	      <keyword>in</keyword>
-	      <keyword>if</keyword>
-	      <keyword>then</keyword>
-	      <keyword>else</keyword>
-	      <keyword>return</keyword>
-	    </context>
-	    <context id="constr-sort" style-ref="constr-sort">
-	      <keyword>Prop</keyword>
-	      <keyword>Set</keyword>
-	      <keyword>Type</keyword>
-	    </context>
-	    <context id="dot-nosep">
-	      <match>\.\.</match>
-	    </context>
-	    <context ref="comment"/>
-	    <context ref="string"/>
-	    <context ref="coqdoc"/>
-	  </include>
-	</context>
-	<context id="proof">
-	  <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"/>
-	    <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
-	    <context ref="command"/>
-	    <context ref="scope-command"/>
-	    <context ref="hint-command"/>
-	    <context ref="command-for-qualit"/>
-	    <context ref="declaration"/>
-	    <context ref="comment"/>
-	    <context ref="string"/>
-	    <context ref="coqdoc"/>
-	    <context ref="proof"/>
-	    <context ref="undotted-sep"/>
-	    <context id="tactic" extend-parent="false">
-	      <start>\b[^-+*{}]</start>
-	      <end>\%{dot_sep}</end>
-	      <include>
-		<context ref="dot-nosep"/>
-		<context ref="constr-keyword"/>
-		<context ref="constr-sort"/>
-	      </include>
-	    </context>
-	  </include>
-	</context>
-	<context id="exact-proof">
-	  <start>Proof</start>
-	  <end>\%{dot_sep}</end>
-	  <include>
-	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
-	    <context ref="constr-keyword"/>
-	    <context ref="constr-sort"/>
-	  </include>
-	</context>
-	<context id="undotted-sep" style-ref="vernac-keyword">
-	  <match>\%{undotted_sep}</match>
-	</context>
-	<context id="command" style-ref="vernac-keyword">
-	  <keyword>Add</keyword>
-	  <keyword>Check</keyword>
-	  <keyword>Eval</keyword>
-	  <keyword>Load</keyword>
-	  <keyword>Undo</keyword>
-	  <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
-	  <keyword>Print</keyword>
-	  <keyword>Comments</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>Declare\%{space}ML\%{space}Module</keyword>
-	  <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword>
-	</context>
-	<context id="hint-command" style-ref="vernac-keyword">
-	  <prefix>\%{locality}Hint\%{space}</prefix>
-	  <keyword>Resolve</keyword>
-	  <keyword>Immediate</keyword>
-	  <keyword>Constructors</keyword>
-	  <keyword>Unfold</keyword>
-	  <keyword>Opaque</keyword>
-	  <keyword>Transparent</keyword>
-	  <keyword>Extern</keyword>
-	  <keyword>Rewrite</keyword>
-	</context>
-	<context id="scope-command" style-ref="vernac-keyword">
-	  <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>
-	  <keyword>Chapter</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>Include</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">
-	  <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>
+        <context ref="coqdoc"/>
+        <context ref="comment"/>
+
+        <context id="declaration">
+          <start>\%{decl_head}</start>
+          <end>\%{dot_sep}</end>
+          <include>
+            <context sub-pattern="id" where="start" style-ref="identifier"/>
+            <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/>
+            <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/>
+            <context sub-pattern="id_list" where="start" style-ref="identifier"/>
+            <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
+            <context ref="constr-keyword"/>
+            <context ref="constr-sort"/>
+            <context id="dot-nosep">
+              <match>\.\.</match>
+            </context>
+            <context ref="string"/>
+            <context ref="coqdoc"/>
+            <context ref="comment"/>
+          </include>
+        </context>
+
+        <context id="proof">
+          <start>(Proof(\%{dot_sep}|\%{space}using|\%{space}with))|Next Obligation</start>
+          <end>\%{end_proof}\%{dot_sep}</end>
+          <include>
+            <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
+            <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
+            <context ref="command-in-proof"/>
+            <context ref="string"/>
+            <context ref="coqdoc"/>
+            <context ref="comment"/>
+            <context ref="constr-keyword"/>
+            <context ref="constr-sort"/>
+            <context id="bullet" extend-parent="false">
+              <match>\%{dot_sep}\s*(?'bul'\%{bullet})</match>
+              <include>
+                <context sub-pattern="bul" style-ref="vernac-keyword"/>
+              </include>
+            </context>
+            <context id="bullet-sol" style-ref="vernac-keyword">
+              <match>^\s*\%{bullet}</match>
+            </context>
+          </include>
+        </context>
+
+        <context id="exact-proof">
+          <start>Proof</start>
+          <end>\%{dot_sep}</end>
+          <include>
+            <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
+            <context ref="constr-keyword"/>
+            <context ref="constr-sort"/>
+          </include>
+        </context>
+
+        <context id="command-in-proof" style-ref="vernac-keyword">
+          <keyword>About</keyword>
+          <keyword>Check</keyword>
+          <keyword>Print</keyword>
+          <keyword>Eval</keyword>
+          <keyword>Undo</keyword>
+          <keyword>Restart</keyword>
+          <keyword>Opaque</keyword>
+          <keyword>Transparent</keyword>
+        </context>
+
+        <context id="command" style-ref="vernac-keyword">
+          <keyword>Add</keyword>
+          <keyword>Load</keyword>
+          <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
+          <keyword>Comments</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>Declare\%{space}ML\%{space}Module</keyword>
+          <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword>
+        </context>
+
+        <context id="hint-command" style-ref="vernac-keyword">
+          <prefix>\%{locality}Hint\%{space}</prefix>
+          <keyword>Resolve</keyword>
+          <keyword>Immediate</keyword>
+          <keyword>Constructors</keyword>
+          <keyword>Unfold</keyword>
+          <keyword>Extern</keyword>
+          <keyword>Rewrite</keyword>
+        </context>
+
+        <context id="scope-command" style-ref="vernac-keyword">
+          <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>
+          <keyword>Chapter</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>Arguments</keyword>
+          <keyword>Implicit\%{space}Arguments</keyword>
+          <keyword>Include</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">
+          <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>
       </include>
     </context>
   </definitions>
diff --git a/ide/coq.mli b/ide/coq.mli
index a72c67b4..2dc5ad30 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -16,7 +16,7 @@ type coqtop
     Liveness management of coqtop is automatic. Whenever a coqtop dies abruptly,
     this module is responsible for relaunching the whole process. The reset
     handler set through [set_reset_handler] will be called after such an
-    abrupt failure. It is also called when explicitely requesting coqtop to
+    abrupt failure. It is also called when explicitly requesting coqtop to
     reset. *)
 
 type 'a task
@@ -29,7 +29,7 @@ type 'a task
     ([is_computing] will answer [true]), and any other task submission
     will be rejected by [try_grab].
 
-    Any exception occuring within the task will trigger a coqtop reset.
+    Any exception occurring within the task will trigger a coqtop reset.
 
     Beware, because of the GTK scheduler, you never know when a task will
     actually be executed. If you need to sequentialize imperative actions, you
@@ -43,7 +43,7 @@ val bind : 'a task -> ('a -> 'b task) -> 'b task
 (** Monadic binding of tasks *)
 
 val lift : (unit -> 'a) -> 'a task
-(** Return the impertative computation waiting to be processed. *)
+(** Return the imperative computation waiting to be processed. *)
 
 val seq : unit task -> 'a task -> 'a task
 (** Sequential composition *)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index af728471..c7e0810f 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -204,7 +204,7 @@ object(self)
     let on_changed (i, f) = segment#add i (flags_to_color f) in
     let on_push s =
       set_index s document_length;
-      (SentenceId.connect s)#changed on_changed;
+      ignore ((SentenceId.connect s)#changed on_changed);
       document_length <- succ document_length;
       segment#set_length document_length;
       let flags = List.map mem_flag_of_flag s.flags in
@@ -559,7 +559,7 @@ object(self)
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] ->
-            logger Pp.Error "You muse close the proof with Qed or Admitted";
+            logger Pp.Error "You must close the proof with Qed or Admitted";
             self#discard_command_queue queue;
             conclude [] 
         | `Skip(start,stop), (_,s) :: topstack ->
@@ -655,8 +655,6 @@ 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.error ~start ~stop;
-      buffer#remove_tag Tags.Script.error_bg ~start ~stop;
       buffer#move_mark ~where:start (`NAME "start_of_input")
     end;
     List.iter (fun { start } -> buffer#delete_mark start) seg;
@@ -671,7 +669,10 @@ object(self)
       push_info "Coq is undoing" in
     let conclusion () =
       pop_info ();
-      if move_insert then buffer#place_cursor ~where:self#get_start_of_input;
+      if move_insert then begin
+        buffer#place_cursor ~where:self#get_start_of_input;
+        script#recenter_insert;
+      end;
       let start = self#get_start_of_input in
       let stop = self#get_end_of_input in
       Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0f4cb7b0..f15e5fa3 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -253,14 +253,14 @@ let newfile _ =
   !refresh_editor_hook ();
   notebook#goto_page index
 
-let load sn =
-  let filename = sn.fileops#filename in
+let load _ =
+  let filename =
+    try notebook#current_term.fileops#filename
+    with Invalid_argument _ -> None in
   match select_file_for_open ~title:"Load file" ?filename () with
     | None -> ()
     | Some f -> FileAux.load_file f
 
-let load = cb_on_current_term load
-
 let save _ = on_current_term (FileAux.check_save ~saveas:false)
 
 let saveas sn =
@@ -1125,10 +1125,10 @@ let build_ui () =
 	~accel:(prefs.modifier_for_navigation^"h");*)
     item "Previous" ~label:"_Previous" ~stock:`GO_BACK
       ~callback:Nav.previous_occ
-      ~tooltip:"Previous occurence"
+      ~tooltip:"Previous occurrence"
       ~accel:(prefs.modifier_for_navigation^"less");
     item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ
-      ~tooltip:"Next occurence"
+      ~tooltip:"Next occurrence"
       ~accel:(prefs.modifier_for_navigation^"greater");
     item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document
       ~tooltip:"Fully check the document" 
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index dc52ea9a..041f2f83 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -185,13 +185,15 @@ let process_goal sigma g =
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
     string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in
-  let process_hyp d =
+  let process_hyp d (env,l) =
     let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
-    (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in
-  let hyps =
-    List.map process_hyp
-      (Termops.compact_named_context_reverse (Environ.named_context env)) in
-  { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
+    let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
+      (List.fold_right Environ.push_named d' env,
+       (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
+  let (_env, hyps) =
+    Context.fold_named_list_context process_hyp
+      (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
+  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
 let export_pre_goals pgs =
   {
@@ -289,11 +291,13 @@ let export_option_value = function
   | Goptions.BoolValue b   -> Interface.BoolValue b
   | Goptions.IntValue x    -> Interface.IntValue x
   | Goptions.StringValue s -> Interface.StringValue s
+  | Goptions.StringOptValue s -> Interface.StringOptValue s
 
 let import_option_value = function
   | Interface.BoolValue b   -> Goptions.BoolValue b
   | Interface.IntValue x    -> Goptions.IntValue x
   | Interface.StringValue s -> Goptions.StringValue s
+  | Interface.StringOptValue s -> Goptions.StringOptValue s
 
 let export_option_state s = {
   Interface.opt_sync  = s.Goptions.opt_sync;
@@ -312,6 +316,8 @@ let set_options options =
   | BoolValue b -> Goptions.set_bool_option_value name b
   | IntValue i -> Goptions.set_int_option_value name i
   | StringValue s -> Goptions.set_string_option_value name s
+  | StringOptValue (Some s) -> Goptions.set_string_option_value name s
+  | StringOptValue None -> Goptions.unset_option_value_gen None name
   in
   List.iter iter options
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 67e4bdb0..5892fb3d 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -311,7 +311,7 @@ let read_buffer = Buffer.create maxread
     I/O Exceptions are propagated. *)
 
 let read_file name buf =
-  let ic = open_in name in
+  let ic = Util.open_utf8_file_in name in
   let len = ref 0 in
   try
     while len := input ic read_string 0 maxread; !len > 0 do
diff --git a/ide/interface.mli b/ide/interface.mli
index 464e851f..767c49d2 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -61,6 +61,7 @@ type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
+  | StringOptValue of string option
 
 (** Summary of an option status *)
 type option_state = {
diff --git a/ide/preferences.ml b/ide/preferences.ml
index c59642d3..90862d06 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -190,7 +190,7 @@ let current = {
     automatic_tactics = ["trivial"; "tauto"; "auto"; "omega";
 			 "auto with *"; "intuition" ];
 
-    modifier_for_navigation = "<Control><Alt>";
+    modifier_for_navigation = "<Control>";
     modifier_for_templates = "<Control><Shift>";
     modifier_for_tactics = "<Control><Alt>";
     modifier_for_display = "<Alt><Shift>";
@@ -711,38 +711,61 @@ let configure ?(apply=(fun () -> ())) () =
       ~f:(fun s -> current.project_file_name <- s)
       current.project_file_name
   in
+  let update_modifiers prefix mds =
+    let change ~path ~key ~modi ~changed =
+      if CString.is_sub prefix path 0 then
+        ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path)
+    in
+    GtkData.AccelMap.foreach change
+  in
   let help_string =
     "restart to apply"
   in
   let the_valid_mod = str_to_mod_list current.modifiers_valid in
   let modifier_for_tactics =
+    let cb l =
+      current.modifier_for_tactics <- mod_list_to_str l;
+      update_modifiers "<Actions>/Tactics/" l
+    in
     modifiers
       ~allow:the_valid_mod
-      ~f:(fun l -> current.modifier_for_tactics <- mod_list_to_str l)
+      ~f:cb
       ~help:help_string
       "Modifiers for Tactics Menu"
       (str_to_mod_list current.modifier_for_tactics)
   in
   let modifier_for_templates =
+    let cb l =
+      current.modifier_for_templates <- mod_list_to_str l;
+      update_modifiers "<Actions>/Templates/" l
+    in
     modifiers
       ~allow:the_valid_mod
-      ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l)
+      ~f:cb
       ~help:help_string
       "Modifiers for Templates Menu"
       (str_to_mod_list current.modifier_for_templates)
   in
   let modifier_for_navigation =
+    let cb l =
+      current.modifier_for_navigation <- mod_list_to_str l;
+      update_modifiers "<Actions>/Navigation/" l
+    in
     modifiers
       ~allow:the_valid_mod
-      ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l)
+      ~f:cb
       ~help:help_string
       "Modifiers for Navigation Menu"
       (str_to_mod_list current.modifier_for_navigation)
   in
   let modifier_for_display =
+    let cb l =
+      current.modifier_for_display <- mod_list_to_str l;
+      update_modifiers "<Actions>/View/" l
+    in
     modifiers
       ~allow:the_valid_mod
-      ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l)
+      ~f:cb
       ~help:help_string
       "Modifiers for View Menu"
       (str_to_mod_list current.modifier_for_display)
diff --git a/ide/session.ml b/ide/session.ml
index 12b77966..a795f633 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -239,7 +239,7 @@ let find_int_col s l =
 let find_string_col s l =
   match List.assoc s l with `StringC c -> c | _ -> assert false
 
-let make_table_widget cd cb =
+let make_table_widget ?sort cd cb =
   let frame = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC () in
   let columns, store =
     let cols = new GTree.column_list in
@@ -253,6 +253,7 @@ let make_table_widget cd cb =
       ~rules_hint:true ~headers_visible:false
       ~model:store ~packing:frame#add () in
   let () = data#set_headers_visible true in
+  let () = data#set_headers_clickable true in
   let refresh () =
     let clr = Tags.color_of_string current.background_color in
     data#misc#modify_base [`NORMAL, `COLOR clr]
@@ -268,21 +269,34 @@ let make_table_widget cd cb =
       c#set_sizing `AUTOSIZE;
       c)
     columns cd in
+  let make_sorting i (_, c) =
+    let sort (store : GTree.model) it1 it2 = match c with
+    | `IntC c ->
+      Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c)
+    | `StringC c ->
+      Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c)
+    in
+    store#set_sort_func i sort
+  in
+  CList.iteri make_sorting columns;
+  CList.iteri (fun i c -> c#set_sort_column_id i) cols;
   List.iter (fun c -> ignore(data#append_column c)) cols;
   ignore(
     data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc)
   );
+  let () = match sort with None -> () | Some (i, t) -> store#set_sort_column_id i t in
   frame, (fun f -> f columns store), refresh
 
 let create_errpage (script : Wg_ScriptView.script_view) : errpage =
   let table, access, refresh =
-    make_table_widget
+    make_table_widget ~sort:(0, `ASCENDING)
       [`Int,"Line",true; `String,"Error message",true]
       (fun columns store tp vc ->
         let row = store#get_iter tp in
         let lno = store#get ~row ~column:(find_int_col "Line" columns) in
         let where = script#buffer#get_iter (`LINE (lno-1)) in
         script#buffer#place_cursor ~where;
+        script#misc#grab_focus ();
         ignore (script#scroll_to_iter
 		  ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in
   let tip = GMisc.label ~text:"Double click to jump to error line" () in
@@ -311,7 +325,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
 
 let create_jobpage coqtop coqops : jobpage =
   let table, access, refresh =
-    make_table_widget
+    make_table_widget ~sort:(0, `ASCENDING)
       [`String,"Worker",true; `String,"Job name",true]
       (fun columns store tp vc ->
         let row = store#get_iter tp in
diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll
index 621833dd..4ebf9a62 100644
--- a/ide/utf8_convert.mll
+++ b/ide/utf8_convert.mll
@@ -12,7 +12,7 @@
 
 }
 
-(* Replace all occurences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *)
+(* Replace all occurrences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *)
 
 let digit = ['0'-'9''A'-'Z''a'-'z']
 let short = digit digit digit digit
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index b12d29d6..69d460b0 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
+
 class type proof_view =
   object
     inherit GObj.widget
@@ -138,20 +140,22 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "No more subgoals."
     | [], [], [], _ :: _ ->
       (* A proof has been finished, but not concluded *)
-      view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
+      view#buffer#insert "No more subgoals, but there are non-instantiated existential variables:\n\n";
       let iter evar =
         let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
         view#buffer#insert msg
       in
-      List.iter iter evars
+      List.iter iter evars;
+      view#buffer#insert "\nYou can use Grab Existential Variables."
     | [], [], _, _ ->
       (* The proof is finished, with the exception of given up goals. *)
-      view#buffer#insert "No more, however there are goals you gave up. You need to go back and solve them:\n\n";
+      view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
       let iter goal =
         let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
         view#buffer#insert msg
       in
-      List.iter iter given_up_goals
+      List.iter iter given_up_goals;
+      view#buffer#insert "\nYou need to go back and solve them."
     | [], _, _, _ ->
       (* All the goals have been resolved but those on the shelf. *)
       view#buffer#insert "All the remaining goals are on the shelf:\n\n";
@@ -162,12 +166,17 @@ let display mode (view : #GText.view_skel) goals hints evars =
       List.iter iter shelved_goals
     | _, _, _, _ ->
       (* No foreground proofs, but still unfocused ones *)
-      view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
-      let iter goal =
+      let total = List.length bg in
+      let goal_str index = Printf.sprintf
+        "______________________________________(%d/%d)\n" index total
+      in
+      view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
+      let iter i goal =
+        let () = view#buffer#insert (goal_str (succ i)) in
         let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
         view#buffer#insert msg
       in
-      List.iter iter bg
+      List.iteri iter bg
     end
   | Some { Interface.fg_goals = fg } ->
     mode view fg hints
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 8298d995..ae50b283 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -139,7 +139,7 @@ object(self)
 
   (** We don't care about atomicity. Return:
     1. `OK when there was no error, `FAIL otherwise
-    2. `NOOP if no write occured, `WRITE otherwise
+    2. `NOOP if no write occurred, `WRITE otherwise
   *)
   method private process_action = function
   | Insert ins ->
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d337a911..84fd8929 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -62,10 +62,12 @@ let of_option_value = function
   | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i]
   | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b]
   | StringValue s -> constructor "option_value" "stringvalue" [of_string s]
+  | StringOptValue s -> constructor "option_value" "stringoptvalue" [of_option of_string s]
 let to_option_value = do_match "option_value" (fun s args -> match s with
   | "intvalue" -> IntValue (to_option to_int (singleton args))
   | "boolvalue" -> BoolValue (to_bool (singleton args))
   | "stringvalue" -> StringValue (to_string (singleton args))
+  | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args))
   | _ -> raise Marshal_error)
 
 let of_option_state s =
@@ -337,6 +339,8 @@ end = struct
     | IntValue None -> "none"
     | IntValue (Some i) -> string_of_int i
     | StringValue s -> s
+    | StringOptValue None -> "none"
+    | StringOptValue (Some s) -> s
     | BoolValue b -> if b then "true" else "false"
   let pr_option_state (s : option_state) =
     Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"