aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ideutils.ml
Commit message (Collapse)AuthorAge
...
* Coqide: some more refactoring to lighten coqide.mlGravatar letouzey2012-12-10
| | | | | | | | | | | | | | | | | | | Main victim is analyzed_view : - some unnecessary methods have been killed (hep_for_keyword for instance) - some other migrated elsewhere (recenter_input, find_next_occurrence, ...) - analyzed_view is now split in two : fileops (filename, save, revert, ...) and coqops (process_next_phrase, ...) Four new files created: - Sentence (for tag_on_insert and alii) - FileOps (ex-first-half of analyzed_view) - CoqOps (ex-second-half of analyzed_view) - Session (ex-record viewable_script and functions about it) Also lots of renaming, trying to be shorter (but still meaningful) and more uniform git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: get rid of threads, use gtk asynchronous i/o insteadGravatar letouzey2012-12-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Threads were only there to handle blocking dialogs with the different coqtops. But programming with threads have drawbacks : complex mutex infrastructure, possible deadlocks, etc. In particular gtk functions are not meant to be called from a thread which isn't the gtk main loop, (unless some gtk mutex have been taken). This seem to pose problem specifically in win32 (and macosx ?), hence the use of the GtkThread.(a)sync hack for scheduling code for execution in the gtk main loop. Instead, we now use the Glib.Io module to install a callback that will be runned when some answer of coqtop is available on the channel. This implies using now a continuation-passing style: for instance, instead of two sequential requests to coqtop, we'll now have the 2nd request inside the callback handling the answer to the 1st request. Remarks: - Also use asynchronous i/o for external commands (editor, coqc, make...). Launching an external editor or browser won't freeze coqide anymore. - Reworked handling of coqtop process, especially when closing them. A responsive coqtop should now hara-kiri immediatly when its input channel is closed. Otherwise we try later a soft kill, then some hard kills if necessary. If nothing work we warns the user. When quitting coqide, all this might induce a small delay (2s at worse). - Be careful now to avoid "long" computations (or blocking i/o) in a coqide function. Experimentally, it seems that loading/saving a .v file is quick enough. If necessary, we could use asynchronous i/o also for writing the .v, but for loading I've no clue. - In the Coqide module, we ensure that the current continuation k will indeed be run at the end thanks to an abstract return type (void = opaque copy of unit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: more cleanup (buffers)Gravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer code around Coq_lexGravatar letouzey2012-12-07
| | | | | | | | | | | Instead of many Coq_lex.delimit_sentence followed by String.sub, we let Coq_lex find the different sentences at once. The offset converter (from byte offset to utf8 offset) is optimized to compute these offsets incrementally instead of re-visiting the whole string buffer again and again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16043 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ideutils: simpler conversion from byte offset to utf8 char offsetGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: opening non-existing files won't create them immediately anymoreGravatar letouzey2012-12-07
| | | | | | ... and many more code cleanup concerning file loading git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: nicer creation of timersGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: code cleanupGravatar letouzey2012-12-07
| | | | | | | | | | | | - indentation, wrap long lines - factorize some code - split Coqide.main in many subfunctions - Put the callbacks in modules (e.g. File.load) - ... Normally this commit shouldn't change coqtop behavior git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRSGravatar pboutill2012-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now CoqIDE separates answer and messages. This should hopefullyGravatar ppedrot2012-06-29
| | | | | | be backward compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now CoqIDE auto-sets the printing width of the goal display.Gravatar ppedrot2012-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15494 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned prerr_endline use.Gravatar ppedrot2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert copy/pasted function in to minilib thanks to clib.cmaGravatar pboutill2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert commit 15287 : the env variables are indeed access at launch-timeGravatar letouzey2012-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: in win32 command given to cmd.exe should be more quotedGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed access to environment variables in CoqIDE. Up to now, thoseGravatar ppedrot2012-05-08
| | | | | | variables where set at compile time... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15287 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed the useless use of a reference in preference handling.Gravatar ppedrot2012-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15271 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: the coqtop to launch is a preference.Gravatar pboutill2012-04-17
| | | | | | | If it is AUTO then we keep the heuristic to change coqide by coqtop in Sys.executable_name. If it fails coqtop location must be given by the users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide input encoding preference is an algebraic type.Gravatar pboutill2012-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15174 85f007b7-540e-0410-9357-904b9bb8a0f7
* Browser documentation & CharSet under WindowsGravatar pboutill2012-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIde files position is freedesktop compliant.Gravatar pboutill2011-12-18
| | | | | | | Beware, it means that files position is not relative to coqtop position but is given by XDG_DATA_DIRS and XDG_CONFIG_DIRS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14822 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide -debug only printed Coqtop information.Gravatar pboutill2011-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile : bug when a project file is not in the current directory.Gravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14443 85f007b7-540e-0410-9357-904b9bb8a0f7
* safe_prerr_endline in MinilibGravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add option -f to coqideGravatar pboutill2011-09-01
| | | | | | to specify where to look the project file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14441 85f007b7-540e-0410-9357-904b9bb8a0f7
* same_file in MinilibGravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attempt to use more local doc in coqideGravatar pboutill2011-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: try to avoid displaying error messages on coqide's consoleGravatar letouzey2011-04-21
| | | | | | | | | In Win32, these messages may trigger some Sys_error if we try to turn coqide into a true windows app (no console). To be continued... The best way would be probably to re-route the whole stdout and stderr to something else via dup2, but to what ? A log file ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14043 85f007b7-540e-0410-9357-904b9bb8a0f7
* Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be ↵Gravatar letouzey2011-04-21
| | | | | | | | | | | | | | | | | | | | | | used This is an adaptation of commit r13751 of branch 8.3 Even if coqide.exe keeps its console by default for the moment, we try to allow turning it off (for instance via the mkwinapp tool) : for that we need to be cautious about the use of functions like prerr_endline. Since stderr doesn't exists in this settings, such functions trigger a Sys_error "bad file descriptor". This patch protects many access to std** by a (try ... with _ ->()). Nota: with camlp5 < 6.02.1, Print Grammar was also generating such a Sys_error. TODO: we should try to figure a way of displaying messages (both debug and early/late error message). A log file ? A popup ? diplay in the response buffer ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: more reorganisation and cleanupGravatar letouzey2011-03-25
| | | | | | | | | | | | | | | | | | | - Avoid using Util which depends on Compat and hence Camlp4 - Instead, a small Minilib module specific to coqide, which duplicate 5 functions from Util (50 lines) - some dead code removal - the coqlib variable is asked to coqtop - remove obsolete Util.check_for_interrupt This way, coqide only depends on 3 files outside ide/ : Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted accordingly. TODO: how should we signal coqide error, warnings, etc ? For the moment, some Printf.eprintf, some failwith. To uniformize later... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
| | | | | | See http://caml.inria.fr/mantis/view.php?id=4940 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
| | | | | | Still messy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tried to make F1 documentation tool working in CoqIDE.Gravatar herbelin2009-08-14
| | | | | | | | | | | | | | | | | | | | | | | In trunk: New strategy for compiling and finding index_url.txt. After all, this file is not specific to CoqIDE but to the documentation. Hence, it seems better to install it close to the documentation. If the documentation is locally installed, it is easy to find the file index_url.txt but what to do if the documentation is remote? We would need a http getter. Does this mean we have to rely on wget or so? In the absence of answer to this question, it seems reasonable, first to assume the doc to be locally installed, second to have a local copy of index_url.txt ready in the installation directory of CoqIDE. Also added an "automatic" field in the CoqIDE url preference to prevent the user to have to update his preference file every time a new version of Coq is out and the link to the doc change. In 8.2: Added a minima the installation of index_urls.txt but the user will have to update its preferences because the links "http://coq.inria.fr/doc/Reference-Manual010.html#..." do not longer exist. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12278 85f007b7-540e-0410-9357-904b9bb8a0f7
* - per session coq command stackGravatar vgross2009-03-07
| | | | | | | | | | | - removed circular dependency between record and class used to keep track of sessions => no need for mutable option in record. - more 'a option ref pruning - more code splitting - more alpha-rewriting git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
* open and save buttons are the defaultGravatar barras2008-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11093 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"Gravatar herbelin2008-05-30
| | | | | | | | | | n'étaient pas gérés, merci à Julien). - Correction pb blocage CoqIDE quand le browser n'est pas déja lancé (utilisation pour cela de Sys.command au lieu de Unix.open_process_full). - MAJ CHANGES et COMPATIBILITY. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11022 85f007b7-540e-0410-9357-904b9bb8a0f7
* backtrack sur utilisation de do_overwrite_confirmationGravatar jnarboux2008-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11020 85f007b7-540e-0410-9357-904b9bb8a0f7
* commented out overwrite confirmation handler (requires lablgtk >=2.10)Gravatar barras2008-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11019 85f007b7-540e-0410-9357-904b9bb8a0f7
* add support for pdf in coqdoc, add export to pdf in coqide, port open and ↵Gravatar jnarboux2008-05-28
| | | | | | save as dialogs of coqide to a not deprecated widget, add filtering of *.v files in these dialogs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11006 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1842 + correction bug initialisation introduit dansGravatar herbelin2008-05-10
| | | | | | | commit 10916 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration de la colorisation, du backtrack et des messages de CoqIDEGravatar herbelin2008-05-10
| | | | | | | | | | | | | | | | | | | - Colorisation: - on ne colorie que les noms de commandes que si en début de phrase (par exemple: Definition F := fun Local => Local) ne colorie pas Local), - ajout de motifs plus sophistiqué, (par exemple, tous les Set/Unset sont uniformément mis en valeur). - Backtracking: résolution bug #1538 et réactivation de la possibilité de déclarer des défs, types, etc pendant une session de preuve. En revanche, il n'est pas clair que cela fonctionne bien avec le mode déclaratif. - Messages d'erreur : on ne capture la sortie de coq qu'après l'initialisation pour que les erreurs d'initialisation soit affichées (cf bug #1424 and item 5 of #1123). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10915 85f007b7-540e-0410-9357-904b9bb8a0f7
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Suppression d'une source de fuite mémoire dans declare_mod.ml (la table de hash library_table n'était pas synchronisée avec le reset et elle grossissait à chaque rejeu de la session; utilisation au passage d'une map pour que la synchronisation avec le reset soit plus rapide). [mod_typing.ml] - Correction d'un bug de synchronisation pour le niveau pattern 200. [pcoq.ml4] - Suppression d'un vieux reste du traducteur [constructeur VernacVar] - Robustesse et uniformité accrue dans CoqIDE vis à vis du statut de chacune des commandes vernaculaires par l'utilisation d'une fonction d'assignation d'attributs à chaque commande vernac. Correction de ce qui semble être des bizarreries (VernacDeclareTacticDefinition considéré comme ouvrant un but; suppression des "loc" dans les Reset: ne pouvait pas faire fonctionner correctement update_on_end_of_segment). Suppression de la nécessité d'expliciter si une commande retourne des messages dépendants du mode "verbose" (on suppose que chaque commande sait ce qu'elle doit dire selon la position du flag verbose). Sinon, le mécanisme de Reset de CoqIDE reste pauvre. CoqIDE ne sait revenir qu'aux états associés à des noms et cela ne vaut pas l'approche de Proof General. Il sera sans doute opportun de se brancher sur l'architecture de Pierre Courtieu à base de "Backtrack". La restriction des buts imbriqués a-t-elle vraiment une raison d'être ? En plus les commandes non cablées en dur comme Next Obligation ne sont pas prises en compte. Interdiction, dès Coq, d'ouvrir sections ou modules si preuve en cours. Réparation approximative de l'option "Help for Keyword" de Coqide mais encore à faire pour plus de robustesse (makefile, installation, synchronisation entre la version du fichier index_urls.txt et la version du refman, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10904 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* redirection of errors in coqide + dynamic warning printer (needed for tm_egg)Gravatar corbinea2007-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 18:41:55 +0000