diff options
| -rw-r--r-- | .depend | 11 | ||||
| -rw-r--r-- | Makefile | 15 | ||||
| -rw-r--r-- | ide/.cvsignore | 2 | ||||
| -rw-r--r-- | ide/config_lexer.mll | 96 | ||||
| -rw-r--r-- | ide/config_parser.mly | 34 | ||||
| -rw-r--r-- | ide/ideutils.ml | 2 | ||||
| -rw-r--r-- | ide/preferences.ml | 176 |
7 files changed, 174 insertions, 162 deletions
@@ -1,3 +1,4 @@ +ide/config_parser.cmi: lib/util.cmi ide/coq.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo interp/constrextern.cmi: kernel/environ.cmi library/impargs.cmi \ @@ -475,6 +476,10 @@ doc/parse.cmo: parsing/ast.cmi doc/parse.cmx: parsing/ast.cmx ide/command_windows.cmo: ide/coq.cmi ide/coq_commands.cmo ide/ideutils.cmo ide/command_windows.cmx: ide/coq.cmx ide/coq_commands.cmx ide/ideutils.cmx +ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi +ide/config_lexer.cmx: ide/config_parser.cmx lib/util.cmx +ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi +ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ tactics/hipattern.cmi ide/ideutils.cmo library/lib.cmi kernel/names.cmi \ @@ -505,8 +510,10 @@ ide/ideutils.cmo: config/coq_config.cmi lib/options.cmi lib/pp_control.cmi \ ide/preferences.cmo ide/ideutils.cmx: config/coq_config.cmx lib/options.cmx lib/pp_control.cmx \ ide/preferences.cmx -ide/preferences.cmo: ide/utils/configwin.cmi ide/utils/editable_cells.cmo -ide/preferences.cmx: ide/utils/configwin.cmx ide/utils/editable_cells.cmx +ide/preferences.cmo: ide/config_lexer.cmo ide/utils/configwin.cmi \ + ide/utils/editable_cells.cmo lib/util.cmi +ide/preferences.cmx: ide/config_lexer.cmx ide/utils/configwin.cmx \ + ide/utils/editable_cells.cmx lib/util.cmx ide/undo.cmo: ide/ideutils.cmo ide/undo.cmi ide/undo.cmx: ide/ideutils.cmx ide/undo.cmi interp/constrextern.cmo: pretyping/classops.cmi library/declare.cmi \ @@ -386,8 +386,8 @@ COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \ ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \ ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \ ide/utils/configwin.cmo \ - ide/utils/editable_cells.cmo ide/config_lexer.cmo \ - ide/preferences.cmo \ + ide/utils/editable_cells.cmo ide/config_parser.cmo \ + ide/config_lexer.cmo ide/preferences.cmo \ ide/ideutils.cmo ide/undo.cmo \ ide/find_phrase.cmo \ ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \ @@ -396,6 +396,7 @@ COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \ COQIDECMX=$(COQIDECMO:.cmo=.cmx) COQIDEFLAGS=-thread -I +lablgtk2 beforedepend:: ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml +beforedepend:: ide/config_parser.mli ide/config_parser.ml FULLIDELIB=$(FULLCOQLIB)/ide IDEFILES=ide/coq.png ide/.coqiderc @@ -429,6 +430,8 @@ ide/utils/%.cmi: ide/%.mli ide/utils/%.cmx: ide/%.ml $(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< clean:: + rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml + rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml rm -f $(COQIDEBYTE) $(COQIDEOPT) # coqc @@ -1101,7 +1104,7 @@ parsing/lexer.cmo: parsing/lexer.ml4 # Default rules ########################################################################### -.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4 .v .vo .el .elc +.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .mly .ml4 .v .vo .el .elc .ml.cmo: $(OCAMLC) $(BYTEFLAGS) -c $< @@ -1115,6 +1118,12 @@ parsing/lexer.cmo: parsing/lexer.ml4 .mll.ml: ocamllex $< +.mly.ml: + ocamlyacc $< + +.mly.mli: + ocamlyacc $< + .ml4.cmx: $(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $< diff --git a/ide/.cvsignore b/ide/.cvsignore index 331b1947b..56eea49c9 100644 --- a/ide/.cvsignore +++ b/ide/.cvsignore @@ -8,3 +8,5 @@ Makefile test config_lexer.ml *.crashcoqide +config_parser.mli +config_parser.ml diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 0d0e6307e..480f04e24 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,60 +1,58 @@ { open Lexing + open Format + open Config_parser + open Util + + let string_buffer = Buffer.create 1024 + } -let space = - [' ' '\010' '\013' '\009' '\012'] +let space = [' ' '\010' '\013' '\009' '\012'] let char = ['A'-'Z' 'a'-'z' '_' '0'-'9'] - let ident = char+ -let value = ('"'|'[')( [^ '='] | ('\\''"') )*('"'|']') -let list_value = [^';']+ ';' - -rule next_config = parse - | ident - { let id = lexeme lexbuf in - let v = value lexbuf in - (id,v) - } - | _ { next_config lexbuf} - | eof { raise End_of_file } - -and value = parse - | value { let s = lexeme lexbuf in - String.sub s 1 (String.length s - 2)} - | _ { value lexbuf } - | eof { raise End_of_file } - -and split_list = parse - | list_value { - let h = lexeme lexbuf in - h::(split_list lexbuf) - } - | _ { split_list lexbuf} - | eof {[]} +rule token = parse + | space+ { token lexbuf } + | '#' [^ '\n']* { token lexbuf } + | ident { IDENT (lexeme lexbuf) } + | '=' { EQUAL } + | '"' { Buffer.reset string_buffer; + Buffer.add_char string_buffer '"'; + string lexbuf; + let s = Buffer.contents string_buffer in + STRING (Scanf.sscanf s "%S" (fun s -> s)) } + | _ { let c = lexeme_start lexbuf in + eprintf ".coqiderc: invalid character (%d)\n@." c; + token lexbuf } + | eof { EOF } + +and string = parse + | '"' { Buffer.add_char string_buffer '"' } + | '\\' '"' | _ + { Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf } + | eof { eprintf ".coqiderc: unterminated string\n@." } { - let get_config f = - let ci = open_in f in - let lb = from_channel ci in - let result = ref [] in - begin try - while true do - let r = next_config lb in - result := r::!result - done - with End_of_file -> close_in ci; - end; - !result - - let split s = - let cs = ref "" in - let l = ref [] in - String.iter - (fun c -> if c = ';' then begin l:= !cs::!l; cs:="" end - else cs := !cs^(Char.escaped c)) - s; - if !cs ="" then !l else !cs::!l + + let load_file f = + let c = open_in f in + let lb = from_channel c in + let m = Config_parser.prefs token lb in + close_in c; + m + + let print_file f m = + let c = open_out f in + let fmt = formatter_of_out_channel c in + let rec print_list fmt = function + | [] -> () + | s :: sl -> fprintf fmt "%S@ %a" s print_list sl + in + Stringmap.iter + (fun k s -> fprintf fmt "@[<hov 2>%s = %a@]@\n" k print_list s) m; + fprintf fmt "@."; + close_out c + } diff --git a/ide/config_parser.mly b/ide/config_parser.mly new file mode 100644 index 000000000..fe9071964 --- /dev/null +++ b/ide/config_parser.mly @@ -0,0 +1,34 @@ + +%{ + + open Parsing + open Util + +%} + +%token <string> IDENT STRING +%token EQUAL EOF + +%type <(string list) Util.Stringmap.t> prefs +%start prefs + +%% + +prefs: + pref_list EOF { $1 } +; + +pref_list: + pref_list pref { let (k,d) = $2 in Stringmap.add k d $1 } + | /* epsilon */ { Stringmap.empty } +; + +pref: + IDENT EQUAL string_list { ($1, List.rev $3) } +; + +string_list: + string_list STRING { $2 :: $1 } + | /* epsilon */ { [] } +; + diff --git a/ide/ideutils.ml b/ide/ideutils.ml index d5d1490fe..f0f54650e 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -200,3 +200,5 @@ let find_tag_limits (tag :GText.tag) (it:GText.iter) = let async = if Sys.os_type <> "Unix" then GtkThread.async else (fun x -> x) + + diff --git a/ide/preferences.ml b/ide/preferences.ml index c78cf3214..4370ca985 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,5 +1,6 @@ open Configwin open Printf +open Util let pref_file = try (Filename.concat (Sys.getenv "HOME") ".coqidepref") @@ -50,7 +51,7 @@ type pref = mutable auto_save : bool; mutable auto_save_delay : int; - mutable auto_save_name : string*string; + mutable auto_save_name : string * string; mutable automatic_tactics : (string * string) list; mutable cmd_print : string; @@ -68,61 +69,34 @@ type pref = let save_pref p = try - let fd = open_out pref_file in - output_value fd p; -(* - let output_string f c = fprintf fd "%s = \"%s\"\n" f c in - let output_bool f c = fprintf fd "%s = \"%b\"\n" f c in - let output_int f c = fprintf fd "%s = \"%d\"\n" f c in - let output_list f to_string l = - fprintf fd "%s = [%a]\n" f - (fun c -> - List.iter - (fun x -> fprintf c "%a;" to_string x)) l in - let output_modi fd m = fprintf fd "%s" (mod_to_str m) in - let output_tactics fd (m1,m2) = fprintf fd "%s,%s" m1 m2 in - output_string "cmd_coqc" p.cmd_coqc; - output_string "cmd_make" p.cmd_make; - output_string "cmd_coqmakefile" p.cmd_coqmakefile; - output_string "cmd_coqdoc" p.cmd_coqdoc; - output_string "cmd_print" p.cmd_print; - - output_bool "global_auto_revert" p.global_auto_revert; - output_int "global_auto_revert_delay" p.global_auto_revert_delay; - - output_bool "auto_save" p.auto_save; - output_int "auto_save_delay" p.auto_save_delay; - output_string "auto_save_prefix" (fst p.auto_save_name); - output_string "auto_save_suffix" (snd p.auto_save_name); - - output_string "cmd_browse_prefix" (fst p.cmd_browse); - output_string "cmd_browse_suffix" (snd p.cmd_browse); - - output_string "doc_url" p.doc_url; - output_string "library_url" p.library_url; - output_list - "modifier_for_navigation" - output_modi - p.modifier_for_navigation; - output_list - "modifier_for_templates" - output_modi - p.modifier_for_templates; - output_list - "modifier_for_tactics" - output_modi - p.modifier_for_navigation; - output_list - "modifiers_valid" - output_modi - p.modifiers_valid; - output_list - "automatic_tactics" - output_tactics - p.automatic_tactics; -*) - close_out fd - + let add = Stringmap.add in + let (++) x f = f x in + Stringmap.empty ++ + add "cmd_coqc" [p.cmd_coqc] ++ + add "cmd_make" [p.cmd_make] ++ + add "cmd_coqmakefile" [p.cmd_coqmakefile] ++ + add "cmd_coqdoc" [p.cmd_coqdoc] ++ + add "global_auto_revert" [string_of_bool p.global_auto_revert] ++ + add "global_auto_revert_delay" + [string_of_int p.global_auto_revert_delay] ++ + add "auto_save" [string_of_bool p.auto_save] ++ + add "auto_save_delay" [string_of_int p.auto_save_delay] ++ + add "auto_save_name" [fst p.auto_save_name; snd p.auto_save_name] ++ + add "automatic_tactics" + (List.fold_left (fun l (v1,v2) -> v1::v2::l) [] p.automatic_tactics) ++ + add "cmd_print" [p.cmd_print] ++ + add "modifier_for_navigation" + (List.map mod_to_str p.modifier_for_navigation) ++ + add "modifier_for_templates" + (List.map mod_to_str p.modifier_for_templates) ++ + add "modifier_for_tactics" + (List.map mod_to_str p.modifier_for_tactics) ++ + add "modifiers_valid" + (List.map mod_to_str p.modifiers_valid) ++ + add "cmd_browse" [fst p.cmd_browse; snd p.cmd_browse] ++ + add "doc_url" [p.doc_url] ++ + add "library_url" [p.library_url] ++ + Config_lexer.print_file pref_file with _ -> prerr_endline "Could not save preferences." let (current:pref ref) = @@ -163,58 +137,44 @@ let (current:pref ref) = let load_pref p = try -(* let l = Config_lexer.get_config pref_file in - List.iter - (function k,v -> try match k with - | "cmd_coqc" -> p.cmd_coqc <- v - | "cmd_make" -> p.cmd_make <- v - | "cmd_coqmakefile" -> p.cmd_coqmakefile <- v - | "cmd_coqdoc" -> p.cmd_coqdoc <- v - | "cmd_print" -> p.cmd_print <- v - | "global_auto_revert" -> p.global_auto_revert <- bool_of_string v - | "global_auto_revert_delay" -> - p.global_auto_revert_delay <- int_of_string v - | "auto_save" -> p.auto_save <- bool_of_string v - | "auto_save_delay" -> p.auto_save_delay <- int_of_string v - | "auto_save_prefix" -> - let x,y = p.auto_save_name in - p.auto_save_name <- (v,y) - | "auto_save_suffix" -> - let x,y = p.auto_save_name in - p.auto_save_name <- (x,v) - - | "cmd_browse_prefix" -> - let x,y = p.cmd_browse in - p.cmd_browse <- (v,y) - | "cmd_browse_suffix" -> - let x,y = p.cmd_browse in - p.cmd_browse <- (x,v) - | "doc_url" -> p.doc_url <- v - | "library_url" -> p.library_url <- v - | "modifier_for_navigation" -> - p.modifier_for_navigation <- - List.rev_map str_to_mod (Config_lexer.split v) - | "modifier_for_templates" -> - p.modifier_for_templates <- - List.rev_map str_to_mod (Config_lexer.split v) - | "modifier_for_tactics" -> - p.modifier_for_tactics <- - List.rev_map str_to_mod (Config_lexer.split v) - | "modifiers_valid" -> - p.modifiers_valid <- - List.rev_map str_to_mod (Config_lexer.split v) - | "automatic_tactics" -> - p.automatic_tactics <- - List.map (fun x -> Pervasives.prerr_endline x;(x,"")) (Config_lexer.split v) - | _ -> prerr_endline ("Warning: unknown option "^k) - with _ -> ()) - l -*) - let cin = open_in pref_file in - let (new_pref:pref) = input_value cin in - close_in cin; - current := new_pref - with _ -> prerr_endline "Could not load preferences." + let m = Config_lexer.load_file pref_file in + let np = { !p with cmd_coqc = !p.cmd_coqc } in + let set k f = try let v = Stringmap.find k m in f v with _ -> () in + let set_hd k f = set k (fun v -> f (List.hd v)) in + let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in + let set_int k f = set_hd k (fun v -> f (int_of_string v)) in + let set_pair k f = set k (function [v1;v2] -> f v1 v2 | _ -> raise Exit) in + set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v); + set_hd "cmd_make" (fun v -> np.cmd_make <- v); + set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v); + set_hd "cmd_coqdoc" (fun v -> np.cmd_coqdoc <- v); + set_bool "global_auto_revert" (fun v -> np.global_auto_revert <- v); + set_int "global_auto_revert_delay" + (fun v -> np.global_auto_revert_delay <- v); + set_bool "auto_save" (fun v -> np.auto_save <- v); + set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v); + set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2)); + set "automatic_tactics" + (fun v -> + let rec from_list = function + | [] | [_] -> [] + | x :: y :: l -> (x,y) :: from_list l + in + np.automatic_tactics <- from_list v); + set_hd "cmd_print" (fun v -> np.cmd_print <- v); + set "modifier_for_navigation" + (fun v -> np.modifier_for_navigation <- List.map str_to_mod v); + set "modifier_for_templates" + (fun v -> np.modifier_for_templates <- List.map str_to_mod v); + set "modifier_for_tactics" + (fun v -> np.modifier_for_tactics <- List.map str_to_mod v); + set "modifiers_valid" + (fun v -> np.modifiers_valid <- List.map str_to_mod v); + set_pair "cmd_browse" (fun v1 v2 -> np.cmd_browse <- (v1,v2)); + set_hd "doc_url" (fun v -> np.doc_url <- v); + set_hd "library_url" (fun v -> np.library_url <- v); + current := np + with e -> prerr_endline (Printexc.to_string e); prerr_endline "Could not load preferences." let configure () = let cmd_coqc = |