diff options
| -rw-r--r-- | .gitignore | 4 | ||||
| -rw-r--r-- | Makefile.dev | 20 | ||||
| -rw-r--r-- | doc/changelog/08-tools/11523-coqdep+refactor2.rst | 13 | ||||
| -rw-r--r-- | ide/coq.ml | 6 | ||||
| -rw-r--r-- | ide/coqide.ml | 5 | ||||
| -rw-r--r-- | ide/ideutils.ml | 13 | ||||
| -rw-r--r-- | ide/ideutils.mli | 2 |
7 files changed, 32 insertions, 31 deletions
diff --git a/.gitignore b/.gitignore index 489e6211a7..b665b2f86d 100644 --- a/.gitignore +++ b/.gitignore @@ -115,9 +115,7 @@ doc/stdlib/index-list.html doc/tools/docgram/productionlistGrammar doc/tools/docgram/editedGrammar doc/tools/docgram/prodnGrammar -doc/tutorial/Tutorial.v.out -doc/RecTutorial/RecTutorial.html -doc/RecTutorial/RecTutorial.ps +doc/unreleased.rst # .mll files diff --git a/Makefile.dev b/Makefile.dev index b1e142333a..6e9b5356ab 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -140,17 +140,17 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ ### 4) plugins ################ -OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) -MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) -RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) -NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) -FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) -BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) -RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) -EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) +OMEGAVO:=$(filter theories/omega/%, $(THEORIESVO)) +MICROMEGAVO:=$(filter theories/micromega/%, $(THEORIESVO)) +RINGVO:=$(filter theories/setoid_ring/%, $(THEORIESVO)) +NSATZVO:=$(filter theories/nsatz/%, $(THEORIESVO)) +FUNINDVO:=$(filter theories/funind/%, $(THEORIESVO)) +BTAUTOVO:=$(filter theories/btauto/%, $(THEORIESVO)) +RTAUTOVO:=$(filter theories/rtauto/%, $(THEORIESVO)) +EXTRACTIONVO:=$(filter theories/extraction/%, $(THEORIESVO)) CCVO:= -DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) -LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO)) +DERIVEVO:=$(filter theories/derive/%, $(THEORIESVO)) +LTACVO:=$(filter theories/ltac/%, $(THEORIESVO)) omega: $(OMEGAVO) $(OMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) diff --git a/doc/changelog/08-tools/11523-coqdep+refactor2.rst b/doc/changelog/08-tools/11523-coqdep+refactor2.rst index 90c23d8b76..32a4750b73 100644 --- a/doc/changelog/08-tools/11523-coqdep+refactor2.rst +++ b/doc/changelog/08-tools/11523-coqdep+refactor2.rst @@ -1,7 +1,10 @@ - **Changed:** - Internal options and behavior of ``coqdep`` have changed, in particular - options ``-w``, ``-D``, ``-mldep``, and ``-dumpbox`` have been removed, - and ``-boot`` will not load any path by default, ``-R/-Q`` should be - used instead - (`#11523 <https://github.com/coq/coq/pull/11523>`_, + Internal options and behavior of ``coqdep`` have changed. ``coqdep`` + no longer works as a replacement for ``ocamldep``, thus ``.ml`` + files are not supported as input. Also, several deprecated options + have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``, + ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will + not load any path by default now, ``-R/-Q`` should be used instead. + (`#11523 <https://github.com/coq/coq/pull/11523>`_ and + `#11589 <https://github.com/coq/coq/pull/11589>`_, by Emilio Jesus Gallego Arias). diff --git a/ide/coq.ml b/ide/coq.ml index 4d6ba55d76..0c6aef0305 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -133,10 +133,10 @@ and asks_for_coqtop args = ~filter:false ~filename:(coqtop_path ()) () in match file with - | Some _ -> - let () = custom_coqtop := file in + | [file] -> + let () = custom_coqtop := Some file in filter_coq_opts args - | None -> exit 0 + | _ -> exit 0 exception WrongExitStatus of string diff --git a/ide/coqide.ml b/ide/coqide.ml index ccf6d40b2b..143a12deeb 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -282,9 +282,8 @@ let load ?parent _ = let filename = try notebook#current_term.fileops#filename with Invalid_argument _ -> None in - match select_file_for_open ~title:"Load file" ?parent ?filename () with - | None -> () - | Some f -> FileAux.load_file f + let filenames = select_file_for_open ~title:"Load file" ~multiple:true ?parent ?filename () in + List.iter FileAux.load_file filenames let save ?parent _ = on_current_term (FileAux.check_save ?parent ~saveas:false) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 1cf065cf25..38da229d61 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -259,7 +259,7 @@ let current_dir () = match project_path#get with | None -> "" | Some dir -> dir -let select_file_for_open ~title ?(filter=true) ?parent ?filename () = +let select_file_for_open ~title ?(filter=true) ?(multiple=false) ?parent ?filename () = let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ?parent () in @@ -271,6 +271,7 @@ let select_file_for_open ~title ?(filter=true) ?parent ?filename () = file_chooser#add_filter (filter_all_files ()) end; file_chooser#set_default_response `OPEN; + file_chooser#set_select_multiple multiple; let dir = match filename with | None -> current_dir () | Some f -> Filename.dirname f in @@ -279,12 +280,12 @@ let select_file_for_open ~title ?(filter=true) ?parent ?filename () = match file_chooser#run () with | `OPEN -> begin - match file_chooser#filename with - | None -> None - | Some _ as f -> - project_path#set file_chooser#current_folder; f + let filenames = file_chooser#get_filenames in + (if filenames <> [] then + project_path#set file_chooser#current_folder); + filenames end - | `DELETE_EVENT | `CANCEL -> None in + | `DELETE_EVENT | `CANCEL -> [] in file_chooser#destroy (); file diff --git a/ide/ideutils.mli b/ide/ideutils.mli index bacb273657..af30cd2b05 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -31,7 +31,7 @@ val find_tag_start : GText.tag -> GText.iter -> GText.iter val find_tag_stop : GText.tag -> GText.iter -> GText.iter val select_file_for_open : - title:string -> ?filter:bool -> ?parent:GWindow.window -> ?filename:string -> unit -> string option + title:string -> ?filter:bool -> ?multiple:bool -> ?parent:GWindow.window -> ?filename:string -> unit -> string list val select_file_for_save : title:string -> ?parent:GWindow.window -> ?filename:string -> unit -> string option val try_convert : string -> string |