aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
| | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
* Merge PR #7419: Remove 100 occurrences of Evd.emptyGravatar Pierre-Marie Pédrot2018-05-28
|\
| * Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
| | | | | | | | We address the easy ones, but they should probably be all removed.
* | [ide] Move common protocol library to its own folder/object.Gravatar Emilio Jesus Gallego Arias2018-05-24
|/ | | | | | | | | | | | | | | | | The `ide` folder contains two different binaries, the language server `coqidetop` and `coqide` itself. Even if these binaries are in the same folder, the only thing they have in common is that they link to the protocol files. In the OCaml world, having "doubly" linked files in the same project is considered a bit of an ugly practice, and some build tools such as Dune disallow it.q Thus, to clean up the build, we move the common protocol files to its own library `ideprotocol`. This helps towards Dune integration and towards having an IDE standalone target, such as the one that was implemented here: https://github.com/ejgallego/coqide-exp
* [ide] Remove special option `-ideslave`Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag.
* [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
* [ide] Don't set `quiet` on start.Gravatar Emilio Jesus Gallego Arias2018-05-16
| | | | | | | | | This makes `coqidetop` behavior consistent with the one of `coqtop`. This was likely needed in the past when Coq used to print all kind of stuff to stdout, including goal display. Now, it is not the case anymore and this flag mainly controls printing verbosity.
* Merge PR #7224: Attempt to fix the doubly encapsulated Ltac errors in coqideGravatar Enrico Tassi2018-05-15
|\
* | [toplevel] let toploop_init change Coq optionsGravatar Enrico Tassi2018-04-19
| | | | | | | | | | Toplevels may want to modify for example the Stm flags, which after #1108 are handled in a functional way.
* | Merge PR #7096: coqide: avoid marking sentences that are not in the document ↵Gravatar Pierre-Marie Pédrot2018-04-12
|\ \ | | | | | | | | | anymore
| | * Attempt to fix the doubly encapsulated Ltac errors in coqide.Gravatar Hugo Herbelin2018-04-12
| |/ |/| | | | | | | | | | | | | | | | | | | | | It seems that ExplainErr.process_vernac_interp_error is called twice in CoqIDE. First time in Stm.stm_vernac_interp (via Stm.call_process_error_once). Second time in the "handle_exn" method used by CoqIDE to handle exceptions coming from Coq (ide_slave.ml/xmlprotocol.ml). The proposed fix is to remove the call in CoqIDE, assuming that the process_vernac_interp_error call is done otherwise on all potential error paths.
* | Remove unused script.Gravatar Théo Zimmermann2018-04-05
| | | | | | | | | | | | This is dead code since fd44a40f9d426a7b65f167bc30d320a0f7dd2bbd. This script was initially introduced in a088d03434417e935df3c75f81a954eadbdfc2b8 and left untouched since then.
| * coqide: avoid marking sentences that are not in the document anymoreGravatar Enrico Tassi2018-03-28
|/
* [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
| | | | | | This is a first step towards moving REPL-specific commands out of the core layers. In particular, we remove `Quit` and `Drop` from the core vernacular to specific toplevel-level parsing rules.
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | | | | The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now.
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes.
* Merge PR #6923: Export optionsGravatar Maxime Dénès2018-03-09
|\
| * Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
| | | | | | | | | | | | | | This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313.
| * Export the various option localities in the API.Gravatar Pierre-Marie Pédrot2018-03-09
| | | | | | | | This prevents relying on an underspecified bool option argument.
* | coqide: queries from the query window are routed there (fix #5684)Gravatar Enrico Tassi2018-03-08
|/ | | | | | | We systematically use Wg_MessageView for both the message panel and each Query tab; we register all MessageView in a RoutedMessageViews where the default route (0) is the message panel. Queries from the Query panel pick a non zero route to have their feedback message delivered to their MessageView
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag.
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Merge PR #6753: [toplevel] Make toplevel state into a record.Gravatar Maxime Dénès2018-02-19
|\
* \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Gravatar Maxime Dénès2018-02-19
|\ \ | | | | | | | | | camlp4
| * | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | | | | | longer use camlp4.
| | * [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
| | | | | | | | | | | | | | | | | | We organize the toplevel execution as a record and pass it around. This will be used by future PRs as to for example decouple goal printing from the classifier.
| | * [ide] Localize a IDE-specific flag.Gravatar Emilio Jesus Gallego Arias2018-02-15
| |/ |/|
* | [toplevel] Refactor command line argument handling.Gravatar Emilio Jesus Gallego Arias2018-02-09
|/ | | | | | | | | | We mostly separate command line argument parsing from interpretation, some (minor) imperative actions are still done at argument parsing time. This tidies up the code quite a bit and allows to better follow the complicated command line handling code. To this effect, we group the key actions to be performed by the toplevel into a new record type. There is still room to improve.
* allow vernacular controls before focus selector, issue #6587Gravatar Paul Steckler2018-01-26
|
* Merge PR #6625: Update location on tab switch, issue 6624Gravatar Maxime Dénès2018-01-22
|\
| * update location on tab switch, issue 6624Gravatar Paul Steckler2018-01-19
| |
* | add flash infos about wrap, not found, no. of replacements, no. of finds, ↵Gravatar Paul Steckler2018-01-18
|/ | | | issue #6452
* Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\
* | Add interfaces for IDE and remove dead code.Gravatar Maxime Dénès2018-01-10
| | | | | | | | Should fix #6177, which was triggered by lonely .ml files.
| * Brackets support single numbered goal selectors.Gravatar Théo Zimmermann2018-01-05
|/ | | | | This allows to focus on a sub-goal other than the first one without resorting to the `Focus` command.
* Remove query-in-IDE warning.Gravatar Maxime Dénès2017-12-27
| | | | | | | I don't understand what is wrong with putting a query in a script running in the IDE. It is typically needed when giving demos, and that sounds like a ligitimate use case. By the way, we do it ourselves every year during the demo at CoqPL...
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
| | | | | | | | | | | | Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
* Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵Gravatar Maxime Dénès2017-12-18
|\ | | | | | | Extraction Language command
* \ Merge PR #1108: [stm] Reorganize flagsGravatar Maxime Dénès2017-12-13
|\ \
| * | [flags] [stm] Reorganize flags.Gravatar Emilio Jesus Gallego Arias2017-12-11
| | | | | | | | | | | | | | | | | | | | | | | | We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag.
| | * use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguageGravatar Paul Steckler2017-12-05
| |/
* / Don't Add LoadPath on CoqIDE startup, #6153Gravatar Paul Steckler2017-12-05
|/
* [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
| | | | | | | | | | | | I followed what seems to be the intention of the code, with the original intention of remove the global imperative proof state. However, I fully fail to see why the new API is better than the old one. In fact the opposite seems the contrary. Still big parts of the "new proof engine" seem unfinished, and I'm afraid I am not the right person to know what direction things should take.
* [ci] [coq] Complete 4.06.0 support.Gravatar Emilio Jesus Gallego Arias2017-11-13
| | | | | | | | | | | | | Due to an API change in laglgtk, we need to update CoqIDE. We use a makefile hack so it can compile with lablgtk < 2.8.16, another option would be to require 2.8.16 as a minimal dependency. We also refactor travis to test more lablgtk versions. We also need to account for improved attribute handling in 4.06.0, in particular module aliases will propagate the deprecation status. Fixes #6140.
* Little code restructuration in CoqIDE tags.Gravatar Hugo Herbelin2017-10-22
| | | | | | | | | | | - Removing tag "found" (unused since bd18c0821 "Now CoqIDE has a nice find & replace mechanism"). - Removing setting the priority of the debugging tag edit_zone: it was set at exactly the level it would have been by default minus 1, which is the level of tooltip, which have no associated visible markers, so the setting was a priori w/o effect. - For clarity, reorganizing order of tags into ephemere ones and non ephemere ones.
* An attempt to fix issue #5771 (error color hidden by warning color).Gravatar Hugo Herbelin2017-10-22
| | | | | | | | | | | | | | | We change the relative priority of errors and warnings, so that the error takes precedence. It is unsure that it is universally the best choice. If the location of the error is finer than the one of the warning, it is better. In the other way round, it might be less good, e.g. if understanding the warning helps to understand the error. Maybe the best policy would be to test the relative locations of the warning and error? Trying to consider the error as more important, at the current time.
* Remove GeoProof support.Gravatar Maxime Dénès2017-10-11
| | | | | Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
* [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
| | | | | | | | | | | | | | We make the Stm API functional over an opaque `doc` type. This allows to have a much better picture of what the toplevel is doing; now almost all users of STM private data are marked by typing. For now only, the API is functional; a PR switching the internals should come soon thou; however we must first fix some initialization bugs. Due to some users, we modify `feedback` internally to include a "document id" field; we don't expose this change in the IDE protocol yet.
* [ide] Avoid duplicate error printing (BZ#5583)Gravatar Emilio Jesus Gallego Arias2017-09-29
| | | | | | | | | | | See the discussion in the bug tracker, basically the STM delays the feedback error message to a point where CoqIDE has forgotten about the sentence, thus we were processing such errors in the generic case, printing them twice as the Fail case will also do it. We could indeed revert back to the 8.6 strategy for error (print always from Fail and ignore Feedback), however I feel that time will be better spent by fixing the STM than adding more CoqIDE workarounds.