| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14637 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14618 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14617 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14590 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14589 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
I assume that once Coq is installed in non-local mode and run from its
installed path, sources are no longer available. The coqsrc variable
doesn't make any sense, then, and its intended value can always be
inferred from Sys.executable_name. Moving it to Envars.coqroot.
Make coqlib optional. Currently, it is set to None only in -local mode
or with ocamlbuild. When set to None, -local layout is assumed
(binaries in ./bin, library in .). The behaviour should not be changed
when an explicit coqlib has been given to ./configure.
This commit should make it possible to run a Coq compiled with -local
from anywhere (no hard-coded absolute path embedded in the
executables, intermediary step to bug #2565). It WILL BREAK settings
re-using source trees after installation in non-local mode (are there
actual use cases for that?).
Hard-coded absolute paths still remain:
- in the build system, so the need to re-run ./configure after moving
the source tree is still expected for now;
- in coqrunbyteflags, I think we are limited by ocaml itself;
- docdir.
All absolute paths should be removed, ultimately.
As a side-effect, simplify computing of Envars.coqbin. I don't see any
good reason to keep it as a function.
Disclaimers:
- initialization of Sys.executable_name is not consistent across all
architectures; relying so much on it might trigger bugs. I'm pretty
sure something will explode if one adds arbitrary symlinks on top of
that;
- ocamlbuild stuff not tested.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14458 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This approach, inspired by ProofGeneral, is *much* simplier than earlier,
and should be more robust (I hope! feedback of testers is welcome).
Coqide still continues to send orders like "Rewind 5" for undoing 5 phrases.
A stack on the coqtop side (in Ide_slave) convert this phrase count to
labels in the sense of Backtrack, and to abort + depth informations
concerning proofs.
We avoid re-entering finished proofs during Rewind by some extra backtracking
until before these proofs. The amount of extra backtracking is then answered
by coqtop to coqide. Now:
- for go_to_insert (the "goto" button), unlike PG, coqide replays
the extra backtracked zone.
- for undo_last_step (the "back" button), coqide now leaves the extra
backtracked zone undone, just like PG. This happens typically when
undoing a Qed, and this should be the only visible semantical change
of this patch.
Two points to check with Pierre C:
- such a coqtop-side stack mapping labels to opened proofs might be
interesting to PG, instead of passing lots of info via the prompt and
computing stuff in emacs.
- Unlike PG, we allow re-entering inside a module / section, while
PG retracts to the start of it. Coqide seems to work fine this way, to
check.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14455 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- merge raw_interp with interp (with one more flag)
- merge read_stdout with interp, which now return a string
- shorter command names
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14454 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Files in a -I path are now installed in every root directory of -R pathes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14445 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14444 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14442 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14439 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14438 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14437 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14436 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14435 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14433 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- The make_cases function was duplicated in two files
- Rather use next_name_away_in_cases_pattern instead of ..._in_goal
when finding fresh pattern variables
- Nicer final pretty-print via some formatting boxes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14414 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In particular, grouping { and } delimiters is now allowed.
The only place where blank (i.e. space or newline or eof) is mandatory
is after dots. For instance "{{tac. }{tac. }}" is ok, while
"tac.}" is not seen as containing any sentence delimiter but rather
the inner-sentence token ".}", that might have been registered (or not)
to Coq by the user via some tactic or constr notation.
This way, coqide should be in sync with what is accepted by coqtop.
Current cvs version of proofgeneral is slightly more laxist, but
this will probably be harmonized soon.
Technically, we cannot rely anymore on functions like
forward_to_tag_toggle, since two delimiters "}}" could be adjacent,
hence no toogle of the corresponding tag. Instead, we use a simplier
(less efficient ?) iterative search.
When retagging a zone after some edition, we retag up to a real "."
delimiter (or eof), since the status of "{" "}" as delimiters is
too fragile to be trusted after edition.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14394 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
GEdit.combo_box_entry_text
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14306 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trying to have a direct rule for "..." seemed to be less hack-ish,
but is in fact _wrong_, shame on me : it's important to have a rule
for ".." since this can appear in a coq sentence (for instance in
recursive notations), and hence we don't want the second dot to be
considered as a terminator. So let's restore the previous situation,
with a rule for ".." (ignoring them) and a rule for "."+blank.
Then "..." is recognized as ".." + ".", which is quite ok after all.
The fact that ".. ." is also recognized by coqide in a similar way
isn't actually a problem: after reading this sentence, coqide
will send it to coqtop, and it's coqtop that will tell that this
sentence makes no sense...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14300 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- New terminators { and } are now accepted only when followed
by a blank or newline.
- reorganisation of coq_lex.mll : in particular stop adding
a fake " " when parsing a string.
- fix the handling of copy-pasted string containing tags :
we isolate this zone, untag it, and retag it properly.
For that we don't monitor the "changed" event anymore,
but wait for a "end_user_input" instead.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14294 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
that forces a given type to always be printed as a record, or with a
constructor, regardless of the setting of 'Printing Records'.
And this is that patch that controls printing by type.
(patch from Tom Prince)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
If a comment is a sentence not sent to coq, undoing a comment mustn't
undo anything !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14273 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14268 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
It doesn't use them for indenting.
Worst, the undo around "End ..." bug leaks on '}' !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14267 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Not perfect, font of unactives command panels won't change on the fly. (As it is for others GtextArea.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14213 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
We can be easily substitute Gdk.Windowing by a glance of configure work...
This reverts commit 8b6f6b1c4b60e74dccd5d8c49bdd433e19d53bf4.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14208 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Because of lablgtk issues, accel_maps can't be customized well on MacOS
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
You'll need to remove/edit your ~/.coqiderc and ~/.coqide.keys.
As it used to be, accelerator modifiers changes are only done after a
reboot but we need more binding in lablgtk to improve that...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14178 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14136 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14083 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We use GenerateConsoleCtrlEvent(CTRL_C_EVENT,...) after having
attached coqide to the console of the coqtop we want to interrupt.
Two caveats:
- This code isn't compatible with Windows < XP SP1.
- It relies on the fact that coqide is now a true GUI app, without
console by default. If for some reason the console of coqide is
restored (for instance via mkwinapp -unset), strange behavior
of the interrupt button is to be expected, at the very least all
instances of coqtop will get Ctrl-C instead of a precise one.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14077 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14065 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14052 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14051 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14050 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
The force_reset_initial starts by killing coqtop, then it tries
to acquire the lock on coq_computing. If it works, no jobs are
pending, we do the real reset_initial (launch of a new coqtop +
removal of buffer coloring) ourself.
Otherwise, the function do_if_not_computing is running, the death
of coqtop will raise a RestartCoqtop exception there, triggering
a reset_initial.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14048 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Now that coqide is a console-free win32 app, writing to
nonexistent stdout/stderr lead to Sys_error. To avoid that:
- We reroute coqide's stdout/stderr to either a pipe that will stay
unread (by default), or to a temp log file (in debug mode).
- When doing create_process, avoid referring to Unix.stderr:
anything printed by coqtop to its stderr will be merged in the
regular channel.
- On the coqtop side, remove the awkward fix consisting in a \r printed
on stderr apparently to fix coqide.byte. This fix is probably obsolete
since the separation of coqide and coqtop as distinct processes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14047 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14046 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14045 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14042 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|