aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/configwin.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-17 23:45:26 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-24 13:21:59 +0200
commit5a564f986b5dcb74e347fbdc571d9e1a9980c2a4 (patch)
tree0b056da1338cb98e07bfc2271e58054c7ec298d2 /ide/configwin.ml
parent9392d7ed7c1dfe3ad2b3d6b0f5e039353fbd6517 (diff)
[ide] Move common protocol library to its own folder/object.
The `ide` folder contains two different binaries, the language server `coqidetop` and `coqide` itself. Even if these binaries are in the same folder, the only thing they have in common is that they link to the protocol files. In the OCaml world, having "doubly" linked files in the same project is considered a bit of an ugly practice, and some build tools such as Dune disallow it.q Thus, to clean up the build, we move the common protocol files to its own library `ideprotocol`. This helps towards Dune integration and towards having an IDE standalone target, such as the one that was implemented here: https://github.com/ejgallego/coqide-exp
Diffstat (limited to 'ide/configwin.ml')
-rw-r--r--ide/configwin.ml51
1 files changed, 51 insertions, 0 deletions
diff --git a/ide/configwin.ml b/ide/configwin.ml
new file mode 100644
index 000000000..69e8b647a
--- /dev/null
+++ b/ide/configwin.ml
@@ -0,0 +1,51 @@
+(*********************************************************************************)
+(* 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 ?width ?height
+ conf_struct_list =
+ Configwin_ihm.edit ~with_apply: true ~apply title ?width ?height conf_struct_list