From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- ide/.merlin | 6 + ide/FAQ | 25 +- ide/MacOS/Info.plist.template | 89 + ide/MacOS/coqfile.icns | Bin 0 -> 234599 bytes ide/MacOS/coqide.icns | Bin 0 -> 326632 bytes ide/MacOS/default_accel_map | 378 +++ ide/MacOS/relatify_with-respect-to_.sh | 15 + ide/Make | 6 + ide/command_windows.ml | 158 -- ide/command_windows.mli | 16 - ide/config_lexer.mll | 9 +- ide/coq-ssreflect.lang | 246 ++ ide/coq.lang | 216 ++ ide/coq.ml | 462 +++- ide/coq.mli | 195 +- ide/coq.png | Bin 6269 -> 71924 bytes ide/coqOps.ml | 824 +++++++ ide/coqOps.mli | 43 + ide/coq_commands.ml | 6 +- ide/coq_lex.mll | 174 +- ide/coq_style.xml | 26 + ide/coqide-gtk2rc | 39 - ide/coqide.ml | 4100 ++++++++++---------------------- ide/coqide.mli | 14 +- ide/coqide_main.ml4 | 169 +- ide/coqide_ui.ml | 28 +- ide/coqidetop.mllib | 2 + ide/document.ml | 186 ++ ide/document.mli | 115 + ide/fileOps.ml | 154 ++ ide/fileOps.mli | 23 + ide/gtk_parsing.ml | 33 +- ide/ide.mllib | 22 +- ide/ide_slave.ml | 505 ++++ ide/ide_win32_stubs.c | 44 +- ide/ideproof.ml | 147 -- ide/ideutils.ml | 541 +++-- ide/ideutils.mli | 91 +- ide/interface.mli | 242 ++ ide/mac_default_accel_map | 376 --- ide/macos_prehook.ml | 37 + ide/minilib.ml | 218 +- ide/minilib.mli | 44 +- ide/nanoPG.ml | 321 +++ ide/preferences.ml | 389 ++- ide/preferences.mli | 30 +- ide/project_file.ml4 | 102 +- ide/sentence.ml | 126 + ide/sentence.mli | 19 + ide/session.ml | 517 ++++ ide/session.mli | 50 + ide/tags.ml | 50 +- ide/tags.mli | 23 +- ide/typed_notebook.ml | 67 - ide/undo.ml | 175 -- ide/undo_lablgtk_ge212.mli | 35 - ide/undo_lablgtk_ge26.mli | 33 - ide/undo_lablgtk_lt26.mli | 33 - ide/utf8_convert.mll | 2 +- ide/utils/config_file.ml | 4 +- ide/utils/config_file.mli | 4 +- ide/utils/configwin_ihm.ml | 14 +- ide/utils/configwin_messages.ml | 2 +- ide/utils/configwin_types.ml | 6 +- ide/utils/editable_cells.ml | 1 - ide/utils/okey.ml | 2 +- ide/wg_Command.ml | 166 ++ ide/wg_Command.mli | 18 + ide/wg_Completion.ml | 453 ++++ ide/wg_Completion.mli | 34 + ide/wg_Detachable.ml | 89 + ide/wg_Detachable.mli | 42 + ide/wg_Find.ml | 199 ++ ide/wg_Find.mli | 18 + ide/wg_MessageView.ml | 63 + ide/wg_MessageView.mli | 22 + ide/wg_Notebook.ml | 67 + ide/wg_Notebook.mli | 38 + ide/wg_ProofView.ml | 202 ++ ide/wg_ProofView.mli | 19 + ide/wg_ScriptView.ml | 467 ++++ ide/wg_ScriptView.mli | 54 + ide/wg_Segment.ml | 143 ++ ide/wg_Segment.mli | 21 + ide/xmlprotocol.ml | 737 ++++++ ide/xmlprotocol.mli | 58 + 86 files changed, 9921 insertions(+), 5018 deletions(-) create mode 100644 ide/.merlin create mode 100644 ide/MacOS/Info.plist.template create mode 100644 ide/MacOS/coqfile.icns create mode 100644 ide/MacOS/coqide.icns create mode 100644 ide/MacOS/default_accel_map create mode 100755 ide/MacOS/relatify_with-respect-to_.sh create mode 100644 ide/Make delete mode 100644 ide/command_windows.ml delete mode 100644 ide/command_windows.mli create mode 100644 ide/coq-ssreflect.lang create mode 100644 ide/coq.lang create mode 100644 ide/coqOps.ml create mode 100644 ide/coqOps.mli create mode 100644 ide/coq_style.xml delete mode 100644 ide/coqide-gtk2rc create mode 100644 ide/coqidetop.mllib create mode 100644 ide/document.ml create mode 100644 ide/document.mli create mode 100644 ide/fileOps.ml create mode 100644 ide/fileOps.mli create mode 100644 ide/ide_slave.ml delete mode 100644 ide/ideproof.ml create mode 100644 ide/interface.mli delete mode 100644 ide/mac_default_accel_map create mode 100644 ide/macos_prehook.ml create mode 100644 ide/nanoPG.ml create mode 100644 ide/sentence.ml create mode 100644 ide/sentence.mli create mode 100644 ide/session.ml create mode 100644 ide/session.mli delete mode 100644 ide/typed_notebook.ml delete mode 100644 ide/undo.ml delete mode 100644 ide/undo_lablgtk_ge212.mli delete mode 100644 ide/undo_lablgtk_ge26.mli delete mode 100644 ide/undo_lablgtk_lt26.mli create mode 100644 ide/wg_Command.ml create mode 100644 ide/wg_Command.mli create mode 100644 ide/wg_Completion.ml create mode 100644 ide/wg_Completion.mli create mode 100644 ide/wg_Detachable.ml create mode 100644 ide/wg_Detachable.mli create mode 100644 ide/wg_Find.ml create mode 100644 ide/wg_Find.mli create mode 100644 ide/wg_MessageView.ml create mode 100644 ide/wg_MessageView.mli create mode 100644 ide/wg_Notebook.ml create mode 100644 ide/wg_Notebook.mli create mode 100644 ide/wg_ProofView.ml create mode 100644 ide/wg_ProofView.mli create mode 100644 ide/wg_ScriptView.ml create mode 100644 ide/wg_ScriptView.mli create mode 100644 ide/wg_Segment.ml create mode 100644 ide/wg_Segment.mli create mode 100644 ide/xmlprotocol.ml create mode 100644 ide/xmlprotocol.mli (limited to 'ide') diff --git a/ide/.merlin b/ide/.merlin new file mode 100644 index 00000000..3f3d9d27 --- /dev/null +++ b/ide/.merlin @@ -0,0 +1,6 @@ +PKG lablgtk2.sourceview2 + +S utils +B utils + +REC diff --git a/ide/FAQ b/ide/FAQ index f07f229f..07b81824 100644 --- a/ide/FAQ +++ b/ide/FAQ @@ -6,8 +6,8 @@ R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more i Q1) How to enable Emacs keybindings? R1: Insert gtk-key-theme-name = "Emacs" - in your "coqide-gtk2rc" file. It should be in $XDG_CONFIG_DIRS/coq dir. - This is done by default. +in your gtkrc file. The location of this file is system-dependent. If you're running +Gnome, you may use the graphical configuration tools. Q2) How to enable antialiased fonts? R2) Set the GDK_USE_XFT variable to 1. This is by default with Gtk >= 2.2. @@ -34,27 +34,14 @@ R5)-First solution : type "2200" to enter a forall in the script 2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀" in UTF-8. 2203 is for exists. See http://www.unicode.org for more codes. --Second solution : rebind "a" to forall and "e" to exists. - Under X11, you need to use something like - xmodmap -e "keycode 24 = a A F13 F13" - xmodmap -e "keycode 26 = e E F14 F14" - and then to add - bind "F13" {"insert-at-cursor" ("∀")} - bind "F14" {"insert-at-cursor" ("∃")} - to your "binding "text"" section in coqiderc-gtk2rc. - The strange ("∀") argument is the UTF-8 encoding for - 0x2200. - You can compute these encodings using the lablgtk2 toplevel with - Glib.Utf8.from_unichar 0x2200;; - Further symbols can be bound on higher Fxx keys or on even on other keys you - do not need . +-Second solution : Use an input method editor, such as SCIM or iBus. The latter offers +a module for LaTeX-like inputting. Q6) How to customize the shortcuts for menus? R6) Two solutions are offered: - Edit $XDG_CONFIG_HOME/coq/coqide.keys by hand or - - Add "gtk-can-change-accels = 1" in your coqide-gtk2rc file. Then - from CoqIde, you may select a menu entry and press the desired - shortcut. + - If your system allows it, from CoqIde, you may select a menu entry and press the + desired shortcut. Q7) What encoding should I use? What is this \x{iiii} in my file? R7) The encoding option is related to the way files are saved. diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template new file mode 100644 index 00000000..fd80c839 --- /dev/null +++ b/ide/MacOS/Info.plist.template @@ -0,0 +1,89 @@ + + + + + CFBundleDocumentTypes + + + CFBundleTypeExtensions + + * + + CFBundleTypeName + NSStringPboardType + CFBundleTypeOSTypes + + **** + + CFBundleTypeRole + Editor + + + CFBundleTypeIconFile + coqfile.icns + CFBundleTypeName + Coq file + CFBundleTypeRole + Editor + CFBundleTypeMIMETypes + + text/plain + + CFBundleTypeExtensions + + v + + LSHandlerRank + Owner + + + CFBundleTypeName + All + CFBundleTypeRole + Editor + CFBundleTypeMIMETypes + + text/plain + + LSHandlerRank + Default + CFBundleTypeExtensions + + * + + + + CFBundleIconFile + coqide.icns + CFBundleVersion + 390 + CFBundleName + CoqIDE + CFBundleShortVersionString + VERSION + CFBundleDisplayName + Coq Proof Assistant vVERSION + CFBundleGetInfoString + Coq_vVERSION + NSHumanReadableCopyright + Copyright 1999-2014, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS + CFBundleHelpBookFolder + share/doc/coq/html/ + CFAppleHelpAnchor + index + CFBundleExecutable + coqide + CFBundlePackageType + APPL + CFBundleInfoDictionaryVersion + 6.0 + CFBundleIdentifier + fr.inria.coq.coqide + LSApplicationCategoryType + public.app-category.developer-tools + CFBundleDevelopmentRegion + English + NSPrincipalClass + NSApplication + + diff --git a/ide/MacOS/coqfile.icns b/ide/MacOS/coqfile.icns new file mode 100644 index 00000000..107e7043 Binary files /dev/null and b/ide/MacOS/coqfile.icns differ diff --git a/ide/MacOS/coqide.icns b/ide/MacOS/coqide.icns new file mode 100644 index 00000000..92bdfe77 Binary files /dev/null and b/ide/MacOS/coqide.icns differ diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map new file mode 100644 index 00000000..6f474eb1 --- /dev/null +++ b/ide/MacOS/default_accel_map @@ -0,0 +1,378 @@ +; coqide GtkAccelMap rc-file -*- scheme -*- +; this file is an automated accelerator map dump +; +; (gtk_accel_path "/Templates/Template Read Module" "") +; (gtk_accel_path "/Tactics/Tactic pattern" "") +(gtk_accel_path "/Templates/Definition" "d") +; (gtk_accel_path "/Templates/Template Program Lemma" "") +(gtk_accel_path "/Templates/Lemma" "l") +; (gtk_accel_path "/Templates/Template Fact" "") +(gtk_accel_path "/Tactics/auto" "a") +; (gtk_accel_path "/Tactics/Tactic fold" "") +; (gtk_accel_path "/Help/About Coq" "") +; (gtk_accel_path "/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "") +; (gtk_accel_path "/Templates/Template Hypothesis" "") +; (gtk_accel_path "/Tactics/Tactic repeat" "") +; (gtk_accel_path "/Templates/Template Unset Extraction Optimize" "") +; (gtk_accel_path "/Templates/Template Add Printing Constructor" "") +; (gtk_accel_path "/Windows/Detach View" "") +; (gtk_accel_path "/Tactics/Tactic inversion" "") +; (gtk_accel_path "/Templates/Template Write State" "") +; (gtk_accel_path "/Export/Export to" "") +(gtk_accel_path "/Tactics/auto with *" "asterisk") +; (gtk_accel_path "/Tactics/Tactic inversion--clear" "") +; (gtk_accel_path "/Templates/Template Implicit Arguments" "") +; (gtk_accel_path "/Edit/Copy" "c") +; (gtk_accel_path "/Tactics/Tactic inversion -- using" "") +; (gtk_accel_path "/View/Previous tab" "Left") +; (gtk_accel_path "/Tactics/Tactic change -- in" "") +; (gtk_accel_path "/Tactics/Tactic jp" "") +; (gtk_accel_path "/Tactics/Tactic red" "") +; (gtk_accel_path "/Templates/Template Coercion" "") +; (gtk_accel_path "/Templates/Template CoFixpoint" "") +; (gtk_accel_path "/Tactics/Tactic intros until" "") +; (gtk_accel_path "/Templates/Template Derive Dependent Inversion" "") +; (gtk_accel_path "/Tactics/Tactic eapply" "") +; (gtk_accel_path "/View/View" "") +; (gtk_accel_path "/Tactics/Tactic change" "") +; (gtk_accel_path "/Tactics/Tactic firstorder using" "") +; (gtk_accel_path "/Tactics/Tactic decompose sum" "") +; (gtk_accel_path "/Tactics/Tactic cut" "") +; (gtk_accel_path "/Templates/Template Remove Printing Let" "") +; (gtk_accel_path "/Templates/Template Structure" "") +; (gtk_accel_path "/Tactics/Tactic compute in" "") +; (gtk_accel_path "/Queries/Locate" "") +; (gtk_accel_path "/Templates/Template Save." "") +; (gtk_accel_path "/Templates/Template Canonical Structure" "") +; (gtk_accel_path "/Tactics/Tactic compare" "") +; (gtk_accel_path "/Templates/Template Next Obligation" "") +(gtk_accel_path "/View/Display notations" "n") +; (gtk_accel_path "/Tactics/Tactic fail" "") +; (gtk_accel_path "/Tactics/Tactic left" "") +(gtk_accel_path "/Edit/Undo" "u") +(gtk_accel_path "/Tactics/eauto with *" "ampersand") +; (gtk_accel_path "/Templates/Template Infix" "") +; (gtk_accel_path "/Tactics/Tactic functional induction" "") +; (gtk_accel_path "/Tactics/Tactic clear" "") +; (gtk_accel_path "/Templates/Template End Silent." "") +; (gtk_accel_path "/Tactics/Tactic intros" "") +; (gtk_accel_path "/Tactics/Tactic constructor -- with" "") +; (gtk_accel_path "/Tactics/Tactic destruct" "") +; (gtk_accel_path "/Tactics/Tactic intro after" "") +; (gtk_accel_path "/Tactics/Tactic abstract" "") +; (gtk_accel_path "/Compile/Compile buffer" "") +; (gtk_accel_path "/Queries/About" "F5") +; (gtk_accel_path "/Templates/Template CoInductive" "") +; (gtk_accel_path "/Templates/Template Test Printing Wildcard" "") +; (gtk_accel_path "/Templates/Template Unset Hyps--limit" "") +; (gtk_accel_path "/Templates/Template Transparent" "") +; (gtk_accel_path "/Export/Ps" "") +; (gtk_accel_path "/Tactics/Tactic elim" "") +; (gtk_accel_path "/Templates/Template Extract Constant" "") +; (gtk_accel_path "/Tactics/Tactic assert (--:--)" "") +; (gtk_accel_path "/Templates/Template Add Rec LoadPath" "") +; (gtk_accel_path "/Edit/Redo" "") +; (gtk_accel_path "/Tactics/Tactic compute" "") +; (gtk_accel_path "/Compile/Next error" "F7") +; (gtk_accel_path "/Templates/Template Add ML Path" "") +; (gtk_accel_path "/Templates/Template Test Printing If" "") +; (gtk_accel_path "/Templates/Template Load Verbose" "") +; (gtk_accel_path "/Templates/Template Reset Extraction Inline" "") +; (gtk_accel_path "/Templates/Template Set Implicit Arguments" "") +; (gtk_accel_path "/Templates/Template Test Printing Let" "") +; (gtk_accel_path "/Windows/Windows" "") +; (gtk_accel_path "/Templates/Template Defined." "") +(gtk_accel_path "/Templates/match" "c") +; (gtk_accel_path "/Tactics/Tactic set (--:=--)" "") +; (gtk_accel_path "/Templates/Template Proof." "") +; (gtk_accel_path "/Compile/Make" "F6") +; (gtk_accel_path "/Templates/Template Module Type" "") +; (gtk_accel_path "/Tactics/Tactic apply -- with" "") +; (gtk_accel_path "/File/Save as" "") +; (gtk_accel_path "/Templates/Template Set Hyps--limit" "") +; (gtk_accel_path "/Templates/Template Global Variable" "") +; (gtk_accel_path "/Templates/Template Remove Printing Constructor" "") +; (gtk_accel_path "/Templates/Template Add Setoid" "") +; (gtk_accel_path "/Edit/Find Next" "F3") +; (gtk_accel_path "/Edit/Find" "f") +; (gtk_accel_path "/Templates/Template Add Relation" "") +; (gtk_accel_path "/Queries/Print" "F4") +; (gtk_accel_path "/Templates/Template Obligations Tactic" "") +; (gtk_accel_path "/Tactics/Tactic trivial" "") +; (gtk_accel_path "/Tactics/Tactic first" "") +; (gtk_accel_path "/Tactics/Tactic case" "") +; (gtk_accel_path "/Templates/Template Hint Constructors" "") +; (gtk_accel_path "/Templates/Template Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T." "") +; (gtk_accel_path "/Templates/Template Coercion Local" "") +(gtk_accel_path "/View/Show Query Pane" "Escape") +; (gtk_accel_path "/Tactics/Tactic cbv" "") +; (gtk_accel_path "/Tactics/Tactic inversion--clear -- in" "") +; (gtk_accel_path "/Templates/Template Add Rec ML Path" "") +; (gtk_accel_path "/Tactics/Tactic apply" "") +; (gtk_accel_path "/Export/Latex" "") +; (gtk_accel_path "/Tactics/Tactic inversion -- using -- in" "") +; (gtk_accel_path "/Tactics/Tactic generalize" "") +(gtk_accel_path "/Navigation/Backward" "Up") +; (gtk_accel_path "/Tactics/Tactic p" "") +(gtk_accel_path "/Navigation/Hide" "h") +; (gtk_accel_path "/File/Close buffer" "w") +; (gtk_accel_path "/Tactics/Tactic induction" "") +; (gtk_accel_path "/Tactics/Tactic eauto with" "") +(gtk_accel_path "/View/Display raw matching expressions" "m") +; (gtk_accel_path "/Tactics/Tactic d" "") +; (gtk_accel_path "/Tactics/Tactic u" "") +; (gtk_accel_path "/Templates/Templates" "") +; (gtk_accel_path "/Tactics/Tactic s" "") +; (gtk_accel_path "/Tactics/Tactic lapply" "") +; (gtk_accel_path "/Tactics/Tactic t" "") +; (gtk_accel_path "/Tactics/Tactic r" "") +; (gtk_accel_path "/Edit/Replace" "r") +; (gtk_accel_path "/Tactics/Tactic case -- with" "") +; (gtk_accel_path "/Tactics/Tactic eexact" "") +; (gtk_accel_path "/Queries/Check" "F3") +; (gtk_accel_path "/Tactics/Tactic omega" "") +; (gtk_accel_path "/File/New" "n") +; (gtk_accel_path "/Tactics/Tactic l" "") +; (gtk_accel_path "/Tactics/Tactic intro" "") +; (gtk_accel_path "/Tactics/Tactic j" "") +; (gtk_accel_path "/Tactics/Tactic i" "") +; (gtk_accel_path "/Templates/Template Definition" "") +; (gtk_accel_path "/Tactics/Tactic g" "") +; (gtk_accel_path "/Tactics/Tactic f" "") +; (gtk_accel_path "/Tactics/Tactic e" "") +; (gtk_accel_path "/Tactics/Tactic c" "") +(gtk_accel_path "/File/Rehighlight" "l") +; (gtk_accel_path "/Tactics/Tactic simple inversion" "") +; (gtk_accel_path "/Tactics/Tactic a" "") +; (gtk_accel_path "/Templates/Template Mutual Inductive" "") +; (gtk_accel_path "/Templates/Template Extraction NoInline" "") +(gtk_accel_path "/Templates/Theorem" "t") +; (gtk_accel_path "/Templates/Template Derive Dependent Inversion--clear" "") +; (gtk_accel_path "/Tactics/Tactic unfold" "") +; (gtk_accel_path "/Tactics/Try Tactics" "") +; (gtk_accel_path "/Tactics/Tactic red in" "") +; (gtk_accel_path "/Tactics/Tactic rewrite <- -- in" "") +; (gtk_accel_path "/Templates/Template Hint Extern" "") +; (gtk_accel_path "/Templates/Template Unfocus" "") +; (gtk_accel_path "/Tactics/Tactic dependent inversion--clear" "") +; (gtk_accel_path "/Help/Browse Coq Library" "") +; (gtk_accel_path "/Tactics/Tactic lazy" "") +; (gtk_accel_path "/Templates/Template Scheme" "") +(gtk_accel_path "/Tactics/tauto" "p") +; (gtk_accel_path "/Tactics/Tactic cutrewrite" "") +; (gtk_accel_path "/Tactics/Tactic contradiction" "") +; (gtk_accel_path "/Templates/Template Set Printing Wildcard" "") +; (gtk_accel_path "/Templates/Template Add LoadPath" "") +(gtk_accel_path "/Navigation/Previous" "less") +; (gtk_accel_path "/Templates/Template Require" "") +; (gtk_accel_path "/Tactics/Tactic simpl" "") +; (gtk_accel_path "/Templates/Template Require Import" "") +; (gtk_accel_path "/Templates/Template Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T." "") +(gtk_accel_path "/Navigation/Forward" "Down") +; (gtk_accel_path "/Tactics/Tactic rename -- into" "") +; (gtk_accel_path "/Compile/Compile" "") +; (gtk_accel_path "/File/Save all" "") +; (gtk_accel_path "/Tactics/Tactic fix" "") +; (gtk_accel_path "/Templates/Template Parameter" "") +; (gtk_accel_path "/Tactics/Tactic assert" "") +; (gtk_accel_path "/Tactics/Tactic do" "") +; (gtk_accel_path "/Tactics/Tactic ring" "") +; (gtk_accel_path "/Export/Pdf" "") +; (gtk_accel_path "/Tactics/Tactic quote" "") +; (gtk_accel_path "/Tactics/Tactic symmetry in" "") +; (gtk_accel_path "/Help/Help" "") +(gtk_accel_path "/Templates/Inductive" "i") +; (gtk_accel_path "/Tactics/Tactic idtac" "") +; (gtk_accel_path "/Templates/Template Syntax" "") +; (gtk_accel_path "/Tactics/Tactic intro -- after" "") +; (gtk_accel_path "/Tactics/Tactic fold -- in" "") +; (gtk_accel_path "/Templates/Template Program Definition" "") +(gtk_accel_path "/Tactics/Wizard" "dollar") +; (gtk_accel_path "/Templates/Template Hint Resolve" "") +; (gtk_accel_path "/Templates/Template Set Extraction Optimize" "") +; (gtk_accel_path "/File/Revert all buffers" "") +; (gtk_accel_path "/Tactics/Tactic subst" "") +; (gtk_accel_path "/Tactics/Tactic autorewrite" "") +; (gtk_accel_path "/Tactics/Tactic pose" "") +; (gtk_accel_path "/Tactics/Tactic simplify--eq" "") +; (gtk_accel_path "/Tactics/Tactic clearbody" "") +; (gtk_accel_path "/Tactics/Tactic eauto" "") +; (gtk_accel_path "/Templates/Template Grammar" "") +; (gtk_accel_path "/Tactics/Tactic exact" "") +; (gtk_accel_path "/Templates/Template Unset Implicit Arguments" "") +; (gtk_accel_path "/Templates/Template Extract Inductive" "") +(gtk_accel_path "/View/Display implicit arguments" "i") +; (gtk_accel_path "/Tactics/Tactic symmetry" "") +; (gtk_accel_path "/Templates/Template Add Printing Let" "") +; (gtk_accel_path "/Help/Help for keyword" "h") +; (gtk_accel_path "/File/Save" "s") +; (gtk_accel_path "/Compile/Make makefile" "") +; (gtk_accel_path "/Templates/Template Remove LoadPath" "") +(gtk_accel_path "/Navigation/Interrupt" "Break") +(gtk_accel_path "/Navigation/End" "End") +; (gtk_accel_path "/Templates/Template Add Morphism" "") +; (gtk_accel_path "/Tactics/Tactic field" "") +; (gtk_accel_path "/Templates/Template Axiom" "") +; (gtk_accel_path "/Tactics/Tactic solve" "") +; (gtk_accel_path "/Tactics/Tactic casetype" "") +; (gtk_accel_path "/Tactics/Tactic cbv in" "") +; (gtk_accel_path "/Templates/Template Load" "") +; (gtk_accel_path "/Tactics/Tactic fourier" "") +; (gtk_accel_path "/Templates/Template Goal" "") +; (gtk_accel_path "/Tactics/Tactic exists" "") +; (gtk_accel_path "/Tactics/Tactic decompose record" "") +(gtk_accel_path "/Navigation/Go to" "Right") +; (gtk_accel_path "/Templates/Template Remark" "") +; (gtk_accel_path "/Templates/Template Set Undo" "") +; (gtk_accel_path "/Templates/Template Inductive" "") +(gtk_accel_path "/Edit/Preferences" "VoidSymbol") +; (gtk_accel_path "/Export/Html" "") +; (gtk_accel_path "/Templates/Template Extraction Inline" "") +; (gtk_accel_path "/Tactics/Tactic absurd" "") +(gtk_accel_path "/Tactics/intuition" "i") +; (gtk_accel_path "/Tactics/Tactic simple induction" "") +; (gtk_accel_path "/Queries/Queries" "") +; (gtk_accel_path "/Tactics/Tactic rewrite -- in" "") +; (gtk_accel_path "/Templates/Template Hint Rewrite" "") +; (gtk_accel_path "/Templates/Template Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]." "") +; (gtk_accel_path "/Navigation/Navigation" "") +; (gtk_accel_path "/Help/Browse Coq Manual" "") +; (gtk_accel_path "/Tactics/Tactic transitivity" "") +; (gtk_accel_path "/Tactics/Tactic auto" "") +; (gtk_accel_path "/Tactics/Tactic dependent inversion -- with" "") +; (gtk_accel_path "/Tactics/Tactic assumption" "") +; (gtk_accel_path "/Templates/Template Notation" "") +; (gtk_accel_path "/Edit/Cut" "x") +; (gtk_accel_path "/Templates/Template Theorem" "") +; (gtk_accel_path "/Tactics/Tactic constructor" "") +; (gtk_accel_path "/Tactics/Tactic elim -- with" "") +; (gtk_accel_path "/Templates/Template Identity Coercion" "") +; (gtk_accel_path "/Queries/Whelp Locate" "") +(gtk_accel_path "/View/Display all low-level contents" "l") +; (gtk_accel_path "/Tactics/Tactic right" "") +; (gtk_accel_path "/Edit/Find Previous" "F3") +; (gtk_accel_path "/Tactics/Tactic cofix" "") +; (gtk_accel_path "/Templates/Template Restore State" "") +; (gtk_accel_path "/Templates/Template Lemma" "") +; (gtk_accel_path "/Tactics/Tactic refine" "") +; (gtk_accel_path "/Templates/Template Section" "") +; (gtk_accel_path "/Tactics/Tactic assert (--:=--)" "") +; (gtk_accel_path "/Templates/Template Unset Printing Wildcard" "") +; (gtk_accel_path "/Tactics/Tactic progress" "") +; (gtk_accel_path "/Templates/Template Add Printing If" "") +; (gtk_accel_path "/Templates/Template Chapter" "") +(gtk_accel_path "/File/Print..." "p") +; (gtk_accel_path "/Templates/Template Record" "") +; (gtk_accel_path "/Tactics/Tactic info" "") +; (gtk_accel_path "/Tactics/Tactic firstorder with" "") +; (gtk_accel_path "/Templates/Template Hint Unfold" "") +; (gtk_accel_path "/Templates/Template Set Silent." "") +; (gtk_accel_path "/Templates/Template Program Theorem" "") +; (gtk_accel_path "/Templates/Template Declare ML Module" "") +; (gtk_accel_path "/Tactics/Tactic lazy in" "") +; (gtk_accel_path "/Tactics/Tactic unfold -- in" "") +; (gtk_accel_path "/Edit/Paste" "v") +; (gtk_accel_path "/Templates/Template Remove Printing If" "") +; (gtk_accel_path "/Tactics/Tactic intuition" "") +; (gtk_accel_path "/Queries/SearchAbout" "F2") +; (gtk_accel_path "/Tactics/Tactic dependent rewrite ->" "") +; (gtk_accel_path "/Templates/Template Module" "") +; (gtk_accel_path "/Templates/Template Unset Extraction AutoInline" "") +(gtk_accel_path "/Templates/Scheme" "s") +; (gtk_accel_path "/Templates/Template V" "") +; (gtk_accel_path "/Templates/Template Variable" "") +; (gtk_accel_path "/Tactics/Tactic decide equality" "") +; (gtk_accel_path "/Tactics/Tactic instantiate (--:=--)" "") +; (gtk_accel_path "/Templates/Template Syntactic Definition" "") +; (gtk_accel_path "/Templates/Template Set Extraction AutoInline" "") +; (gtk_accel_path "/Templates/Template Unset Undo" "") +; (gtk_accel_path "/Tactics/Tactic dependent inversion" "") +; (gtk_accel_path "/Tactics/Tactic setoid--rewrite" "") +; (gtk_accel_path "/Templates/Template Add Field" "") +; (gtk_accel_path "/Templates/Template Require Export" "") +; (gtk_accel_path "/Tactics/Tactic rewrite <-" "") +(gtk_accel_path "/Tactics/omega" "o") +; (gtk_accel_path "/Tactics/Tactic split" "") +; (gtk_accel_path "/File/Quit" "q") +(gtk_accel_path "/View/Display existential variable instances" "e") +(gtk_accel_path "/Navigation/Start" "Home") +; (gtk_accel_path "/Tactics/Tactic dependent rewrite <-" "") +; (gtk_accel_path "/Templates/Template U" "") +; (gtk_accel_path "/Templates/Template Variables" "") +; (gtk_accel_path "/Templates/Template S" "") +; (gtk_accel_path "/Tactics/Tactic move -- after" "") +; (gtk_accel_path "/Templates/Template Unset Silent." "") +; (gtk_accel_path "/Templates/Template Local" "") +; (gtk_accel_path "/Templates/Template T" "") +; (gtk_accel_path "/Tactics/Tactic reflexivity" "") +; (gtk_accel_path "/Templates/Template R" "") +; (gtk_accel_path "/Templates/Template Time" "") +; (gtk_accel_path "/Templates/Template P" "") +; (gtk_accel_path "/Tactics/Tactic decompose" "") +; (gtk_accel_path "/Templates/Template N" "") +; (gtk_accel_path "/Templates/Template Eval" "") +; (gtk_accel_path "/Tactics/Tactic congruence" "") +; (gtk_accel_path "/Templates/Template O" "") +; (gtk_accel_path "/Templates/Template E" "") +; (gtk_accel_path "/Templates/Template I" "") +; (gtk_accel_path "/Templates/Template H" "") +; (gtk_accel_path "/Templates/Template Extraction Language" "") +; (gtk_accel_path "/Templates/Template M" "") +; (gtk_accel_path "/Templates/Template Derive Inversion" "") +; (gtk_accel_path "/Tactics/Tactic double induction" "") +; (gtk_accel_path "/Templates/Template L" "") +; (gtk_accel_path "/Templates/Template Derive Inversion--clear" "") +(gtk_accel_path "/View/Display universe levels" "u") +; (gtk_accel_path "/Templates/Template G" "") +; (gtk_accel_path "/Templates/Template F" "") +; (gtk_accel_path "/Tactics/Tactic dependent inversion--clear -- with" "") +; (gtk_accel_path "/Templates/Template D" "") +; (gtk_accel_path "/Edit/Edit" "") +; (gtk_accel_path "/Tactics/Tactic firstorder" "") +; (gtk_accel_path "/Templates/Template C" "") +(gtk_accel_path "/Tactics/simpl" "s") +; (gtk_accel_path "/Tactics/Tactic replace -- with" "") +; (gtk_accel_path "/Templates/Template A" "") +; (gtk_accel_path "/Templates/Template Remove Printing Record" "") +; (gtk_accel_path "/Templates/Template Qed." "") +; (gtk_accel_path "/Templates/Template Program Fixpoint" "") +(gtk_accel_path "/View/Display coercions" "c") +; (gtk_accel_path "/Tactics/Tactic hnf" "") +; (gtk_accel_path "/Tactics/Tactic injection" "") +; (gtk_accel_path "/Tactics/Tactic rewrite" "") +; (gtk_accel_path "/Templates/Template Opaque" "") +; (gtk_accel_path "/Templates/Template Focus" "") +; (gtk_accel_path "/Templates/Template Ltac" "") +; (gtk_accel_path "/Tactics/Tactic simple destruct" "") +(gtk_accel_path "/View/Display all basic low-level contents" "a") +; (gtk_accel_path "/Tactics/Tactic jp " "") +; (gtk_accel_path "/Templates/Template Test Printing Synth" "") +; (gtk_accel_path "/Tactics/Tactic set" "") +; (gtk_accel_path "/Edit/External editor" "") +; (gtk_accel_path "/View/Show Toolbar" "") +; (gtk_accel_path "/Tactics/Tactic try" "") +; (gtk_accel_path "/Tactics/Tactic discriminate" "") +(gtk_accel_path "/Templates/Fixpoint" "f") +(gtk_accel_path "/Edit/Complete Word" "slash") +(gtk_accel_path "/Navigation/Next" "greater") +; (gtk_accel_path "/Tactics/Tactic elimtype" "") +; (gtk_accel_path "/Templates/Template End" "") +; (gtk_accel_path "/Templates/Template Fixpoint" "") +; (gtk_accel_path "/View/Next tab" "Right") +; (gtk_accel_path "/File/File" "") +; (gtk_accel_path "/Tactics/Tactic setoid--replace" "") +; (gtk_accel_path "/Tactics/Tactic generalize dependent" "") +(gtk_accel_path "/Tactics/trivial" "v") +; (gtk_accel_path "/Tactics/Tactic fix -- with" "") +; (gtk_accel_path "/Tactics/Tactic pose --:=--)" "") +; (gtk_accel_path "/Tactics/Tactic auto with" "") +; (gtk_accel_path "/Templates/Template Add Printing Record" "") +; (gtk_accel_path "/Tactics/Tactic inversion -- in" "") +(gtk_accel_path "/Tactics/eauto" "e") +; (gtk_accel_path "/File/Open" "o") +; (gtk_accel_path "/Tactics/Tactic elim -- using" "") +; (gtk_accel_path "/Templates/Template Hint" "") +; (gtk_accel_path "/Tactics/Tactic tauto" "") +; (gtk_accel_path "/Export/Dvi" "") +; (gtk_accel_path "/Tactics/Tactic simpl -- in" "") +; (gtk_accel_path "/Templates/Template Hint Immediate" "") diff --git a/ide/MacOS/relatify_with-respect-to_.sh b/ide/MacOS/relatify_with-respect-to_.sh new file mode 100755 index 00000000..a24af939 --- /dev/null +++ b/ide/MacOS/relatify_with-respect-to_.sh @@ -0,0 +1,15 @@ +#!/bin/sh + +set -e + +for i in "$3/"*.dylib +do install_name_tool -change "$2"/$(basename $i) @executable_path/../Resources/lib/$(basename $i) "$1" +done +case "$1" in + *.dylib) + install_name_tool -id @executable_path/../Resources/lib/$(basename $1) $1 + for i in "$3"/*.dylib + do install_name_tool -change "$2/"$(basename $1) @executable_path/../Resources/lib/$(basename $1) $i + done;; + *) +esac diff --git a/ide/Make b/ide/Make new file mode 100644 index 00000000..c0881ca3 --- /dev/null +++ b/ide/Make @@ -0,0 +1,6 @@ +interface.mli +xmlprotocol.mli +xmlprotocol.ml +ide_slave.ml + +coqidetop.mllib diff --git a/ide/command_windows.ml b/ide/command_windows.ml deleted file mode 100644 index 67b09656..00000000 --- a/ide/command_windows.ml +++ /dev/null @@ -1,158 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* i <> index) !views - in - let _ = - toolbar#insert_button - ~tooltip:"Delete Page" - ~text:"Delete Page" - ~icon:(Ideutils.stock_to_widget `DELETE) - ~callback:remove_cb - () - in -object(self) - val frame = frame - - - val new_page_menu = new_page_menu - val notebook = notebook - - method frame = frame - method new_command ?command ?term () = - let frame = GBin.frame - ~shadow_type:`ETCHED_OUT - () - in - let _ = notebook#append_page frame#coerce in - notebook#goto_page (notebook#page_num frame#coerce); - let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in - let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in - let (combo,_) = GEdit.combo_box_entry_text ~strings:Coq_commands.state_preserving - ~packing:hbox#pack - () - in - let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in - entry#misc#set_can_default true; - let r_bin = - GBin.scrolled_window - ~vpolicy:`AUTOMATIC - ~hpolicy:`AUTOMATIC - ~packing:(vbox#pack ~fill:true ~expand:true) () in - let ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in - let result = GText.view ~packing:r_bin#add () in - let () = views := !views @ [result] in - result#misc#modify_font !current.Preferences.text_font; - let clr = Tags.color_of_string !current.Preferences.background_color in - result#misc#modify_base [`NORMAL, `COLOR clr]; - result#misc#set_can_focus true; (* false causes problems for selection *) - result#set_editable false; - let on_activate c () = - if List.mem combo#entry#text Coq_commands.state_preserving then c () - else result#buffer#set_text "Error: Not a state preserving command" - in - let callback () = - let com = combo#entry#text in - let phrase = - if String.get com (String.length com - 1) = '.' - then com ^ " " else com ^ " " ^ entry#text ^" . " - in - try - result#buffer#set_text - (match Coq.interp !coqtop ~raw:true 0 phrase with - | Interface.Fail (l,str) -> - ("Error while interpreting "^phrase^":\n"^str) - | Interface.Good results -> - ("Result for command " ^ phrase ^ ":\n" ^ results)) - with e -> - let s = Printexc.to_string e in - assert (Glib.Utf8.validate s); - result#buffer#set_text s - in - ignore (combo#entry#connect#activate ~callback:(on_activate callback)); - ignore (ok_b#connect#clicked ~callback:(on_activate callback)); - - begin match command,term with - | None,None -> () - | Some c, None -> - combo#entry#set_text c; - - | Some c, Some t -> - combo#entry#set_text c; - entry#set_text t - - | None , Some t -> - entry#set_text t - end; - on_activate callback (); - entry#misc#grab_focus (); - entry#misc#grab_default (); - ignore (entry#connect#activate ~callback); - ignore (combo#entry#connect#activate ~callback); - self#frame#misc#show () - - method refresh_font () = - let iter view = view#misc#modify_font !current.Preferences.text_font in - List.iter iter !views - - method refresh_color () = - let clr = Tags.color_of_string !current.Preferences.background_color in - let iter view = view#misc#modify_base [`NORMAL, `COLOR clr] in - List.iter iter !views - - initializer - ignore (new_page_menu#connect#clicked ~callback:self#new_command); - (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*) -end diff --git a/ide/command_windows.mli b/ide/command_windows.mli deleted file mode 100644 index 4ac480c9..00000000 --- a/ide/command_windows.mli +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Preferences.pref ref -> - object - method new_command : ?command:string -> ?term:string -> unit -> unit - method frame : GBin.frame - method refresh_font : unit -> unit - method refresh_color : unit -> unit - end diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index aafc90f4..87cc6d06 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + \%{first_ident_char}\%{ident_char}* + (\%{ident}*\.)*\%{ident} + [-+*{}] + \.(\s|\z) + (Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion) + (Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?) + (((Local)|(Global))\%{space}+)? + (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property) + (Qed)|(Defined)|(Admitted)|(Abort) + ((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*)) + + + "" + + + " + " + + + + + + do + last + first + + + apply + auto + case + case + congr + elim + exists + have + gen have + generally have + move + pose + rewrite + set + split + suffices + suff + transitivity + without loss + wlog + + + by + exact + reflexivity + + + + + + \(\*\*(\s|\z) + \*\) + + + + + + + + \(\* + \*\) + + + \(\* + \*\) + + + + + + + + + + + + \%{decl_head} + \%{dot_sep} + + + + + + + forall + fun + match + fix + cofix + with + for + end + as + let + in + if + then + else + return + using + + + Prop + Set + Type + + + \.\. + + + + + + + + Proof + \%{end_proof}\%{dot_sep} + + + + + + + + + + + + + + + + \%{dot_sep} + + + + + + + + + + + + + + + \%{undotted_sep} + + + Add + Check + Eval + Load + Undo + Goal + Print + Save + Comments + Solve\%{space}+Obligation + ((Uns)|(S))et(\%{space}+\%{ident})+ + (\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation + \%{locality}Infix + (Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist) + + + \%{locality}Hint\%{space}+ + Resolve + Immediate + Constructors + unfold + Opaque + Transparent + Extern + + + \%{space}+Scope + \%{locality}Open + \%{locality}Close + Bind + Delimit + + + \%{space}+(?'qua'\%{qualit}) + Chapter + Combined\%{space}+Scheme + End + Section + Arguments + Implicit\%{space}+Arguments + (Import)|(Include) + Require(\%{space}+((Import)|(Export)))? + (Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))? + Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive) + + + + + + (?'qua_list'(\%{space}+\%{qualit})+) + Typeclasses (Transparent)|(Opaque) + + + + + + + + diff --git a/ide/coq.lang b/ide/coq.lang new file mode 100644 index 00000000..608a4aea --- /dev/null +++ b/ide/coq.lang @@ -0,0 +1,216 @@ + + + + *.v + \(\* + \*\) + + + +