From 33021618a06a94563d28691940f02a55bd9d358d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 16 May 2020 17:07:37 +0200 Subject: Move CoqIDE to its own folder The will make it possible to put a VsCoq toplevel in `ide/vscoq`. --- ide/FAQ | 54 - ide/MacOS/Info.plist.template | 89 - ide/MacOS/coqfile.icns | Bin 234599 -> 0 bytes ide/MacOS/coqide.icns | Bin 326632 -> 0 bytes ide/Make | 6 - ide/config_lexer.mli | 12 - ide/config_lexer.mll | 68 - ide/configwin.ml | 53 - ide/configwin.mli | 167 -- ide/configwin_ihm.ml | 834 ---------- ide/configwin_ihm.mli | 78 - ide/configwin_messages.ml | 50 - ide/configwin_types.ml | 121 -- ide/coq-ssreflect.lang | 249 --- ide/coq.ico | Bin 11326 -> 0 bytes ide/coq.lang | 249 --- ide/coq.ml | 610 ------- ide/coq.mli | 180 -- ide/coq.png | Bin 12907 -> 0 bytes ide/coq2.ico | Bin 4710 -> 0 bytes ide/coqOps.ml | 846 ---------- ide/coqOps.mli | 46 - ide/coq_commands.ml | 228 --- ide/coq_commands.mli | 12 - ide/coq_icon.rc | 1 - ide/coq_lex.mli | 13 - ide/coq_lex.mll | 156 -- ide/coq_style.xml | 26 - ide/coqide.ml | 1408 ---------------- ide/coqide.mli | 44 - ide/coqide/FAQ | 54 + ide/coqide/MacOS/Info.plist.template | 89 + ide/coqide/MacOS/coqfile.icns | Bin 0 -> 234599 bytes ide/coqide/MacOS/coqide.icns | Bin 0 -> 326632 bytes ide/coqide/Make | 6 + ide/coqide/config_lexer.mli | 12 + ide/coqide/config_lexer.mll | 68 + ide/coqide/configwin.ml | 53 + ide/coqide/configwin.mli | 167 ++ ide/coqide/configwin_ihm.ml | 834 ++++++++++ ide/coqide/configwin_ihm.mli | 78 + ide/coqide/configwin_messages.ml | 50 + ide/coqide/configwin_types.ml | 121 ++ ide/coqide/coq-ssreflect.lang | 249 +++ ide/coqide/coq.ico | Bin 0 -> 11326 bytes ide/coqide/coq.lang | 249 +++ ide/coqide/coq.ml | 610 +++++++ ide/coqide/coq.mli | 180 ++ ide/coqide/coq.png | Bin 0 -> 12907 bytes ide/coqide/coq2.ico | Bin 0 -> 4710 bytes ide/coqide/coqOps.ml | 846 ++++++++++ ide/coqide/coqOps.mli | 46 + ide/coqide/coq_commands.ml | 228 +++ ide/coqide/coq_commands.mli | 12 + ide/coqide/coq_icon.rc | 1 + ide/coqide/coq_lex.mli | 13 + ide/coqide/coq_lex.mll | 156 ++ ide/coqide/coq_style.xml | 26 + ide/coqide/coqide.ml | 1408 ++++++++++++++++ ide/coqide/coqide.mli | 44 + ide/coqide/coqide_QUARTZ.ml.in | 37 + ide/coqide/coqide_WIN32.ml.in | 50 + ide/coqide/coqide_X11.ml.in | 11 + ide/coqide/coqide_main.ml | 71 + ide/coqide/coqide_main.mli | 12 + ide/coqide/coqide_os_specific.mli | 11 + ide/coqide/coqide_ui.ml | 168 ++ ide/coqide/coqide_ui.mli | 12 + ide/coqide/default_bindings_src.ml | 2899 +++++++++++++++++++++++++++++++++ ide/coqide/document.ml | 189 +++ ide/coqide/document.mli | 117 ++ ide/coqide/dune | 74 + ide/coqide/fake_ide.ml | 344 ++++ ide/coqide/fileOps.ml | 156 ++ ide/coqide/fileOps.mli | 25 + ide/coqide/gtk_parsing.ml | 72 + ide/coqide/gtk_parsing.mli | 28 + ide/coqide/ide.mllib | 34 + ide/coqide/ide_common.mllib | 7 + ide/coqide/ide_win32_stubs.c | 33 + ide/coqide/idetop.ml | 596 +++++++ ide/coqide/ideutils.ml | 607 +++++++ ide/coqide/ideutils.mli | 120 ++ ide/coqide/macos_prehook.ml | 37 + ide/coqide/macos_prehook.mli | 12 + ide/coqide/microPG.ml | 344 ++++ ide/coqide/microPG.mli | 13 + ide/coqide/minilib.ml | 70 + ide/coqide/minilib.mli | 45 + ide/coqide/preferences.ml | 1066 ++++++++++++ ide/coqide/preferences.mli | 116 ++ ide/coqide/protocol/dune | 7 + ide/coqide/protocol/ideprotocol.mllib | 7 + ide/coqide/protocol/interface.ml | 263 +++ ide/coqide/protocol/richpp.ml | 171 ++ ide/coqide/protocol/richpp.mli | 53 + ide/coqide/protocol/serialize.ml | 123 ++ ide/coqide/protocol/serialize.mli | 41 + ide/coqide/protocol/xml_lexer.mli | 44 + ide/coqide/protocol/xml_lexer.mll | 317 ++++ ide/coqide/protocol/xml_parser.ml | 232 +++ ide/coqide/protocol/xml_parser.mli | 106 ++ ide/coqide/protocol/xml_printer.ml | 147 ++ ide/coqide/protocol/xml_printer.mli | 31 + ide/coqide/protocol/xmlprotocol.ml | 962 +++++++++++ ide/coqide/protocol/xmlprotocol.mli | 73 + ide/coqide/sentence.ml | 129 ++ ide/coqide/sentence.mli | 21 + ide/coqide/session.ml | 555 +++++++ ide/coqide/session.mli | 55 + ide/coqide/tags.ml | 50 + ide/coqide/tags.mli | 43 + ide/coqide/unicode_bindings.ml | 131 ++ ide/coqide/unicode_bindings.mli | 48 + ide/coqide/utf8_convert.mli | 11 + ide/coqide/utf8_convert.mll | 51 + ide/coqide/wg_Command.ml | 183 +++ ide/coqide/wg_Command.mli | 18 + ide/coqide/wg_Completion.ml | 163 ++ ide/coqide/wg_Completion.mli | 18 + ide/coqide/wg_Detachable.ml | 94 ++ ide/coqide/wg_Detachable.mli | 44 + ide/coqide/wg_Find.ml | 246 +++ ide/coqide/wg_Find.mli | 20 + ide/coqide/wg_MessageView.ml | 140 ++ ide/coqide/wg_MessageView.mli | 35 + ide/coqide/wg_Notebook.ml | 69 + ide/coqide/wg_Notebook.mli | 39 + ide/coqide/wg_ProofView.ml | 252 +++ ide/coqide/wg_ProofView.mli | 22 + ide/coqide/wg_RoutedMessageViews.ml | 47 + ide/coqide/wg_RoutedMessageViews.mli | 23 + ide/coqide/wg_ScriptView.ml | 555 +++++++ ide/coqide/wg_ScriptView.mli | 57 + ide/coqide/wg_Segment.ml | 141 ++ ide/coqide/wg_Segment.mli | 37 + ide/coqide_QUARTZ.ml.in | 37 - ide/coqide_WIN32.ml.in | 50 - ide/coqide_X11.ml.in | 11 - ide/coqide_main.ml | 71 - ide/coqide_main.mli | 12 - ide/coqide_os_specific.mli | 11 - ide/coqide_ui.ml | 168 -- ide/coqide_ui.mli | 12 - ide/default_bindings_src.ml | 2899 --------------------------------- ide/document.ml | 189 --- ide/document.mli | 117 -- ide/dune | 74 - ide/fake_ide.ml | 344 ---- ide/fileOps.ml | 156 -- ide/fileOps.mli | 25 - ide/gtk_parsing.ml | 72 - ide/gtk_parsing.mli | 28 - ide/ide.mllib | 34 - ide/ide_common.mllib | 7 - ide/ide_win32_stubs.c | 33 - ide/idetop.ml | 596 ------- ide/ideutils.ml | 607 ------- ide/ideutils.mli | 120 -- ide/macos_prehook.ml | 37 - ide/macos_prehook.mli | 12 - ide/microPG.ml | 344 ---- ide/microPG.mli | 13 - ide/minilib.ml | 70 - ide/minilib.mli | 45 - ide/preferences.ml | 1066 ------------ ide/preferences.mli | 116 -- ide/protocol/dune | 7 - ide/protocol/ideprotocol.mllib | 7 - ide/protocol/interface.ml | 263 --- ide/protocol/richpp.ml | 171 -- ide/protocol/richpp.mli | 53 - ide/protocol/serialize.ml | 123 -- ide/protocol/serialize.mli | 41 - ide/protocol/xml_lexer.mli | 44 - ide/protocol/xml_lexer.mll | 317 ---- ide/protocol/xml_parser.ml | 232 --- ide/protocol/xml_parser.mli | 106 -- ide/protocol/xml_printer.ml | 147 -- ide/protocol/xml_printer.mli | 31 - ide/protocol/xmlprotocol.ml | 962 ----------- ide/protocol/xmlprotocol.mli | 73 - ide/sentence.ml | 129 -- ide/sentence.mli | 21 - ide/session.ml | 555 ------- ide/session.mli | 55 - ide/tags.ml | 50 - ide/tags.mli | 43 - ide/unicode_bindings.ml | 131 -- ide/unicode_bindings.mli | 48 - ide/utf8_convert.mli | 11 - ide/utf8_convert.mll | 51 - ide/wg_Command.ml | 183 --- ide/wg_Command.mli | 18 - ide/wg_Completion.ml | 163 -- ide/wg_Completion.mli | 18 - ide/wg_Detachable.ml | 94 -- ide/wg_Detachable.mli | 44 - ide/wg_Find.ml | 246 --- ide/wg_Find.mli | 20 - ide/wg_MessageView.ml | 140 -- ide/wg_MessageView.mli | 35 - ide/wg_Notebook.ml | 69 - ide/wg_Notebook.mli | 39 - ide/wg_ProofView.ml | 252 --- ide/wg_ProofView.mli | 22 - ide/wg_RoutedMessageViews.ml | 47 - ide/wg_RoutedMessageViews.mli | 23 - ide/wg_ScriptView.ml | 555 ------- ide/wg_ScriptView.mli | 57 - ide/wg_Segment.ml | 141 -- ide/wg_Segment.mli | 37 - 212 files changed, 18850 insertions(+), 18850 deletions(-) delete mode 100644 ide/FAQ delete mode 100644 ide/MacOS/Info.plist.template delete mode 100644 ide/MacOS/coqfile.icns delete mode 100644 ide/MacOS/coqide.icns delete mode 100644 ide/Make delete mode 100644 ide/config_lexer.mli delete mode 100644 ide/config_lexer.mll delete mode 100644 ide/configwin.ml delete mode 100644 ide/configwin.mli delete mode 100644 ide/configwin_ihm.ml delete mode 100644 ide/configwin_ihm.mli delete mode 100644 ide/configwin_messages.ml delete mode 100644 ide/configwin_types.ml delete mode 100644 ide/coq-ssreflect.lang delete mode 100644 ide/coq.ico delete mode 100644 ide/coq.lang delete mode 100644 ide/coq.ml delete mode 100644 ide/coq.mli delete mode 100644 ide/coq.png delete mode 100644 ide/coq2.ico delete mode 100644 ide/coqOps.ml delete mode 100644 ide/coqOps.mli delete mode 100644 ide/coq_commands.ml delete mode 100644 ide/coq_commands.mli delete mode 100644 ide/coq_icon.rc delete mode 100644 ide/coq_lex.mli delete mode 100644 ide/coq_lex.mll delete mode 100644 ide/coq_style.xml delete mode 100644 ide/coqide.ml delete mode 100644 ide/coqide.mli create mode 100644 ide/coqide/FAQ create mode 100644 ide/coqide/MacOS/Info.plist.template create mode 100644 ide/coqide/MacOS/coqfile.icns create mode 100644 ide/coqide/MacOS/coqide.icns create mode 100644 ide/coqide/Make create mode 100644 ide/coqide/config_lexer.mli create mode 100644 ide/coqide/config_lexer.mll create mode 100644 ide/coqide/configwin.ml create mode 100644 ide/coqide/configwin.mli create mode 100644 ide/coqide/configwin_ihm.ml create mode 100644 ide/coqide/configwin_ihm.mli create mode 100644 ide/coqide/configwin_messages.ml create mode 100644 ide/coqide/configwin_types.ml create mode 100644 ide/coqide/coq-ssreflect.lang create mode 100644 ide/coqide/coq.ico create mode 100644 ide/coqide/coq.lang create mode 100644 ide/coqide/coq.ml create mode 100644 ide/coqide/coq.mli create mode 100644 ide/coqide/coq.png create mode 100644 ide/coqide/coq2.ico create mode 100644 ide/coqide/coqOps.ml create mode 100644 ide/coqide/coqOps.mli create mode 100644 ide/coqide/coq_commands.ml create mode 100644 ide/coqide/coq_commands.mli create mode 100644 ide/coqide/coq_icon.rc create mode 100644 ide/coqide/coq_lex.mli create mode 100644 ide/coqide/coq_lex.mll create mode 100644 ide/coqide/coq_style.xml create mode 100644 ide/coqide/coqide.ml create mode 100644 ide/coqide/coqide.mli create mode 100644 ide/coqide/coqide_QUARTZ.ml.in create mode 100644 ide/coqide/coqide_WIN32.ml.in create mode 100644 ide/coqide/coqide_X11.ml.in create mode 100644 ide/coqide/coqide_main.ml create mode 100644 ide/coqide/coqide_main.mli create mode 100644 ide/coqide/coqide_os_specific.mli create mode 100644 ide/coqide/coqide_ui.ml create mode 100644 ide/coqide/coqide_ui.mli create mode 100644 ide/coqide/default_bindings_src.ml create mode 100644 ide/coqide/document.ml create mode 100644 ide/coqide/document.mli create mode 100644 ide/coqide/dune create mode 100644 ide/coqide/fake_ide.ml create mode 100644 ide/coqide/fileOps.ml create mode 100644 ide/coqide/fileOps.mli create mode 100644 ide/coqide/gtk_parsing.ml create mode 100644 ide/coqide/gtk_parsing.mli create mode 100644 ide/coqide/ide.mllib create mode 100644 ide/coqide/ide_common.mllib create mode 100644 ide/coqide/ide_win32_stubs.c create mode 100644 ide/coqide/idetop.ml create mode 100644 ide/coqide/ideutils.ml create mode 100644 ide/coqide/ideutils.mli create mode 100644 ide/coqide/macos_prehook.ml create mode 100644 ide/coqide/macos_prehook.mli create mode 100644 ide/coqide/microPG.ml create mode 100644 ide/coqide/microPG.mli create mode 100644 ide/coqide/minilib.ml create mode 100644 ide/coqide/minilib.mli create mode 100644 ide/coqide/preferences.ml create mode 100644 ide/coqide/preferences.mli create mode 100644 ide/coqide/protocol/dune create mode 100644 ide/coqide/protocol/ideprotocol.mllib create mode 100644 ide/coqide/protocol/interface.ml create mode 100644 ide/coqide/protocol/richpp.ml create mode 100644 ide/coqide/protocol/richpp.mli create mode 100644 ide/coqide/protocol/serialize.ml create mode 100644 ide/coqide/protocol/serialize.mli create mode 100644 ide/coqide/protocol/xml_lexer.mli create mode 100644 ide/coqide/protocol/xml_lexer.mll create mode 100644 ide/coqide/protocol/xml_parser.ml create mode 100644 ide/coqide/protocol/xml_parser.mli create mode 100644 ide/coqide/protocol/xml_printer.ml create mode 100644 ide/coqide/protocol/xml_printer.mli create mode 100644 ide/coqide/protocol/xmlprotocol.ml create mode 100644 ide/coqide/protocol/xmlprotocol.mli create mode 100644 ide/coqide/sentence.ml create mode 100644 ide/coqide/sentence.mli create mode 100644 ide/coqide/session.ml create mode 100644 ide/coqide/session.mli create mode 100644 ide/coqide/tags.ml create mode 100644 ide/coqide/tags.mli create mode 100644 ide/coqide/unicode_bindings.ml create mode 100644 ide/coqide/unicode_bindings.mli create mode 100644 ide/coqide/utf8_convert.mli create mode 100644 ide/coqide/utf8_convert.mll create mode 100644 ide/coqide/wg_Command.ml create mode 100644 ide/coqide/wg_Command.mli create mode 100644 ide/coqide/wg_Completion.ml create mode 100644 ide/coqide/wg_Completion.mli create mode 100644 ide/coqide/wg_Detachable.ml create mode 100644 ide/coqide/wg_Detachable.mli create mode 100644 ide/coqide/wg_Find.ml create mode 100644 ide/coqide/wg_Find.mli create mode 100644 ide/coqide/wg_MessageView.ml create mode 100644 ide/coqide/wg_MessageView.mli create mode 100644 ide/coqide/wg_Notebook.ml create mode 100644 ide/coqide/wg_Notebook.mli create mode 100644 ide/coqide/wg_ProofView.ml create mode 100644 ide/coqide/wg_ProofView.mli create mode 100644 ide/coqide/wg_RoutedMessageViews.ml create mode 100644 ide/coqide/wg_RoutedMessageViews.mli create mode 100644 ide/coqide/wg_ScriptView.ml create mode 100644 ide/coqide/wg_ScriptView.mli create mode 100644 ide/coqide/wg_Segment.ml create mode 100644 ide/coqide/wg_Segment.mli delete mode 100644 ide/coqide_QUARTZ.ml.in delete mode 100644 ide/coqide_WIN32.ml.in delete mode 100644 ide/coqide_X11.ml.in delete mode 100644 ide/coqide_main.ml delete mode 100644 ide/coqide_main.mli delete mode 100644 ide/coqide_os_specific.mli delete mode 100644 ide/coqide_ui.ml delete mode 100644 ide/coqide_ui.mli delete mode 100644 ide/default_bindings_src.ml delete mode 100644 ide/document.ml delete mode 100644 ide/document.mli delete mode 100644 ide/dune delete mode 100644 ide/fake_ide.ml delete mode 100644 ide/fileOps.ml delete mode 100644 ide/fileOps.mli delete mode 100644 ide/gtk_parsing.ml delete mode 100644 ide/gtk_parsing.mli delete mode 100644 ide/ide.mllib delete mode 100644 ide/ide_common.mllib delete mode 100644 ide/ide_win32_stubs.c delete mode 100644 ide/idetop.ml delete mode 100644 ide/ideutils.ml delete mode 100644 ide/ideutils.mli delete mode 100644 ide/macos_prehook.ml delete mode 100644 ide/macos_prehook.mli delete mode 100644 ide/microPG.ml delete mode 100644 ide/microPG.mli delete mode 100644 ide/minilib.ml delete mode 100644 ide/minilib.mli delete mode 100644 ide/preferences.ml delete mode 100644 ide/preferences.mli delete mode 100644 ide/protocol/dune delete mode 100644 ide/protocol/ideprotocol.mllib delete mode 100644 ide/protocol/interface.ml delete mode 100644 ide/protocol/richpp.ml delete mode 100644 ide/protocol/richpp.mli delete mode 100644 ide/protocol/serialize.ml delete mode 100644 ide/protocol/serialize.mli delete mode 100644 ide/protocol/xml_lexer.mli delete mode 100644 ide/protocol/xml_lexer.mll delete mode 100644 ide/protocol/xml_parser.ml delete mode 100644 ide/protocol/xml_parser.mli delete mode 100644 ide/protocol/xml_printer.ml delete mode 100644 ide/protocol/xml_printer.mli delete mode 100644 ide/protocol/xmlprotocol.ml delete mode 100644 ide/protocol/xmlprotocol.mli delete mode 100644 ide/sentence.ml delete mode 100644 ide/sentence.mli delete mode 100644 ide/session.ml delete mode 100644 ide/session.mli delete mode 100644 ide/tags.ml delete mode 100644 ide/tags.mli delete mode 100644 ide/unicode_bindings.ml delete mode 100644 ide/unicode_bindings.mli delete mode 100644 ide/utf8_convert.mli delete mode 100644 ide/utf8_convert.mll delete mode 100644 ide/wg_Command.ml delete mode 100644 ide/wg_Command.mli delete mode 100644 ide/wg_Completion.ml delete mode 100644 ide/wg_Completion.mli delete mode 100644 ide/wg_Detachable.ml delete mode 100644 ide/wg_Detachable.mli delete mode 100644 ide/wg_Find.ml delete mode 100644 ide/wg_Find.mli delete mode 100644 ide/wg_MessageView.ml delete mode 100644 ide/wg_MessageView.mli delete mode 100644 ide/wg_Notebook.ml delete mode 100644 ide/wg_Notebook.mli delete mode 100644 ide/wg_ProofView.ml delete mode 100644 ide/wg_ProofView.mli delete mode 100644 ide/wg_RoutedMessageViews.ml delete mode 100644 ide/wg_RoutedMessageViews.mli delete mode 100644 ide/wg_ScriptView.ml delete mode 100644 ide/wg_ScriptView.mli delete mode 100644 ide/wg_Segment.ml delete mode 100644 ide/wg_Segment.mli (limited to 'ide') diff --git a/ide/FAQ b/ide/FAQ deleted file mode 100644 index c8b0a5d328..0000000000 --- a/ide/FAQ +++ /dev/null @@ -1,54 +0,0 @@ - CoqIde FAQ - -Q0) What is CoqIde? -R0: A powerful graphical interface for Coq. See http://coq.inria.fr. for more informations. - -Q1) How to enable Emacs keybindings? -R1: Insert - gtk-key-theme-name = "Emacs" -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. - If some of your fonts are not available, set GDK_USE_XFT to 0. - -Q4) How to use those Forall and Exists pretty symbols? -R4) Thanks to the Notation features in Coq, you just need to insert these - lines in your Coq Buffer : -====================================================================== -Notation "∀ x : t, P" := (forall x:t, P) (at level 200, x ident). -Notation "∃ x : t, P" := (exists x:t, P) (at level 200, x ident). -====================================================================== -Copy/Paste of these lines from this file will not work outside of CoqIde. -You need to load a file containing these lines or to enter the "∀" -using an input method (see Q5). To try it just use "Require utf8" from inside -CoqIde. -To enable these notations automatically start coqide with - coqide -l utf8 -In the ide subdir of Coq library, you will find a sample utf8.v with some -pretty simple notations. - -Q5) How to define an input method for non ASCII symbols? -R5)-First solution : type "2200" to enter a forall in the script widow. - 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 : 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 - - 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. - Keep it as UTF-8 until it becomes important for you to exchange files - with non UTF-8 aware applications. - If you choose something else than UTF-8, then missing characters will - be encoded by \x{....} or \x{........} where each dot is an hex. digit. - The number between braces is the hexadecimal UNICODE index for the - missing character. - diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template deleted file mode 100644 index e4fb0e5980..0000000000 --- a/ide/MacOS/Info.plist.template +++ /dev/null @@ -1,89 +0,0 @@ - - - - - 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-2019, Inria, CNRS and contributors - 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 deleted file mode 100644 index 107e70431d..0000000000 Binary files a/ide/MacOS/coqfile.icns and /dev/null differ diff --git a/ide/MacOS/coqide.icns b/ide/MacOS/coqide.icns deleted file mode 100644 index 92bdfe773f..0000000000 Binary files a/ide/MacOS/coqide.icns and /dev/null differ diff --git a/ide/Make b/ide/Make deleted file mode 100644 index c0881ca392..0000000000 --- a/ide/Make +++ /dev/null @@ -1,6 +0,0 @@ -interface.mli -xmlprotocol.mli -xmlprotocol.ml -ide_slave.ml - -coqidetop.mllib diff --git a/ide/config_lexer.mli b/ide/config_lexer.mli deleted file mode 100644 index 196192d5be..0000000000 --- a/ide/config_lexer.mli +++ /dev/null @@ -1,12 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* string list Util.String.Map.t -> unit -val load_file : string -> string list Util.String.Map.t diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll deleted file mode 100644 index 4ef9a1fafd..0000000000 --- a/ide/config_lexer.mll +++ /dev/null @@ -1,68 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* s))::l) lexbuf } - |ignore+ { List.rev l} - -and string = parse - | '"' { Buffer.add_char string_buffer '"' } - | '\\' '"' | _ - { Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf } - | eof { eprintf "coqiderc: unterminated string\n@." } - -{ - - let load_file f = - let c = open_in f in - let lb = from_channel c in - let m = prefs Util.String.Map.empty lb in - close_in c; - m - - let print_file f m = - let c = open_out f in - let fmt = formatter_of_out_channel c in - let rec print_list fmt = function - | [] -> () - | s :: sl -> fprintf fmt "%S@ %a" s print_list sl - in - Util.String.Map.iter - (fun k s -> fprintf fmt "@[%s = %a@]@\n" k print_list s) m; - fprintf fmt "@."; - close_out c - -} diff --git a/ide/configwin.ml b/ide/configwin.ml deleted file mode 100644 index 79a1eae880..0000000000 --- a/ide/configwin.ml +++ /dev/null @@ -1,53 +0,0 @@ -(*********************************************************************************) -(* Cameleon *) -(* *) -(* Copyright (C) 2005 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. *) -(* *) -(* This program is free software; you can redistribute it and/or modify *) -(* it under the terms of the GNU Library General Public License as *) -(* published by the Free Software Foundation; either version 2 of the *) -(* License, or any later version. *) -(* *) -(* This program is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU Library General Public License for more details. *) -(* *) -(* You should have received a copy of the GNU Library General Public *) -(* License along with this program; if not, write to the Free Software *) -(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA *) -(* 02111-1307 USA *) -(* *) -(* Contact: Maxence.Guesdon@inria.fr *) -(* *) -(*********************************************************************************) - -type parameter_kind = Configwin_types.parameter_kind - -type configuration_structure = - Configwin_types.configuration_structure = - Section of string * GtkStock.id option * parameter_kind list - | Section_list of string * GtkStock.id option * configuration_structure list - -type return_button = - Configwin_types.return_button = - Return_apply - | Return_ok - | Return_cancel - -let string = Configwin_ihm.string -(* -let strings = Configwin_ihm.strings -let list = Configwin_ihm.list -*) -let bool = Configwin_ihm.bool -let combo = Configwin_ihm.combo -let custom = Configwin_ihm.custom -let modifiers = Configwin_ihm.modifiers - -let edit - ?(apply=(fun () -> ())) - title ?parent ?width ?height - conf_struct_list = - Configwin_ihm.edit ~with_apply: true ~apply title ?parent ?width ?height conf_struct_list diff --git a/ide/configwin.mli b/ide/configwin.mli deleted file mode 100644 index b5c3e74aec..0000000000 --- a/ide/configwin.mli +++ /dev/null @@ -1,167 +0,0 @@ -(*********************************************************************************) -(* Cameleon *) -(* *) -(* Copyright (C) 2005 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. *) -(* *) -(* This program is free software; you can redistribute it and/or modify *) -(* it under the terms of the GNU Library General Public License as *) -(* published by the Free Software Foundation; either version 2 of the *) -(* License, or any later version. *) -(* *) -(* This program is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU Library General Public License for more details. *) -(* *) -(* You should have received a copy of the GNU Library General Public *) -(* License along with this program; if not, write to the Free Software *) -(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA *) -(* 02111-1307 USA *) -(* *) -(* Contact: Maxence.Guesdon@inria.fr *) -(* *) -(*********************************************************************************) - -(** This module is the interface of the Configwin library. *) - -(** {2 Types} *) - -(** This type represents the different kinds of parameters. *) -type parameter_kind;; - -(** This type represents the structure of the configuration window. *) -type configuration_structure = - | Section of string * GtkStock.id option * parameter_kind list - (** label of the section, icon, parameters *) - | Section_list of string * GtkStock.id option * configuration_structure list - (** label of the section, icon, list of the sub sections *) -;; - -(** To indicate what button pushed the user when the window is closed. *) -type return_button = - Return_apply - (** The user clicked on Apply at least once before - closing the window with Cancel or the window manager. *) - | Return_ok - (** The user closed the window with the ok button. *) - | Return_cancel - (** The user closed the window with the cancel - button or the window manager but never clicked - on the apply button.*) - -(** {2 Functions to create parameters} *) - -(** [string label value] creates a string parameter. - @param editable indicate if the value is editable (default is [true]). - @param expand indicate if the entry widget must expand or not (default is [true]). - @param help an optional help message. - @param f the function called to apply the value (default function does nothing). -*) -val string : ?editable: bool -> ?expand: bool -> ?help: string -> - ?f: (string -> unit) -> string -> string -> parameter_kind - -(** [bool label value] creates a boolean parameter. - @param editable indicate if the value is editable (default is [true]). - @param help an optional help message. - @param f the function called to apply the value (default function does nothing). -*) -val bool : ?editable: bool -> ?help: string -> - ?f: (bool -> unit) -> string -> bool -> parameter_kind - -(* -(** [strings label value] creates a string list parameter. - @param editable indicate if the value is editable (default is [true]). - @param help an optional help message. - @param f the function called to apply the value (default function does nothing). - @param add the function returning a list of strings when the user wants to add strings - (default returns an empty list). - @param eq the comparison function, used not to have doubles in list. Default - is [Pervasives.(=)]. If you want to allow doubles in the list, give a function - always returning false. -*) -val strings : ?editable: bool -> ?help: string -> - ?f: (string list -> unit) -> - ?eq: (string -> string -> bool) -> - ?add: (unit -> string list) -> - string -> string list -> parameter_kind - -(** [list label f_strings value] creates a list parameter. - [f_strings] is a function taking a value and returning a list - of strings to display it. The list length should be the same for - any value, and the same as the titles list length. The [value] - is the initial list. - @param editable indicate if the value is editable (default is [true]). - @param help an optional help message. - @param f the function called to apply the value (default function does nothing). - @param eq the comparison function, used not to have doubles in list. Default - is [Pervasives.(=)]. If you want to allow doubles in the list, give a function - always returning false. - @param edit an optional function to use to edit an element of the list. - The function returns an element, no matter if element was changed or not. - When this function is given, a "Edit" button appears next to the list. - @param add the function returning a list of values when the user wants to add values - (default returns an empty list). - @param titles an optional list of titles for the list. If the [f_strings] - function returns a list with more than one element, then you must give - a list of titles. - @param color an optional function returning the optional color for a given element. - This color is used to display the element in the list. The default function returns - no color for any element. -*) -val list : ?editable: bool -> ?help: string -> - ?f: ('a list -> unit) -> - ?eq: ('a -> 'a -> bool) -> - ?edit: ('a -> 'a) -> - ?add: (unit -> 'a list) -> - ?titles: string list -> - ?color: ('a -> string option) -> - string -> - ('a -> string list) -> - 'a list -> - parameter_kind -*) - -(** [combo label choices value] creates a combo parameter. - @param editable indicate if the value is editable (default is [true]). - @param expand indicate if the entry widget must expand or not (default is [true]). - @param help an optional help message. - @param f the function called to apply the value (default function does nothing). - @param new_allowed indicate if a entry not in the list of choices is accepted - (default is [false]). - @param blank_allowed indicate if the empty selection [""] is accepted - (default is [false]). -*) -val combo : ?editable: bool -> ?expand: bool -> ?help: string -> - ?f: (string -> unit) -> - ?new_allowed: bool -> ?blank_allowed: bool -> - string -> string list -> string -> parameter_kind - -val modifiers : ?editable: bool -> ?expand: bool -> ?help: string -> - ?allow:(Gdk.Tags.modifier list) -> - ?f: (Gdk.Tags.modifier list -> unit) -> - string -> Gdk.Tags.modifier list -> parameter_kind - -(** [custom box f expand] creates a custom parameter, with - the given [box], the [f] function is called when the user - wants to apply his changes, and [expand] indicates if the box - must expand in its father. - @param label if a value is specified, a the box is packed into a frame. -*) -val custom : ?label: string -> GPack.box -> (unit -> unit) -> bool -> parameter_kind - -(** {2 Functions creating configuration windows and boxes} *) - -(** This function takes a configuration structure and creates a window - to configure the various parameters. - @param apply this function is called when the apply button is clicked, after - giving new values to parameters. -*) -val edit : - ?apply: (unit -> unit) -> - string -> - ?parent:GWindow.window -> - ?width:int -> - ?height:int -> - configuration_structure list -> - return_button diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml deleted file mode 100644 index e768131dcf..0000000000 --- a/ide/configwin_ihm.ml +++ /dev/null @@ -1,834 +0,0 @@ -(*********************************************************************************) -(* Cameleon *) -(* *) -(* Copyright (C) 2005 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. *) -(* *) -(* This program is free software; you can redistribute it and/or modify *) -(* it under the terms of the GNU Library General Public License as *) -(* published by the Free Software Foundation; either version 2 of the *) -(* License, or any later version. *) -(* *) -(* This program is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU Library General Public License for more details. *) -(* *) -(* You should have received a copy of the GNU Library General Public *) -(* License along with this program; if not, write to the Free Software *) -(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA *) -(* 02111-1307 USA *) -(* *) -(* Contact: Maxence.Guesdon@inria.fr *) -(* *) -(*********************************************************************************) - -(** This module contains the gui functions of Configwin.*) - -open Configwin_types - -let set_help_tip wev = function - | None -> () - | Some help -> GtkBase.Widget.Tooltip.set_text wev#as_widget help - -let modifiers_to_string m = - let rec iter m s = - match m with - [] -> s - | c :: m -> - iter m (( - match c with - `CONTROL -> "" - | `SHIFT -> "" - | `LOCK -> "" - | `MOD1 -> "" - | `MOD2 -> "" - | `MOD3 -> "" - | `MOD4 -> "" - | `MOD5 -> "" - | _ -> raise Not_found - ) ^ s) - in - iter m "" - -class type widget = - object - method box : GObj.widget - method apply : unit -> unit - end - -let debug = false -let dbg s = if debug then Minilib.log s else () -(* -(** This class builds a frame with a clist and two buttons : - one to add items and one to remove the selected items. - The class takes in parameter a function used to add items and - a string list ref which is used to store the content of the clist. - At last, a title for the frame is also in parameter, so that - each instance of the class creates a frame. *) -class ['a] list_selection_box - (listref : 'a list ref) - titles_opt - help_opt - f_edit_opt - f_strings - f_color - (eq : 'a -> 'a -> bool) - add_function title editable - = - let _ = dbg "list_selection_box" in - let wev = GBin.event_box () in - let wf = GBin.frame ~label: title ~packing: wev#add () in - let hbox = GPack.hbox ~packing: wf#add () in - (* the scroll window and the clist *) - let wscroll = GBin.scrolled_window - ~vpolicy: `AUTOMATIC - ~hpolicy: `AUTOMATIC - ~packing: (hbox#pack ~expand: true) () - in - let wlist = match titles_opt with - None -> - GList.clist ~selection_mode: `MULTIPLE - ~titles_show: false - ~packing: wscroll#add () - | Some l -> - GList.clist ~selection_mode: `MULTIPLE - ~titles: l - ~titles_show: true - ~packing: wscroll#add () - in - let _ = set_help_tip wev help_opt in - (* the vbox for the buttons *) - let vbox_buttons = GPack.vbox () in - let _ = - if editable then - let _ = hbox#pack ~expand: false vbox_buttons#coerce in - () - else - () - in - let _ = dbg "list_selection_box: wb_add" in - let wb_add = GButton.button - ~label: Configwin_messages.mAdd - ~packing: (vbox_buttons#pack ~expand:false ~padding:2) - () - in - let wb_edit = GButton.button - ~label: Configwin_messages.mEdit - () - in - let _ = match f_edit_opt with - None -> () - | Some _ -> vbox_buttons#pack ~expand:false ~padding:2 wb_edit#coerce - in - let wb_up = GButton.button - ~label: Configwin_messages.mUp - ~packing: (vbox_buttons#pack ~expand:false ~padding:2) - () - in - let wb_remove = GButton.button - ~label: Configwin_messages.mRemove - ~packing: (vbox_buttons#pack ~expand:false ~padding:2) - () - in - let _ = dbg "list_selection_box: object(self)" in - object (self) - (** the list of selected rows *) - val mutable list_select = [] - - (** This method returns the frame created. *) - method box = wev - - method update l = - (* set the new list in the provided listref *) - listref := l; - (* insert the elements in the clist *) - wlist#freeze (); - wlist#clear (); - List.iter - (fun ele -> - ignore (wlist#append (f_strings ele)); - match f_color ele with - None -> () - | Some c -> - try wlist#set_row ~foreground: (`NAME c) (wlist#rows - 1) - with _ -> () - ) - !listref; - - (match titles_opt with - None -> wlist#columns_autosize () - | Some _ -> GToolbox.autosize_clist wlist); - wlist#thaw (); - (* the list of selectd elements is now empty *) - list_select <- [] - - (** Move up the selected rows. *) - method up_selected = - let rec iter n selrows l = - match selrows with - [] -> (l, []) - | m :: qrows -> - match l with - [] -> ([],[]) - | [_] -> (l,[]) - | e1 :: e2 :: q when m = n + 1 -> - let newl, newrows = iter (n+1) qrows (e1 :: q) in - (e2 :: newl, n :: newrows) - | e1 :: q -> - let newl, newrows = iter (n+1) selrows q in - (e1 :: newl, newrows) - in - let sorted_select = List.sort compare list_select in - let new_list, new_rows = iter 0 sorted_select !listref in - self#update new_list; - List.iter (fun n -> wlist#select n 0) new_rows - - (** Make the user edit the first selected row. *) - method edit_selected f_edit = - let sorted_select = List.sort compare list_select in - match sorted_select with - [] -> () - | n :: _ -> - try - let ele = List.nth !listref n in - let ele2 = f_edit ele in - let rec iter m = function - [] -> [] - | e :: q -> - if n = m then - ele2 :: q - else - e :: (iter (m+1) q) - in - self#update (iter 0 !listref); - wlist#select n 0 - with - Not_found -> - () - - initializer - - (* create the functions called when the buttons are clicked *) - let f_add () = - (* get the files to add with the function provided *) - let l = add_function () in - (* remove from the list the ones which are already in - the listref, using the eq predicate *) - let l2 = List.fold_left - (fun acc -> fun ele -> - if List.exists (eq ele) acc then - acc - else - acc @ [ele]) - !listref - l - in - self#update l2 - in - let f_remove () = - (* remove the selected items from the listref and the clist *) - let rec iter n = function - [] -> [] - | h :: q -> - if List.mem n list_select then - iter (n+1) q - else - h :: (iter (n+1) q) - in - let new_list = iter 0 !listref in - self#update new_list - in - let _ = dbg "list_selection_box: connecting wb_add" in - (* connect the functions to the buttons *) - ignore (wb_add#connect#clicked ~callback:f_add); - let _ = dbg "list_selection_box: connecting wb_remove" in - ignore (wb_remove#connect#clicked ~callback:f_remove); - let _ = dbg "list_selection_box: connecting wb_up" in - ignore (wb_up#connect#clicked ~callback:(fun () -> self#up_selected)); - ( - match f_edit_opt with - None -> () - | Some f -> - let _ = dbg "list_selection_box: connecting wb_edit" in - ignore (wb_edit#connect#clicked ~callback:(fun () -> self#edit_selected f)) - ); - (* connect the selection and deselection of items in the clist *) - let f_select ~row ~column ~event = - try - list_select <- row :: list_select - with - Failure _ -> - () - in - let f_unselect ~row ~column ~event = - try - let new_list_select = List.filter (fun n -> n <> row) list_select in - list_select <- new_list_select - with - Failure _ -> - () - in - (* connect the select and deselect events *) - let _ = dbg "list_selection_box: connecting select_row" in - ignore(wlist#connect#select_row ~callback:f_select); - let _ = dbg "list_selection_box: connecting unselect_row" in - ignore(wlist#connect#unselect_row ~callback:f_unselect); - - (* initialize the clist with the listref *) - self#update !listref - end;; -*) - -(** This class is used to build a box for a string parameter.*) -class string_param_box param = - let _ = dbg "string_param_box" in - let hbox = GPack.hbox () in - let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in - let _wl = GMisc.label ~text: param.string_label ~packing: wev#add () in - let we = GEdit.entry - ~editable: param.string_editable - ~packing: (hbox#pack ~expand: param.string_expand ~padding: 2) - () - in - let _ = set_help_tip wev param.string_help in - let _ = we#set_text (param.string_to_string param.string_value) in - - object (self) - - (** This method returns the main box ready to be packed. *) - method box = hbox#coerce - - (** This method applies the new value of the parameter. *) - method apply = - let new_value = param.string_of_string we#text in - if new_value <> param.string_value then - let _ = param.string_f_apply new_value in - param.string_value <- new_value - else - () - end ;; - -(** This class is used to build a box for a combo parameter.*) -class combo_param_box param = - let _ = dbg "combo_param_box" in - let hbox = GPack.hbox () in - let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in - let _wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in - let _ = set_help_tip wev param.combo_help in - let get_value = if not param.combo_new_allowed then - let wc = GEdit.combo_box_text - ~strings: param.combo_choices - ?active:(let rec aux i = function - |[] -> None - |h::_ when h = param.combo_value -> Some i - |_::t -> aux (succ i) t - in aux 0 param.combo_choices) - ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2) - () - in - fun () -> match GEdit.text_combo_get_active wc with |None -> "" |Some s -> s - else - let (wc,_) = GEdit.combo_box_entry_text - ~strings: param.combo_choices - ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2) - () - in - let _ = wc#entry#set_editable param.combo_editable in - let _ = wc#entry#set_text param.combo_value in - fun () -> wc#entry#text - in -object (self) - - (** This method returns the main box ready to be packed. *) - method box = hbox#coerce - - (** This method applies the new value of the parameter. *) - method apply = - let new_value = get_value () in - if new_value <> param.combo_value then - let _ = param.combo_f_apply new_value in - param.combo_value <- new_value - else - () -end ;; - -(** Class used to pack a custom box. *) -class custom_param_box param = - let _ = dbg "custom_param_box" in - let top = - match param.custom_framed with - None -> param.custom_box#coerce - | Some l -> - let wf = GBin.frame ~label: l () in - wf#add param.custom_box#coerce; - wf#coerce - in - object (self) - method box = top - method apply = param.custom_f_apply () - end - -(** This class is used to build a box for a text parameter.*) -class text_param_box param = - let _ = dbg "text_param_box" in - let wf = GBin.frame ~label: param.string_label ~height: 100 () in - let wev = GBin.event_box ~packing: wf#add () in - let wscroll = GBin.scrolled_window - ~vpolicy: `AUTOMATIC - ~hpolicy: `AUTOMATIC - ~packing: wev#add () - in - let wview = GText.view - ~editable: param.string_editable - ~packing: wscroll#add - () - in - let _ = set_help_tip wev param.string_help in - let _ = dbg "text_param_box: buffer creation" in - let buffer = GText.buffer () in - - let _ = wview#set_buffer buffer in - let _ = buffer#insert (param.string_to_string param.string_value) in - let _ = dbg "text_param_box: object(self)" in - object (self) - val wview = wview - - (** This method returns the main box ready to be packed. *) - method box = wf#coerce - - (** This method applies the new value of the parameter. *) - method apply = - let v = param.string_of_string (buffer#get_text ()) in - if v <> param.string_value then - ( - dbg "apply new value!"; - let _ = param.string_f_apply v in - param.string_value <- v - ) - else - () - end ;; - -(** This class is used to build a box for a boolean parameter.*) -class bool_param_box param = - let _ = dbg "bool_param_box" in - let wchk = GButton.check_button - ~label: param.bool_label - () - in - let _ = set_help_tip wchk param.bool_help in - let _ = wchk#set_active param.bool_value in - let _ = wchk#misc#set_sensitive param.bool_editable in - - object (self) - - (** This method returns the check button ready to be packed. *) - method box = wchk#coerce - - (** This method applies the new value of the parameter. *) - method apply = - let new_value = wchk#active in - if new_value <> param.bool_value then - let _ = param.bool_f_apply new_value in - param.bool_value <- new_value - else - () - end ;; - -class modifiers_param_box param = - let hbox = GPack.hbox () in - let wev = GBin.event_box ~packing: (hbox#pack ~expand:true ~fill:true ~padding: 2) () in - let _wl = GMisc.label ~text: param.md_label ~packing: wev#add () in - let value = ref param.md_value in - let _ = List.map (fun modifier -> - let but = GButton.toggle_button - ~label:(modifiers_to_string [modifier]) - ~active:(List.mem modifier param.md_value) - ~packing:(hbox#pack ~expand:false) () in - ignore (but#connect#toggled - ~callback:(fun _ -> if but#active then value := modifier::!value - else value := List.filter ((<>) modifier) !value))) - param.md_allow - in - let _ = set_help_tip wev param.md_help in - object (self) - - (** This method returns the main box ready to be packed. *) - method box = hbox#coerce - - (** This method applies the new value of the parameter. *) - method apply = - let new_value = !value in - if new_value <> param.md_value then - let _ = param.md_f_apply new_value in - param.md_value <- new_value - else - () - end ;; -(* -(** This class is used to build a box for a parameter whose values are a list.*) -class ['a] list_param_box (param : 'a list_param) = - let _ = dbg "list_param_box" in - let listref = ref param.list_value in - let frame_selection = new list_selection_box - listref - param.list_titles - param.list_help - param.list_f_edit - param.list_strings - param.list_color - param.list_eq - param.list_f_add param.list_label param.list_editable - tt - in - - object (self) - - (** This method returns the main box ready to be packed. *) - method box = frame_selection#box#coerce - - (** This method applies the new value of the parameter. *) - method apply = - param.list_f_apply !listref ; - param.list_value <- !listref - end ;; -*) - -(** This class creates a configuration box from a configuration structure *) -class configuration_box conf_struct = - - let main_box = GPack.hbox () in - - let columns = new GTree.column_list in - let icon_col = columns#add GtkStock.conv in - let label_col = columns#add Gobject.Data.string in - let box_col = columns#add Gobject.Data.caml in - let () = columns#lock () in - - let pane = GPack.paned `HORIZONTAL ~packing:main_box#add () in - - (* Tree view part *) - let scroll = GBin.scrolled_window ~hpolicy:`NEVER ~packing:pane#pack1 () in - let tree = GTree.tree_store columns in - let view = GTree.view ~model:tree ~headers_visible:false ~packing:scroll#add_with_viewport () in - let selection = view#selection in - let _ = selection#set_mode `SINGLE in - - let menu_box = GPack.vbox ~packing:pane#pack2 () in - - let renderer = (GTree.cell_renderer_pixbuf [], ["stock-id", icon_col]) in - let col = GTree.view_column ~renderer () in - let _ = view#append_column col in - - let renderer = (GTree.cell_renderer_text [], ["text", label_col]) in - let col = GTree.view_column ~renderer () in - let _ = view#append_column col in - - let make_param (main_box : #GPack.box) = function - | String_param p -> - let box = new string_param_box p in - let _ = main_box#pack ~expand: false ~padding: 2 box#box in - box - | Combo_param p -> - let box = new combo_param_box p in - let _ = main_box#pack ~expand: false ~padding: 2 box#box in - box - | Text_param p -> - let box = new text_param_box p in - let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in - box - | Bool_param p -> - let box = new bool_param_box p in - let _ = main_box#pack ~expand: false ~padding: 2 box#box in - box - | List_param f -> - let box = f () in - let _ = main_box#pack ~expand: true ~padding: 2 box#box in - box - | Custom_param p -> - let box = new custom_param_box p in - let _ = main_box#pack ~expand: p.custom_expand ~padding: 2 box#box in - box - | Modifiers_param p -> - let box = new modifiers_param_box p in - let _ = main_box#pack ~expand: false ~padding: 2 box#box in - box - in - - let set_icon iter = function - | None -> () - | Some icon -> tree#set ~row:iter ~column:icon_col icon - in - - (* Populate the tree *) - - let rec make_tree iter conf_struct = - (* box is not shown at first *) - let box = GPack.vbox ~packing:(menu_box#pack ~expand:true) ~show:false () in - let new_iter = match iter with - | None -> tree#append () - | Some parent -> tree#append ~parent () - in - match conf_struct with - | Section (label, icon, param_list) -> - let params = List.map (make_param box) param_list in - let widget = - object - method box = box#coerce - method apply () = List.iter (fun param -> param#apply) params - end - in - let () = tree#set ~row:new_iter ~column:label_col label in - let () = set_icon new_iter icon in - let () = tree#set ~row:new_iter ~column:box_col widget in - () - | Section_list (label, icon, struct_list) -> - let widget = - object - (* Section_list does not contain any effect widget, so we do not have to - apply anything. *) - method apply () = () - method box = box#coerce - end - in - let () = tree#set ~row:new_iter ~column:label_col label in - let () = set_icon new_iter icon in - let () = tree#set ~row:new_iter ~column:box_col widget in - List.iter (make_tree (Some new_iter)) struct_list - in - - let () = List.iter (make_tree None) conf_struct in - - (* Dealing with signals *) - - let current_prop : widget option ref = ref None in - - let select_iter iter = - let () = match !current_prop with - | None -> () - | Some box -> box#box#misc#hide () - in - let box = tree#get ~row:iter ~column:box_col in - let () = box#box#misc#show () in - current_prop := Some box - in - - let when_selected () = - let rows = selection#get_selected_rows in - match rows with - | [] -> () - | row :: _ -> - let iter = tree#get_iter row in - select_iter iter - in - - (* Focus on a box when selected *) - - let _ = selection#connect#changed ~callback:when_selected in - - let _ = match tree#get_iter_first with - | None -> () - | Some iter -> select_iter iter - in - - object - - method box = main_box - - method apply = - let foreach _ iter = - let widget = tree#get ~row:iter ~column:box_col in - widget#apply(); false - in - tree#foreach foreach - - end - -(** This function takes a configuration structure list and creates a window - to configure the various parameters. *) -let edit ?(with_apply=true) - ?(apply=(fun () -> ())) - title ?parent ?width ?height - conf_struct = - let dialog = GWindow.dialog - ~position:`CENTER - ~modal: true ~title: title - ~type_hint:`DIALOG - ?parent ?height ?width - () - in - let config_box = new configuration_box conf_struct in - - let _ = dialog#vbox#pack ~expand:true config_box#box#coerce in - - if with_apply then - dialog#add_button Configwin_messages.mApply `APPLY; - - dialog#add_button Configwin_messages.mOk `OK; - dialog#add_button Configwin_messages.mCancel `CANCEL; - - let destroy () = - dialog#destroy (); - in - let rec iter rep = - try - match dialog#run () with - | `APPLY -> config_box#apply; iter Return_apply - | `OK -> config_box#apply; destroy (); Return_ok - | _ -> destroy (); rep - with - Failure s -> - GToolbox.message_box ~title:"Error" s; iter rep - | e -> - GToolbox.message_box ~title:"Error" (Printexc.to_string e); iter rep - in - iter Return_cancel - -(* -let edit_string l s = - match GToolbox.input_string ~title: l ~text: s Configwin_messages.mValue with - None -> s - | Some s2 -> s2 -*) - -(** Create a string param. *) -let string ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v = - String_param - { - string_label = label ; - string_help = help ; - string_value = v ; - string_editable = editable ; - string_f_apply = f ; - string_expand = expand ; - string_to_string = (fun x -> x) ; - string_of_string = (fun x -> x) ; - } - -(** Create a bool param. *) -let bool ?(editable=true) ?help ?(f=(fun _ -> ())) label v = - Bool_param - { - bool_label = label ; - bool_help = help ; - bool_value = v ; - bool_editable = editable ; - bool_f_apply = f ; - } - -(* -(** Create a list param. *) -let list ?(editable=true) ?help - ?(f=(fun (_:'a list) -> ())) - ?(eq=Pervasives.(=)) - ?(edit:('a -> 'a) option) - ?(add=(fun () -> ([] : 'a list))) - ?titles ?(color=(fun (_:'a) -> (None : string option))) - label (f_strings : 'a -> string list) v = - List_param - (fun () -> - new list_param_box - { - list_label = label ; - list_help = help ; - list_value = v ; - list_editable = editable ; - list_titles = titles; - list_eq = eq ; - list_strings = f_strings ; - list_color = color ; - list_f_edit = edit ; - list_f_add = add ; - list_f_apply = f ; - } - ) - -(** Create a strings param. *) -let strings ?(editable=true) ?help - ?(f=(fun _ -> ())) - ?(eq=Pervasives.(=)) - ?(add=(fun () -> [])) label v = - list ~editable ?help ~f ~eq ~edit: (edit_string label) ~add label (fun s -> [s]) v -*) - -(** Create a combo param. *) -let combo ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) - ?(new_allowed=false) - ?(blank_allowed=false) label choices v = - Combo_param - { - combo_label = label ; - combo_help = help ; - combo_value = v ; - combo_editable = editable ; - combo_choices = choices ; - combo_new_allowed = new_allowed ; - combo_blank_allowed = blank_allowed ; - combo_f_apply = f ; - combo_expand = expand ; - } - -let modifiers - ?(editable=true) - ?(expand=true) - ?help - ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5]) - ?(f=(fun _ -> ())) label v = - Modifiers_param - { - md_label = label ; - md_help = help ; - md_value = v ; - md_editable = editable ; - md_f_apply = f ; - md_expand = expand ; - md_allow = allow ; - } - -(** Create a custom param.*) -let custom ?label box f expand = - Custom_param - { - custom_box = box ; - custom_f_apply = f ; - custom_expand = expand ; - custom_framed = label ; - } - -(* Copying lablgtk question_box + forbidding hiding *) - -let question_box ~title ~buttons ?(default=1) ?icon ?parent message = - let button_nb = ref 0 in - let window = GWindow.dialog ~position:`CENTER ~modal:true ?parent ~type_hint:`DIALOG ~title () in - let hbox = GPack.hbox ~border_width:10 ~packing:window#vbox#add () in - let bbox = window#action_area in - begin match icon with - None -> () - | Some i -> hbox#pack i#coerce ~padding:4 - end; - ignore (GMisc.label ~text: message ~packing: hbox#add ()); - (* the function called to create each button by iterating *) - let rec iter_buttons n = function - [] -> - () - | button_label :: q -> - let b = GButton.button ~label: button_label - ~packing:(bbox#pack ~expand:true ~padding:4) () - in - ignore (b#connect#clicked ~callback: - (fun () -> button_nb := n; window#destroy ())); - (* If it's the first button then give it the focus *) - if n = default then b#grab_default () else (); - - iter_buttons (n+1) q - in - iter_buttons 1 buttons; - ignore (window#connect#destroy ~callback: GMain.Main.quit); - window#set_position `CENTER; - window#show (); - GMain.Main.main (); - !button_nb - -let message_box ~title ?icon ?parent ?(ok="Ok") message = - ignore (question_box ?icon ?parent ~title message ~buttons:[ ok ]) diff --git a/ide/configwin_ihm.mli b/ide/configwin_ihm.mli deleted file mode 100644 index ce6cd4d7c1..0000000000 --- a/ide/configwin_ihm.mli +++ /dev/null @@ -1,78 +0,0 @@ -(*********************************************************************************) -(* Cameleon *) -(* *) -(* Copyright (C) 2005 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. *) -(* *) -(* This program is free software; you can redistribute it and/or modify *) -(* it under the terms of the GNU Library General Public License as *) -(* published by the Free Software Foundation; either version 2 of the *) -(* License, or any later version. *) -(* *) -(* This program is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU Library General Public License for more details. *) -(* *) -(* You should have received a copy of the GNU Library General Public *) -(* License along with this program; if not, write to the Free Software *) -(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA *) -(* 02111-1307 USA *) -(* *) -(* Contact: Maxence.Guesdon@inria.fr *) -(* *) -(*********************************************************************************) - -open Configwin_types - -val string : ?editable: bool -> ?expand: bool -> ?help: string -> - ?f: (string -> unit) -> string -> string -> parameter_kind -val bool : ?editable: bool -> ?help: string -> - ?f: (bool -> unit) -> string -> bool -> parameter_kind -(* -val strings : ?editable: bool -> ?help: string -> - ?f: (string list -> unit) -> - ?eq: (string -> string -> bool) -> - ?add: (unit -> string list) -> - string -> string list -> parameter_kind -val list : ?editable: bool -> ?help: string -> - ?f: ('a list -> unit) -> - ?eq: ('a -> 'a -> bool) -> - ?edit: ('a -> 'a) -> - ?add: (unit -> 'a list) -> - ?titles: string list -> - ?color: ('a -> string option) -> - string -> - ('a -> string list) -> - 'a list -> - parameter_kind -*) -val combo : ?editable: bool -> ?expand: bool -> ?help: string -> - ?f: (string -> unit) -> - ?new_allowed: bool -> ?blank_allowed: bool -> - string -> string list -> string -> parameter_kind - -val modifiers : ?editable: bool -> ?expand: bool -> ?help: string -> - ?allow:(Gdk.Tags.modifier list) -> - ?f: (Gdk.Tags.modifier list -> unit) -> - string -> Gdk.Tags.modifier list -> parameter_kind -val custom : ?label: string -> GPack.box -> (unit -> unit) -> bool -> parameter_kind - -val edit : - ?with_apply:bool -> - ?apply:(unit -> unit) -> - string -> - ?parent:GWindow.window -> - ?width:int -> - ?height:int -> - configuration_structure list -> - return_button - -val question_box : title:string -> - buttons:string list -> - ?default:int -> ?icon:#GObj.widget -> - ?parent:GWindow.window -> string -> int - -val message_box : - title:string -> ?icon:#GObj.widget -> - ?parent:GWindow.window -> ?ok:string -> string -> unit diff --git a/ide/configwin_messages.ml b/ide/configwin_messages.ml deleted file mode 100644 index de1b4721d0..0000000000 --- a/ide/configwin_messages.ml +++ /dev/null @@ -1,50 +0,0 @@ -(*********************************************************************************) -(* Cameleon *) -(* *) -(* Copyright (C) 2005 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. *) -(* *) -(* This program is free software; you can redistribute it and/or modify *) -(* it under the terms of the GNU Library General Public License as *) -(* published by the Free Software Foundation; either version 2 of the *) -(* License, or any later version. *) -(* *) -(* This program is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU Library General Public License for more details. *) -(* *) -(* You should have received a copy of the GNU Library General Public *) -(* License along with this program; if not, write to the Free Software *) -(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA *) -(* 02111-1307 USA *) -(* *) -(* Contact: Maxence.Guesdon@inria.fr *) -(* *) -(*********************************************************************************) - -(** Module containing the messages of Configwin.*) - -let software = "Configwin";; -let version = "1.2";; - -let html_config = "Configwin bindings configurator for html parameters" - -let home = Option.default "" (Glib.get_home_dir ()) - -let mCapture = "Capture";; -let mType_key = "Type key" ;; -let mAdd = "Add";; -let mRemove = "Remove";; -let mUp = "Up";; -let mEdit = "Edit";; -let mOk = "Ok";; -let mCancel = "Cancel";; -let mApply = "Apply";; -let mValue = "Value" -let mKey = "Key" - -let shortcuts = "Shortcuts" -let html_end = "End with" -let html_begin = "Begin with" - diff --git a/ide/configwin_types.ml b/ide/configwin_types.ml deleted file mode 100644 index 711eccd08e..0000000000 --- a/ide/configwin_types.ml +++ /dev/null @@ -1,121 +0,0 @@ -(*********************************************************************************) -(* Cameleon *) -(* *) -(* Copyright (C) 2005 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. *) -(* *) -(* This program is free software; you can redistribute it and/or modify *) -(* it under the terms of the GNU Library General Public License as *) -(* published by the Free Software Foundation; either version 2 of the *) -(* License, or any later version. *) -(* *) -(* This program is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU Library General Public License for more details. *) -(* *) -(* You should have received a copy of the GNU Library General Public *) -(* License along with this program; if not, write to the Free Software *) -(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA *) -(* 02111-1307 USA *) -(* *) -(* Contact: Maxence.Guesdon@inria.fr *) -(* *) -(*********************************************************************************) - -(** This module contains the types used in Configwin. *) - -(** This type represents a string or filename parameter, or - any other type, depending on the given conversion functions. *) -type 'a string_param = { - string_label : string; (** the label of the parameter *) - mutable string_value : 'a; (** the current value of the parameter *) - string_editable : bool ; (** indicates if the value can be changed *) - string_f_apply : ('a -> unit) ; (** the function to call to apply the new value of the parameter *) - string_help : string option ; (** optional help string *) - string_expand : bool ; (** expand or not *) - string_to_string : 'a -> string ; - string_of_string : string -> 'a ; - } ;; - -(** This type represents a boolean parameter. *) -type bool_param = { - bool_label : string; (** the label of the parameter *) - mutable bool_value : bool; (** the current value of the parameter *) - bool_editable : bool ; (** indicates if the value can be changed *) - bool_f_apply : (bool -> unit) ; (** the function to call to apply the new value of the parameter *) - bool_help : string option ; (** optional help string *) - } ;; - -(** This type represents a parameter whose value is a list of ['a]. *) -type 'a list_param = { - list_label : string; (** the label of the parameter *) - mutable list_value : 'a list; (** the current value of the parameter *) - list_titles : string list option; (** the titles of columns, if they must be displayed *) - list_f_edit : ('a -> 'a) option; (** optional edition function *) - list_eq : ('a -> 'a -> bool) ; (** the comparison function used to get list without doubles *) - list_strings : ('a -> string list); (** the function to get a string list from a ['a]. *) - list_color : ('a -> string option) ; (** a function to get the optional color of an element *) - list_editable : bool ; (** indicates if the value can be changed *) - list_f_add : unit -> 'a list ; (** the function to call to add list *) - list_f_apply : ('a list -> unit) ; (** the function to call to apply the new value of the parameter *) - list_help : string option ; (** optional help string *) - } ;; - -type combo_param = { - combo_label : string ; - mutable combo_value : string ; - combo_choices : string list ; - combo_editable : bool ; - combo_blank_allowed : bool ; - combo_new_allowed : bool ; - combo_f_apply : (string -> unit); - combo_help : string option ; (** optional help string *) - combo_expand : bool ; (** expand the entry widget or not *) - } ;; - -type custom_param = { - custom_box : GPack.box ; - custom_f_apply : (unit -> unit) ; - custom_expand : bool ; - custom_framed : string option ; (** optional label for an optional frame *) - } ;; - -type modifiers_param = { - md_label : string ; (** the label of the parameter *) - mutable md_value : Gdk.Tags.modifier list ; - (** The value, as a list of modifiers and a key code *) - md_editable : bool ; (** indicates if the value can be changed *) - md_f_apply : Gdk.Tags.modifier list -> unit ; - (** the function to call to apply the new value of the parameter *) - md_help : string option ; (** optional help string *) - md_expand : bool ; (** expand or not *) - md_allow : Gdk.Tags.modifier list - } - - -(** This type represents the different kinds of parameters. *) -type parameter_kind = - String_param of string string_param - | List_param of (unit -> ) - | Bool_param of bool_param - | Text_param of string string_param - | Combo_param of combo_param - | Custom_param of custom_param - | Modifiers_param of modifiers_param -;; - -(** This type represents the structure of the configuration window. *) -type configuration_structure = - | Section of string * GtkStock.id option * parameter_kind list (** label of the section, icon, parameters *) - | Section_list of string * GtkStock.id option * configuration_structure list (** label of the section, list of the sub sections *) -;; - -(** To indicate what button was pushed by the user when the window is closed. *) -type return_button = - Return_apply (** The user clicked on Apply at least once before - closing the window with Cancel or the window manager. *) - | Return_ok (** The user closed the window with the ok button. *) - | Return_cancel (** The user closed the window with the cancel - button or the window manager but never clicked - on the apply button.*) diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang deleted file mode 100644 index fc7bc64a68..0000000000 --- a/ide/coq-ssreflect.lang +++ /dev/null @@ -1,249 +0,0 @@ - - - - *.v - \(\* - \*\) - - - -