diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq-ssreflect.lang | 2 | ||||
| -rw-r--r-- | ide/coq.lang | 2 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 12 |
3 files changed, 4 insertions, 12 deletions
diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang index 7cfc167018..bd9cb4bfa2 100644 --- a/ide/coq-ssreflect.lang +++ b/ide/coq-ssreflect.lang @@ -228,7 +228,7 @@ <keyword>Implicit\%{space}+Arguments</keyword> <keyword>(Import)|(Include)</keyword> <keyword>Require(\%{space}+((Import)|(Export)))?</keyword> - <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</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> <include> <context sub-pattern="1" style-ref="vernac-keyword"/> diff --git a/ide/coq.lang b/ide/coq.lang index 484264ece3..e9eab48de7 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -188,7 +188,7 @@ <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> + <keyword>Extraction\%{space}Language\%{space}(OCaml|Haskell|Scheme|JSON)</keyword> </context> <context id="hint-command" style-ref="vernac-keyword"> diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index cfc0e09a0c..58599a14dc 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -13,7 +13,6 @@ open Util open Pp open Printer -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration @@ -377,15 +376,8 @@ let init = match file with | None -> init_sid | Some file -> - let dir = Filename.dirname file in - let open Loadpath in let open CUnix in let doc, initial_id, _ = - let doc = get_doc () in - if not (is_in_load_paths (physical_path_of_string dir)) then begin - let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in - let loc_ast = Stm.parse_sentence ~doc init_sid pa in - Stm.add false ~doc ~ontop:init_sid loc_ast - end else doc, init_sid, `NewTip in + get_doc (), init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; set_doc (Stm.finish ~doc); @@ -517,7 +509,7 @@ let rec parse = function let () = Coqtop.toploop_init := (fun args -> let args = parse args in Flags.quiet := true; - CoqworkmgrApi.(init Flags.High); + CoqworkmgrApi.(init High); args) let () = Coqtop.toploop_run := loop |