Merge branch 'v8.5'

3 files changed, 21 insertions, 4 deletions

diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 072939106..c282083b5 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -102,7 +102,7 @@ generator using for instance the command:
 
 This command generates a file \texttt{Makefile} that can be used to
 compile all the sources of the current project. It follows the
-syntax described by the output of \texttt{\% coq\_makefile --help}.
+syntax described by the output of \texttt{\% coq\_makefile ----help}.
 Once the \texttt{Makefile} file has been generated a first time, it
 can be used by the \texttt{make} command to compile part or all of
 the project. Note that once it has been generated once, as soon as
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 8520cce0d..765dc7e59 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -248,6 +248,17 @@ let automatic_tactics =
 let cmd_print =
   new preference ~name:["cmd_print"] ~init:"lpr" ~repr:Repr.(string)
 
+let attach_modifiers (pref : string preference) prefix =
+  let cb mds =
+    let mds = str_to_mod_list mds in
+    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
+  pref#connect#changed cb
+
 let modifier_for_navigation =
   new preference ~name:["modifier_for_navigation"] ~init:"<Control><Alt>" ~repr:Repr.(string)
 
@@ -260,6 +271,11 @@ let modifier_for_tactics =
 let modifier_for_display =
   new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string)
 
+let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/"
+let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/"
+let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/"
+let _ = attach_modifiers modifier_for_display "<Actions>/View/"
+
 let modifiers_valid =
   new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)
 
diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
index f6943dd13..290f2c89a 100644
--- a/lib/xml_lexer.mll
+++ b/lib/xml_lexer.mll
@@ -88,7 +88,8 @@ let error lexbuf e =
 let newline = ['\n']
 let break = ['\r']
 let space = [' ' '\t']
-let identchar =  ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-']
+let identchar =  ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.']
+let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar*
 let entitychar = ['A'-'Z' 'a'-'z']
 let pcchar = [^ '\r' '\n' '<' '>' '&']
 
@@ -226,7 +227,7 @@ and entity = parse
                 { raise (Error EUnterminatedEntity) }
 
 and ident_name = parse
-        | identchar+
+        | ident
                 { lexeme lexbuf }
         | _ | eof
                 { error lexbuf EIdentExpected }
@@ -252,7 +253,7 @@ and attributes = parse
                 }
 
 and attribute = parse
-        | identchar+
+        | ident
                 { lexeme lexbuf }
         | _ | eof
                 { error lexbuf EAttributeNameExpected }