aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
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
2010-07-05Fix goal display when backtrackingvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13246 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Robustness fix : clean restart of coqtop on pipe error + force matchingvgross
of coqtop return codes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13245 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-05Stronger checks on coqtop termination, warning when zombies.vgross
Also, reindentation + typed_notebook simplification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13241 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Fixing tabs closing problems by removing activation infrastructure.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13238 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22fix bug #2318, parsing error on dos line endingsvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13177 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-10Fix build with OCaml 3.12glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13107 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-07fixing error message display.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13082 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-01added -args option to coqide to pass options to coqtopsvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13046 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31CoqIDE goes multiprocessvgross
This commit changes many things in CoqIDE, and several breakage are to be expected. So far, evaluation in standard tactic mode and backtracking seems to be working. Future work : - clean up the thread management crud remaining in ide/coqide.ml - rework the exception handling - rework the init system in Coqtop plus many other things git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13043 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31More indirection.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13042 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31Introducing strong typing for IDE - toplevel IPCvgross
Obj.magic in toplevel/ide_blob.ml is the only way to simulate GADT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13041 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31deporting Coq specific code from ide to toplevel.vgross
Still messy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31Modifying startup sequencevgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13039 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-07Fix bug #2315 : printing of defined evars in Coqide.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13003 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-05Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proofpboutill
- ide doesn't crash anymore at any backtrack - I don't see if vernacentries.ml did the same assumption so I didn't change anything. (The only other use of resume_proof) - ide still raises "NoCurrentProof" when you type a bad keyword such as "Priint"... But at least, this on is catch somewhere ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12993 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-04 - Fixing bug #2308 about Lemma ... withvsiles
- Fixing a wierd behaviour of the goal window (scroll_at_iter doesn't work) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12991 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 08:10:16 +0000