aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
2011-04-21Coqide: quote coqtop filename if necessaryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14045 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Coqide: a special kill function for win32letouzey
This is implemented as a C external launching the TerminateProcess of the Win32 API. This should be considered as quite experimental (cf. the way we handle pid in the comment of ide_win32_stubs.c). I don't know how to emulate an interrupt (Ctrl-C), for now the two button "Restart" and "Interrupt" have the same semantics on win32 (kill the subprocess and start at top). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14044 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Coqide: try to avoid displaying error messages on coqide's consoleletouzey
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
2011-04-21Coqide: better construction of default coqtop pathletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14042 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Win32: remove the need for Coq.bat and Coqide.batletouzey
This is an adaptation of commit r13750 of branch 8.3 - coqlib is currently computed relatively of Sys.executable_name, hence no need to set it manually - in Win32, better detection of user home dir : in System.ml, if HOME isn't set, we look now for HOMEDRIVE\HOMEPATH, and then for USERPROFILE - concerning PATH, in Win32 we now add coqbin (or the location of coqide) to PATH during the initialization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14041 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be ↵letouzey
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
2011-04-21Win32: let's directly make coqtop.exe and coqide.exe incorporate coq.icoletouzey
This is an adaptation of commit 13747 for 8.3 branch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14038 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-20Coqide: Fix the command separator for external cmds (#2363)letouzey
We use "&&" instead of ";" which is - compatible with unix and win32 - more adequate anyway than ";" : no need to run the command if the cd has failed... Concerning coqdoc, since previous commit it should not be mandatory to provide the "--coqlib-path" option. We remove them... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14036 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08More up to date About in coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13975 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Macos integration step2 : shutdownpboutill
You can quit coqide from the dock and reboot/shutdown will ask you if you want to save your unsavec files. Asks for a re"configure". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13974 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08coqide shutdown process change (and out the main function)pboutill
It now checks for 5 sec every 0.1 sec if is there is still running coqtop then it asks the user if he wants to leave zombies or cancel quit. (Cancel quit was continue to wait). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13973 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
This is useful, for example, in declaring the projection of the dependent record bundled form of an unbundled typeclass. Patch submitted by Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13956 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Coqide: avoid confusion of process when restarting coqtop + cosmeticletouzey
When using "Goto start" while many phrases are evaluated, it's frequent with earlier code that the restart occurs between two phrases, and hence the second is sent to the new coqtop, triggering things like "Anomaly: NoCurrentProof". To avoid that, Coq.coqtop is now immutable (no silent switch of channels). In Coqide, toplvl and mycoqtop are now references, that are updated when using reset_coqtop. We organize things in order to have only one access to mycoqtop during code that does many sequential calls to coqtop. This way, when coqtop changes, the code speaks to the old one, and gets some exception when writing/reading on a close channel. By the way, some documentation, cleanup, etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13942 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Ide_intf: remove useless int answer to the "interp" and "rewind" callsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13940 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Ide_slave: better handling of Ctrl-Cletouzey
- During input and output to coqide, we postpone Ctrl-C instead of ignoring them. For that we use Util.interrupt and Util.check_for_interrupt. - During evaluation of coqide requests, a Ctrl-C directly raises Sys.break, which is more reliable than waiting for the next Util.check_for_interrupt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13939 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Coqide: synchronise the reset_initial via the coq_computing mutexletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13938 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide: misc (nicer message than End_of_file, a useless try removedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13935 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsletouzey
* Run "coqide -coqtop someothercoqtop" if you want to use a toplevel which isn't the one coming alongside coqide. To be documented, to be improved (maybe an field in coqide's preferences ?). coqide -h should display this kind of ide-specific option. * Since we now use create_process instead of open_process, we don't use /bin/sh, hence running Filename.quote on args was actually wrong. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13932 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-25ide/coqide.ml: a pass of more decent automatic indentationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13931 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-25Ide: more reorganisation and cleanupletouzey
- 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
2011-03-25Ide_intf : change type of location in ideletouzey
We use (int * int) option instead of Loc.t, it's easier to use later in coqide, and this way we do not depend on camlp4,5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13929 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-25Ide: mention "Restart" instead of "Go to start" for corresponding buttonletouzey
This way probably emphasizes more the fact that the coqtop subprocess is killed and a new one is spawned. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13928 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-23Ide: stronger separation from coqtopletouzey
Former module Ide_blob is now divided in Ide_intf (linked both by coqtop and coqide) and Ide_slave (now only in coqtop). Ide_intf has almost no dependencies, we can now compile coqide with only coq_config.cm* and lib.cm(x)a TODO: - Devise a better way to display whether coqide is byte or opt in the about message (instead of Mltop.is_native, I display now the executable name, which hopefully contains opt or byte) - Check the late error handling in ide/coq.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-23Ide: experimentally allow coqide to interrupt or kill coqtopletouzey
- We now use create_process instead of open_process, and stores the answered pid. - The "Stop" button now sends a Sigint signal to this coqtop pid. - The "Goto Start" button now works even if a computation is ongoing, a new process is spawned and the previous one is killed -9, and then a waitpid is done to avoid having zombies around. Note that currently a vm_compute won't be stopped by a "Stop", but only by a "Goto Start". This can be quite confusing. How to properly document that "Goto Start" has the side effect of being a kill ? Maybe we could check someday if the Ctrl-C has been successful, and kill -9 if not ? Or maybe make coqide aware of a flag "we_are_vm_computing" and then kill -9 instead of Ctrl-C in this case ? TODO: - for the moment a forced "Goto Start" displays an unfriendly anomaly - check if all this works under Windows (probably but not sure). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13926 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Remove references to -ide option of coqmktopglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13789 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07MacOS integrationpboutill
if `pkg-config --exists ige-mac-integration`, coqide.opt will be able to open files by double-clik in finder on Darwin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13779 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Separate load_file handler in coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13778 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Coqide is not built with coqmktop any morepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13777 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Call coqtop with -nois when probing for filespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13775 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Fix print in coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13774 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-06Reverted r13715 "Add improved indenters that rely on the current proof state ↵gmelquio
to choose the indentation depth." It seems to be the cause for bug #2472. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13766 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-06Remove Safe_marshalglondu
Safe_marshal was using intermediate strings that are subject to Sys.max_string_length limitation. Use directly binary channel-oriented functions instead. This is a fix for bug #2471. Remark: this might reduce robustness w.r.t. noise in the communication channel. AFAIK, the original purpose of Safe_marshal was to work around a bug on Windows... this should be investigated further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13765 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-14Add improved indenters that rely on the current proof state to choose the ↵gmelquio
indentation depth. Patch by Cedric Auger. These two indenters need to be exercised a bit to see if they are actually useful to users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13715 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-14Add navigation items for quickly moving between word occurrences.gmelquio
Patch by Cedric Auger. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13714 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-14Improved the search/replace dialog box:gmelquio
+-----------------------------------+ | Find: ************** [Find again] | | Replace With: ****** [Repl.&Find] | | [?] Search backward [ Close ] | +-----------------------------------+ Ctrl+b (un)checks "Search backward", Return searches again, Ctrl+r replaces and searches again, Esc close the dialog box. Patch by Cedric Auger. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13713 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-14Fix mutex being released from a different thread than it is acquired from.gmelquio
Needed for FreeBSD. Patch by Cedric Auger. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13712 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-13Avoid silent loss of data when closing an unsaved buffer.gmelquio
Patch by David Baelde. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13707 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-04Made new comm. model between coq and coqide support '-R foo ""'-style option.herbelin
This fixes bug #2442. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13683 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-07Improved error messages in CoqIDE:herbelin
- add a check that coqtop can be run before starting the interface - returns the error message in case of problem - made illegal option message more informative - use coqtop.byte when coqide.byte (is it a good heuristic?) - made debugging messages silent by default in ide/undo.ml (Ctrl-C was calling Pervasives.prerr_endline instead of Ideutils.prerr_endline) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13627 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-04End of commit 13600: files can be given as arguments of coqide again.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13622 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-31Remove some unnecessary (?) "open Ideutils"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13589 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-31Remove (unused) ide/highlight.mllglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13588 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-07TeX input method is now supported upstreamvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-06Remove ide/coq_tactics.ml*glondu
Unused and refers to pre-v8 tactics. Basically untouched since 2003. Most likely obsolete. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13507 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-19Addressing part 2 of bug report 2377 (removing intrusive warning whenherbelin
coqide doc link is the canonical link to last released version of reference manual instead of link to corresponding coqide version). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13436 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-14CoqIDE argv parsing delegated to coqtopvgross
Introduces some hacks to have a consistent user experience. When coqtop prints info on self then exit, return code is 2 if called with -filteropts, 0 else For now, no options are accepted by coqide. there is no way for now to specify a filename that begins with a dash. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
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
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-12coqide: s/Sys.argv.(0)/Sys.executable_name/ for coqtop (cf #2341)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13277 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 00:09:58 +0000