From 2834cf72add1459d7460e3c1757e7352a1ff7466 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Sep 2015 10:34:19 +0200 Subject: Extending the grammar for CoqIDE preferences so as to match trunk. --- ide/config_lexer.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 87cc6d06e..367153568 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 -- cgit v1.2.3 From 77101ea44d88983ec399c8662b81f9392d92110b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Sep 2015 10:40:49 +0200 Subject: Fixing the XML lexer definition of names to match the standard. --- lib/xml_lexer.mll | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll index f6943dd13..0b541ee04 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 } -- cgit v1.2.3 From 3140d22d75ac3f30e97c799a05819b8838d167ca Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Sep 2015 10:54:41 +0200 Subject: Fixing previous patch. --- lib/xml_lexer.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll index 0b541ee04..290f2c89a 100644 --- a/lib/xml_lexer.mll +++ b/lib/xml_lexer.mll @@ -89,7 +89,7 @@ let newline = ['\n'] let break = ['\r'] let space = [' ' '\t'] let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.'] -let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar+ +let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar* let entitychar = ['A'-'Z' 'a'-'z'] let pcchar = [^ '\r' '\n' '<' '>' '&'] -- cgit v1.2.3 From 238725dd24d43574690b0111761b705753d3bee2 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 27 Apr 2015 15:40:48 +0200 Subject: typo in refman. --- doc/refman/RefMan-uti.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3 From 490160d25d3caac1d2ea5beebbbebc959b1b3832 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 7 Jun 2015 14:39:18 +0200 Subject: Fixing bug #2498: Coqide navigation preferences delayed effect. --- ide/preferences.ml | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/ide/preferences.ml b/ide/preferences.ml index c59642d3a..1bd9f587c 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -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 "/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 "/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 "/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 "/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) -- cgit v1.2.3