From 5a564f986b5dcb74e347fbdc571d9e1a9980c2a4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 17 May 2018 23:45:26 +0200 Subject: [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 --- ide/configwin.ml | 51 +++ ide/configwin.mli | 164 +++++++ ide/configwin_ihm.ml | 809 +++++++++++++++++++++++++++++++++ ide/configwin_ihm.mli | 66 +++ ide/configwin_messages.ml | 50 +++ ide/configwin_types.ml | 121 +++++ ide/ide.mllib | 8 - ide/interface.mli | 261 ----------- ide/protocol/ideprotocol.mllib | 7 + ide/protocol/interface.ml | 261 +++++++++++ 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 | 320 +++++++++++++ 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 | 964 ++++++++++++++++++++++++++++++++++++++++ ide/protocol/xmlprotocol.mli | 73 +++ ide/richpp.ml | 171 ------- ide/richpp.mli | 53 --- ide/serialize.ml | 123 ----- ide/serialize.mli | 41 -- ide/utils/configwin.ml | 51 --- ide/utils/configwin.mli | 164 ------- ide/utils/configwin_ihm.ml | 809 --------------------------------- ide/utils/configwin_ihm.mli | 66 --- ide/utils/configwin_messages.ml | 50 --- ide/utils/configwin_types.mli | 121 ----- ide/xml_lexer.mli | 44 -- ide/xml_lexer.mll | 320 ------------- ide/xml_parser.ml | 232 ---------- ide/xml_parser.mli | 106 ----- ide/xml_printer.ml | 147 ------ ide/xml_printer.mli | 31 -- ide/xmlprotocol.ml | 964 ---------------------------------------- ide/xmlprotocol.mli | 73 --- 40 files changed, 3834 insertions(+), 3835 deletions(-) create mode 100644 ide/configwin.ml create mode 100644 ide/configwin.mli create mode 100644 ide/configwin_ihm.ml create mode 100644 ide/configwin_ihm.mli create mode 100644 ide/configwin_messages.ml create mode 100644 ide/configwin_types.ml delete mode 100644 ide/interface.mli create mode 100644 ide/protocol/ideprotocol.mllib create mode 100644 ide/protocol/interface.ml create mode 100644 ide/protocol/richpp.ml create mode 100644 ide/protocol/richpp.mli create mode 100644 ide/protocol/serialize.ml create mode 100644 ide/protocol/serialize.mli create mode 100644 ide/protocol/xml_lexer.mli create mode 100644 ide/protocol/xml_lexer.mll create mode 100644 ide/protocol/xml_parser.ml create mode 100644 ide/protocol/xml_parser.mli create mode 100644 ide/protocol/xml_printer.ml create mode 100644 ide/protocol/xml_printer.mli create mode 100644 ide/protocol/xmlprotocol.ml create mode 100644 ide/protocol/xmlprotocol.mli delete mode 100644 ide/richpp.ml delete mode 100644 ide/richpp.mli delete mode 100644 ide/serialize.ml delete mode 100644 ide/serialize.mli delete mode 100644 ide/utils/configwin.ml delete mode 100644 ide/utils/configwin.mli delete mode 100644 ide/utils/configwin_ihm.ml delete mode 100644 ide/utils/configwin_ihm.mli delete mode 100644 ide/utils/configwin_messages.ml delete mode 100644 ide/utils/configwin_types.mli delete mode 100644 ide/xml_lexer.mli delete mode 100644 ide/xml_lexer.mll delete mode 100644 ide/xml_parser.ml delete mode 100644 ide/xml_parser.mli delete mode 100644 ide/xml_printer.ml delete mode 100644 ide/xml_printer.mli delete mode 100644 ide/xmlprotocol.ml delete mode 100644 ide/xmlprotocol.mli (limited to 'ide') 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 diff --git a/ide/configwin.mli b/ide/configwin.mli new file mode 100644 index 000000000..7616e471d --- /dev/null +++ b/ide/configwin.mli @@ -0,0 +1,164 @@ +(*********************************************************************************) +(* 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 -> + ?width:int -> + ?height:int -> + configuration_structure list -> + return_button diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml new file mode 100644 index 000000000..d16efa603 --- /dev/null +++ b/ide/configwin_ihm.ml @@ -0,0 +1,809 @@ +(*********************************************************************************) +(* 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 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 + (tt:GData.tooltips) + = + 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 _ = + match help_opt with + None -> () + | Some help -> + tt#set_tip ~text: help ~privat: help wev#coerce + 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 (tt:GData.tooltips) = + 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 _ = + match param.string_help with + None -> () + | Some help -> + tt#set_tip ~text: help ~privat: help wev#coerce + 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 (tt:GData.tooltips) = + 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 _ = + match param.combo_help with + None -> () + | Some help -> + tt#set_tip ~text: help ~privat: help wev#coerce + 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 (tt:GData.tooltips) = + 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 (tt:GData.tooltips) = + 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 _ = + match param.string_help with + None -> () + | Some help -> + tt#set_tip ~text: help ~privat: help wev#coerce + 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 (tt:GData.tooltips) = + let _ = dbg "bool_param_box" in + let wchk = GButton.check_button + ~label: param.bool_label + () + in + let _ = + match param.bool_help with + None -> () + | Some help -> tt#set_tip ~text: help ~privat: help wchk#coerce + 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 _ = + match param.md_help with + None -> () + | Some help -> + let tooltips = GData.tooltips () in + ignore (hbox#connect#destroy ~callback: tooltips#destroy); + tooltips#set_tip wev#coerce ~text: help ~privat: 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) (tt:GData.tooltips) = + 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 (tt : GData.tooltips) 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 tt in + let _ = main_box#pack ~expand: false ~padding: 2 box#box in + box + | Combo_param p -> + let box = new combo_param_box p tt in + let _ = main_box#pack ~expand: false ~padding: 2 box#box in + box + | Text_param p -> + let box = new text_param_box p tt 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 tt in + let _ = main_box#pack ~expand: false ~padding: 2 box#box in + box + | List_param f -> + let box = f tt in + let _ = main_box#pack ~expand: true ~padding: 2 box#box in + box + | Custom_param p -> + let box = new custom_param_box p tt 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 ?width ?height + conf_struct = + let dialog = GWindow.dialog + ~position:`CENTER + ~modal: true ~title: title + ?height ?width + () + in + let tooltips = GData.tooltips () in + + let config_box = new configuration_box tooltips conf_struct in + + let _ = dialog#vbox#add 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 () = + tooltips#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 tt -> + 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 ; + } + tt + ) + +(** 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 ; + } diff --git a/ide/configwin_ihm.mli b/ide/configwin_ihm.mli new file mode 100644 index 000000000..c867ad912 --- /dev/null +++ b/ide/configwin_ihm.mli @@ -0,0 +1,66 @@ +(*********************************************************************************) +(* 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 -> + ?width:int -> + ?height:int -> + configuration_structure list -> + return_button diff --git a/ide/configwin_messages.ml b/ide/configwin_messages.ml new file mode 100644 index 000000000..de1b4721d --- /dev/null +++ b/ide/configwin_messages.ml @@ -0,0 +1,50 @@ +(*********************************************************************************) +(* 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 new file mode 100644 index 000000000..9e339d135 --- /dev/null +++ b/ide/configwin_types.ml @@ -0,0 +1,121 @@ +(*********************************************************************************) +(* 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 paramter *) + 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 (GData.tooltips -> ) + | 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/ide.mllib b/ide/ide.mllib index 96ea8c410..a7ade7130 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -9,15 +9,7 @@ Config_lexer Utf8_convert Preferences Project_file -Serialize -Richprinter -Xml_lexer -Xml_parser -Xml_printer -Serialize -Richpp Topfmt -Xmlprotocol Ideutils Coq Coq_lex diff --git a/ide/interface.mli b/ide/interface.mli deleted file mode 100644 index debbc8301..000000000 --- a/ide/interface.mli +++ /dev/null @@ -1,261 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* add_rty; - edit_at : edit_at_sty -> edit_at_rty; - query : query_sty -> query_rty; - goals : goals_sty -> goals_rty; - evars : evars_sty -> evars_rty; - hints : hints_sty -> hints_rty; - status : status_sty -> status_rty; - search : search_sty -> search_rty; - get_options : get_options_sty -> get_options_rty; - set_options : set_options_sty -> set_options_rty; - mkcases : mkcases_sty -> mkcases_rty; - about : about_sty -> about_rty; - stop_worker : stop_worker_sty -> stop_worker_rty; - print_ast : print_ast_sty -> print_ast_rty; - annotate : annotate_sty -> annotate_rty; - handle_exn : handle_exn_sty -> handle_exn_rty; - init : init_sty -> init_rty; - quit : quit_sty -> quit_rty; - (* for internal use (fake_id) only, do not use *) - wait : wait_sty -> wait_rty; - (* Retrocompatibility stuff *) - interp : interp_sty -> interp_rty; -} - diff --git a/ide/protocol/ideprotocol.mllib b/ide/protocol/ideprotocol.mllib new file mode 100644 index 000000000..8317a0868 --- /dev/null +++ b/ide/protocol/ideprotocol.mllib @@ -0,0 +1,7 @@ +Xml_lexer +Xml_parser +Xml_printer +Serialize +Richpp +Interface +Xmlprotocol diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml new file mode 100644 index 000000000..debbc8301 --- /dev/null +++ b/ide/protocol/interface.ml @@ -0,0 +1,261 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* add_rty; + edit_at : edit_at_sty -> edit_at_rty; + query : query_sty -> query_rty; + goals : goals_sty -> goals_rty; + evars : evars_sty -> evars_rty; + hints : hints_sty -> hints_rty; + status : status_sty -> status_rty; + search : search_sty -> search_rty; + get_options : get_options_sty -> get_options_rty; + set_options : set_options_sty -> set_options_rty; + mkcases : mkcases_sty -> mkcases_rty; + about : about_sty -> about_rty; + stop_worker : stop_worker_sty -> stop_worker_rty; + print_ast : print_ast_sty -> print_ast_rty; + annotate : annotate_sty -> annotate_rty; + handle_exn : handle_exn_sty -> handle_exn_rty; + init : init_sty -> init_rty; + quit : quit_sty -> quit_rty; + (* for internal use (fake_id) only, do not use *) + wait : wait_sty -> wait_rty; + (* Retrocompatibility stuff *) + interp : interp_sty -> interp_rty; +} + diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml new file mode 100644 index 000000000..19e9799c1 --- /dev/null +++ b/ide/protocol/richpp.ml @@ -0,0 +1,171 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* assert false + | Node (node, child, pos, ctx) -> + let data = Buffer.contents pp_buffer in + let () = Buffer.clear pp_buffer in + let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in + context.offset <- context.offset + len + in + + let open_xml_tag tag = + let () = push_pcdata () in + context.stack <- Node (tag, [], context.offset, context.stack) + in + + let close_xml_tag tag = + let () = push_pcdata () in + match context.stack with + | Leaf -> assert false + | Node (node, child, pos, ctx) -> + let () = assert (String.equal tag node) in + let annotation = { + annotation = Some tag; + startpos = pos; + endpos = context.offset; + } in + let xml = Element (node, annotation, List.rev child) in + match ctx with + | Leaf -> + (** Final node: we keep the result in a dummy context *) + context.stack <- Node ("", [xml], 0, Leaf) + | Node (node, child, pos, ctx) -> + context.stack <- Node (node, xml :: child, pos, ctx) + in + + let open Format in + + let ft = formatter_of_buffer pp_buffer in + + let tag_functions = { + mark_open_tag = (fun tag -> let () = open_xml_tag tag in ""); + mark_close_tag = (fun tag -> let () = close_xml_tag tag in ""); + print_open_tag = ignore; + print_close_tag = ignore; + } in + + pp_set_formatter_tag_functions ft tag_functions; + pp_set_mark_tags ft true; + + (* Setting the formatter *) + pp_set_margin ft width; + let m = max (64 * width / 100) (width-30) in + pp_set_max_indent ft m; + pp_set_max_boxes ft 50 ; + pp_set_ellipsis_text ft "..."; + + (** The whole output must be a valid document. To that + end, we nest the document inside tags. *) + pp_open_box ft 0; + pp_open_tag ft "pp"; + Pp.(pp_with ft ppcmds); + pp_close_tag ft (); + pp_close_box ft (); + + (** Get the resulting XML tree. *) + let () = pp_print_flush ft () in + let () = assert (Buffer.length pp_buffer = 0) in + match context.stack with + | Node ("", [xml], 0, Leaf) -> xml + | _ -> assert false + + +let annotations_positions xml = + let rec node accu = function + | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> + children ((annotation, (startpos, endpos)) :: accu) cs + | Element (_, _, cs) -> + children accu cs + | _ -> + accu + and children accu cs = + List.fold_left node accu cs + in + node [] xml + +let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = + let rec node = function + | Element (index, { annotation; startpos; endpos }, cs) -> + let attributes = + [ "startpos", string_of_int startpos; + "endpos", string_of_int endpos + ] + @ (match annotation with + | None -> [] + | Some annotation -> attributes_of_annotation annotation + ) + in + let tag = + match annotation with + | None -> index + | Some annotation -> tag_of_annotation annotation + in + Element (tag, attributes, List.map node cs) + | PCData s -> + PCData s + in + node xml + +type richpp = xml + +let richpp_of_pp width pp = + let rec drop = function + | PCData s -> [PCData s] + | Element (_, annotation, cs) -> + let cs = List.concat (List.map drop cs) in + match annotation.annotation with + | None -> cs + | Some s -> [Element (s, [], cs)] + in + let xml = rich_pp width pp in + Element ("_", [], drop xml) diff --git a/ide/protocol/richpp.mli b/ide/protocol/richpp.mli new file mode 100644 index 000000000..31fc7b56f --- /dev/null +++ b/ide/protocol/richpp.mli @@ -0,0 +1,53 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Pp.t -> Pp.pp_tag located Xml_datatype.gxml + +(** [annotations_positions ssdoc] returns a list associating each + annotations with its position in the string from which [ssdoc] is + built. *) +val annotations_positions : + 'annotation located Xml_datatype.gxml -> + ('annotation * (int * int)) list + +(** [xml_of_rich_pp ssdoc] returns an XML representation of the + semi-structured document [ssdoc]. *) +val xml_of_rich_pp : + ('annotation -> string) -> + ('annotation -> (string * string) list) -> + 'annotation located Xml_datatype.gxml -> + Xml_datatype.xml + +(** {5 Enriched text} *) + +type richpp = Xml_datatype.xml + +(** Type of text with style annotations *) + +val richpp_of_pp : int -> Pp.t -> richpp +(** Extract style information from formatted text *) diff --git a/ide/protocol/serialize.ml b/ide/protocol/serialize.ml new file mode 100644 index 000000000..86074d44d --- /dev/null +++ b/ide/protocol/serialize.ml @@ -0,0 +1,123 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* raise Not_found + | (k, v) :: l when CString.equal k attr -> v + | _ :: l -> get_attr attr l + +let massoc x l = + try get_attr x l + with Not_found -> raise (Marshal_error("attribute " ^ x,PCData "not there")) + +let constructor t c args = Element (t, ["val", c], args) +let do_match t mf = function + | Element (s, attrs, args) when CString.equal s t -> + let c = massoc "val" attrs in + mf c args + | x -> raise (Marshal_error (t,x)) + +let singleton = function + | [x] -> x + | l -> raise (Marshal_error + ("singleton",PCData ("list of length " ^ string_of_int (List.length l)))) + +let raw_string = function + | [] -> "" + | [PCData s] -> s + | x::_ -> raise (Marshal_error("raw string",x)) + +(** Base types *) + +let of_unit () = Element ("unit", [], []) +let to_unit : xml -> unit = function + | Element ("unit", [], []) -> () + | x -> raise (Marshal_error ("unit",x)) + +let of_bool (b : bool) : xml = + if b then constructor "bool" "true" [] + else constructor "bool" "false" [] +let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with + | "true" -> true + | "false" -> false + | x -> raise (Marshal_error("bool",PCData x))) + +let of_list (f : 'a -> xml) (l : 'a list) = + Element ("list", [], List.map f l) +let to_list (f : xml -> 'a) : xml -> 'a list = function + | Element ("list", [], l) -> List.map f l + | x -> raise (Marshal_error("list",x)) + +let of_option (f : 'a -> xml) : 'a option -> xml = function + | None -> Element ("option", ["val", "none"], []) + | Some x -> Element ("option", ["val", "some"], [f x]) +let to_option (f : xml -> 'a) : xml -> 'a option = function + | Element ("option", ["val", "none"], []) -> None + | Element ("option", ["val", "some"], [x]) -> Some (f x) + | x -> raise (Marshal_error("option",x)) + +let of_string (s : string) : xml = Element ("string", [], [PCData s]) +let to_string : xml -> string = function + | Element ("string", [], l) -> raw_string l + | x -> raise (Marshal_error("string",x)) + +let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)]) +let to_int : xml -> int = function + | Element ("int", [], [PCData s]) -> + (try int_of_string s with Failure _ -> raise(Marshal_error("int",PCData s))) + | x -> raise (Marshal_error("int",x)) + +let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml = + Element ("pair", [], [f (fst x); g (snd x)]) +let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function + | Element ("pair", [], [x; y]) -> (f x, g y) + | x -> raise (Marshal_error("pair",x)) + +let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function + | CSig.Inl x -> Element ("union", ["val","in_l"], [f x]) + | CSig.Inr x -> Element ("union", ["val","in_r"], [g x]) +let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function + | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x) + | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x) + | x -> raise (Marshal_error("union",x)) + +(** More elaborate types *) + +let of_edit_id i = Element ("edit_id",["val",string_of_int i],[]) +let to_edit_id = function + | Element ("edit_id",["val",i],[]) -> + let id = int_of_string i in + assert (id <= 0 ); + id + | x -> raise (Marshal_error("edit_id",x)) + +let of_loc loc = + let start, stop = Loc.unloc loc in + Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[]) +let to_loc xml = + match xml with + | Element ("loc", l,[]) -> + let start = massoc "start" l in + let stop = massoc "stop" l in + (try + Loc.make_loc (int_of_string start, int_of_string stop) + with Not_found | Invalid_argument _ -> raise (Marshal_error("loc",PCData(start^":"^stop)))) + | x -> raise (Marshal_error("loc",x)) + +let of_xml x = Element ("xml", [], [x]) +let to_xml xml = match xml with +| Element ("xml", [], [x]) -> x +| x -> raise (Marshal_error("xml",x)) diff --git a/ide/protocol/serialize.mli b/ide/protocol/serialize.mli new file mode 100644 index 000000000..af082f25b --- /dev/null +++ b/ide/protocol/serialize.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* (string * string) list -> string +val constructor: string -> string -> xml list -> xml +val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b +val singleton: 'a list -> 'a +val raw_string: xml list -> string +val of_unit: unit -> xml +val to_unit: xml -> unit +val of_bool: bool -> xml +val to_bool: xml -> bool +val of_list: ('a -> xml) -> 'a list -> xml +val to_list: (xml -> 'a) -> xml -> 'a list +val of_option: ('a -> xml) -> 'a option -> xml +val to_option: (xml -> 'a) -> xml -> 'a option +val of_string: string -> xml +val to_string: xml -> string +val of_int: int -> xml +val to_int: xml -> int +val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml +val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b +val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml +val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union +val of_edit_id: int -> xml +val to_edit_id: xml -> int +val of_loc : Loc.t -> xml +val to_loc : xml -> Loc.t +val of_xml : xml -> xml +val to_xml : xml -> xml diff --git a/ide/protocol/xml_lexer.mli b/ide/protocol/xml_lexer.mli new file mode 100644 index 000000000..e61cb055f --- /dev/null +++ b/ide/protocol/xml_lexer.mli @@ -0,0 +1,44 @@ +(* + * Xml Light, an small Xml parser/printer with DTD support. + * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) + * + * This library is free software; you can redistribute it and/or + * modify it under the terms of the GNU Lesser General Public + * License as published by the Free Software Foundation; either + * version 2.1 of the License, or (at your option) any later version. + * + * This library 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 + * Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public + * License along with this library; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + *) + +type error = + | EUnterminatedComment + | EUnterminatedString + | EIdentExpected + | ECloseExpected + | ENodeExpected + | EAttributeNameExpected + | EAttributeValueExpected + | EUnterminatedEntity + +exception Error of error + +type token = + | Tag of string * (string * string) list * bool + | PCData of string + | Endtag of string + | Eof + +type pos = int * int * int * int + +val init : Lexing.lexbuf -> unit +val close : unit -> unit +val token : Lexing.lexbuf -> token +val pos : Lexing.lexbuf -> pos +val restore : pos -> unit diff --git a/ide/protocol/xml_lexer.mll b/ide/protocol/xml_lexer.mll new file mode 100644 index 000000000..4a52147e1 --- /dev/null +++ b/ide/protocol/xml_lexer.mll @@ -0,0 +1,320 @@ +{(* + * Xml Light, an small Xml parser/printer with DTD support. + * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) + * + * This library is free software; you can redistribute it and/or + * modify it under the terms of the GNU Lesser General Public + * License as published by the Free Software Foundation; either + * version 2.1 of the License, or (at your option) any later version. + * + * This library 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 + * Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public + * License along with this library; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + *) + +open Lexing + +type error = + | EUnterminatedComment + | EUnterminatedString + | EIdentExpected + | ECloseExpected + | ENodeExpected + | EAttributeNameExpected + | EAttributeValueExpected + | EUnterminatedEntity + +exception Error of error + +type pos = int * int * int * int + +type token = + | Tag of string * (string * string) list * bool + | PCData of string + | Endtag of string + | Eof + +let last_pos = ref 0 +and current_line = ref 0 +and current_line_start = ref 0 + +let tmp = Buffer.create 200 + +let idents = Hashtbl.create 0 + +let _ = begin + Hashtbl.add idents "nbsp;" " "; + Hashtbl.add idents "gt;" ">"; + Hashtbl.add idents "lt;" "<"; + Hashtbl.add idents "amp;" "&"; + Hashtbl.add idents "apos;" "'"; + Hashtbl.add idents "quot;" "\""; +end + +let init lexbuf = + current_line := 1; + current_line_start := lexeme_start lexbuf; + last_pos := !current_line_start + +let close lexbuf = + Buffer.reset tmp + +let pos lexbuf = + !current_line , !current_line_start , + !last_pos , + lexeme_start lexbuf + +let restore (cl,cls,lp,_) = + current_line := cl; + current_line_start := cls; + last_pos := lp + +let newline lexbuf = + incr current_line; + last_pos := lexeme_end lexbuf; + current_line_start := !last_pos + +let error lexbuf e = + last_pos := lexeme_start lexbuf; + raise (Error e) + +[@@@ocaml.warning "-3"] (* String.lowercase_ascii since 4.03.0 GPR#124 *) +let lowercase = String.lowercase +[@@@ocaml.warning "+3"] +} + +let newline = ['\n'] +let break = ['\r'] +let space = [' ' '\t'] +let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.'] +let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar* +let entitychar = ['A'-'Z' 'a'-'z'] +let pcchar = [^ '\r' '\n' '<' '>' '&'] + +rule token = parse + | newline | (newline break) | break + { + newline lexbuf; + PCData "\n" + } + | "" + { () } + | eof + { raise (Error EUnterminatedComment) } + | _ + { comment lexbuf } + +and header = parse + | newline | (newline break) | break + { + newline lexbuf; + header lexbuf + } + | "?>" + { () } + | eof + { error lexbuf ECloseExpected } + | _ + { header lexbuf } + +and pcdata = parse + | newline | (newline break) | break + { + Buffer.add_char tmp '\n'; + newline lexbuf; + pcdata lexbuf + } + | pcchar+ + { + Buffer.add_string tmp (lexeme lexbuf); + pcdata lexbuf + } + | "&#" + { + Buffer.add_string tmp (lexeme lexbuf); + pcdata lexbuf; + } + | '&' + { + Buffer.add_string tmp (entity lexbuf); + pcdata lexbuf + } + | "" + { Buffer.contents tmp } + +and entity = parse + | entitychar+ ';' + { + let ident = lexeme lexbuf in + try + Hashtbl.find idents (lowercase ident) + with + Not_found -> "&" ^ ident + } + | _ | eof + { raise (Error EUnterminatedEntity) } + +and ident_name = parse + | ident + { lexeme lexbuf } + | _ | eof + { error lexbuf EIdentExpected } + +and close_tag = parse + | '>' + { () } + | _ | eof + { error lexbuf ECloseExpected } + +and attributes = parse + | '>' + { [], false } + | "/>" + { [], true } + | "" (* do not read a char ! *) + { + let key = attribute lexbuf in + let data = attribute_data lexbuf in + ignore_spaces lexbuf; + let others, closed = attributes lexbuf in + (key, data) :: others, closed + } + +and attribute = parse + | ident + { lexeme lexbuf } + | _ | eof + { error lexbuf EAttributeNameExpected } + +and attribute_data = parse + | space* '=' space* '"' + { + Buffer.reset tmp; + last_pos := lexeme_end lexbuf; + dq_string lexbuf + } + | space* '=' space* '\'' + { + Buffer.reset tmp; + last_pos := lexeme_end lexbuf; + q_string lexbuf + } + | _ | eof + { error lexbuf EAttributeValueExpected } + +and dq_string = parse + | '"' + { Buffer.contents tmp } + | '\\' [ '"' '\\' ] + { + Buffer.add_char tmp (lexeme_char lexbuf 1); + dq_string lexbuf + } + | '&' + { + Buffer.add_string tmp (entity lexbuf); + dq_string lexbuf + } + | eof + { raise (Error EUnterminatedString) } + | _ + { + Buffer.add_char tmp (lexeme_char lexbuf 0); + dq_string lexbuf + } + +and q_string = parse + | '\'' + { Buffer.contents tmp } + | '\\' [ '\'' '\\' ] + { + Buffer.add_char tmp (lexeme_char lexbuf 1); + q_string lexbuf + } + | '&' + { + Buffer.add_string tmp (entity lexbuf); + q_string lexbuf + } + | eof + { raise (Error EUnterminatedString) } + | _ + { + Buffer.add_char tmp (lexeme_char lexbuf 0); + q_string lexbuf + } diff --git a/ide/protocol/xml_parser.ml b/ide/protocol/xml_parser.ml new file mode 100644 index 000000000..8db3f9e8b --- /dev/null +++ b/ide/protocol/xml_parser.ml @@ -0,0 +1,232 @@ +(* + * Xml Light, an small Xml parser/printer with DTD support. + * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) + * Copyright (C) 2003 Jacques Garrigue + * + * This library is free software; you can redistribute it and/or + * modify it under the terms of the GNU Lesser General Public + * License as published by the Free Software Foundation; either + * version 2.1 of the License, or (at your option) any later version. + * + * This library 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 + * Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public + * License along with this library; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + *) + +open Printf +open Xml_datatype + +type xml = Xml_datatype.xml + +type error_pos = { + eline : int; + eline_start : int; + emin : int; + emax : int; +} + +type error_msg = + | UnterminatedComment + | UnterminatedString + | UnterminatedEntity + | IdentExpected + | CloseExpected + | NodeExpected + | AttributeNameExpected + | AttributeValueExpected + | EndOfTagExpected of string + | EOFExpected + | Empty + +type error = error_msg * error_pos + +exception Error of error + +exception File_not_found of string + +type t = { + mutable check_eof : bool; + mutable concat_pcdata : bool; + source : Lexing.lexbuf; + stack : Xml_lexer.token Stack.t; +} + +type source = + | SChannel of in_channel + | SString of string + | SLexbuf of Lexing.lexbuf + +exception Internal_error of error_msg +exception NoMoreData + +let xml_error = ref (fun _ -> assert false) +let file_not_found = ref (fun _ -> assert false) + +let is_blank s = + let len = String.length s in + let break = ref true in + let i = ref 0 in + while !break && !i < len do + let c = s.[!i] in + (* no '\r' because we replaced them in the lexer *) + if c = ' ' || c = '\n' || c = '\t' then incr i + else break := false + done; + !i = len + +let _raises e f = + xml_error := e; + file_not_found := f + +let make source = + let source = match source with + | SChannel chan -> Lexing.from_channel chan + | SString s -> Lexing.from_string s + | SLexbuf lexbuf -> lexbuf + in + let () = Xml_lexer.init source in + { + check_eof = false; + concat_pcdata = true; + source = source; + stack = Stack.create (); + } + +let check_eof p v = p.check_eof <- v + +let pop s = + try + Stack.pop s.stack + with + Stack.Empty -> + Xml_lexer.token s.source + +let push t s = + Stack.push t s.stack + +let canonicalize l = + let has_elt = List.exists (function Element _ -> true | _ -> false) l in + if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l + else l + +let rec read_xml do_not_canonicalize s = + let rec read_node s = + match pop s with + | Xml_lexer.PCData s -> PCData s + | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, []) + | Xml_lexer.Tag (tag, attr, false) -> + let elements = read_elems tag s in + let elements = + if do_not_canonicalize then elements else canonicalize elements + in + Element (tag, attr, elements) + | t -> + push t s; + raise NoMoreData + + and read_elems tag s = + let elems = ref [] in + (try + while true do + let node = read_node s in + match node, !elems with + | PCData c , (PCData c2) :: q -> + elems := PCData (c2 ^ c) :: q + | _, l -> + elems := node :: l + done + with + NoMoreData -> ()); + match pop s with + | Xml_lexer.Endtag s when s = tag -> List.rev !elems + | t -> raise (Internal_error (EndOfTagExpected tag)) + in + match read_node s with + | (Element _) as node -> + node + | PCData c -> + if is_blank c then + read_xml do_not_canonicalize s + else + raise (Xml_lexer.Error Xml_lexer.ENodeExpected) + +let convert = function + | Xml_lexer.EUnterminatedComment -> UnterminatedComment + | Xml_lexer.EUnterminatedString -> UnterminatedString + | Xml_lexer.EIdentExpected -> IdentExpected + | Xml_lexer.ECloseExpected -> CloseExpected + | Xml_lexer.ENodeExpected -> NodeExpected + | Xml_lexer.EAttributeNameExpected -> AttributeNameExpected + | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected + | Xml_lexer.EUnterminatedEntity -> UnterminatedEntity + +let error_of_exn xparser = function + | NoMoreData when pop xparser = Xml_lexer.Eof -> Empty + | NoMoreData -> NodeExpected + | Internal_error e -> e + | Xml_lexer.Error e -> convert e + | e -> + (*let e = Errors.push e in: We do not record backtrace here. *) + raise e + +let do_parse do_not_canonicalize xparser = + try + Xml_lexer.init xparser.source; + let x = read_xml do_not_canonicalize xparser in + if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected); + Xml_lexer.close (); + x + with any -> + Xml_lexer.close (); + raise (!xml_error (error_of_exn xparser any) xparser.source) + +let parse ?(do_not_canonicalize=false) p = + do_parse do_not_canonicalize p + +let error_msg = function + | UnterminatedComment -> "Unterminated comment" + | UnterminatedString -> "Unterminated string" + | UnterminatedEntity -> "Unterminated entity" + | IdentExpected -> "Ident expected" + | CloseExpected -> "Element close expected" + | NodeExpected -> "Xml node expected" + | AttributeNameExpected -> "Attribute name expected" + | AttributeValueExpected -> "Attribute value expected" + | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag + | EOFExpected -> "End of file expected" + | Empty -> "Empty" + +let error (msg,pos) = + if pos.emin = pos.emax then + sprintf "%s line %d character %d" (error_msg msg) pos.eline + (pos.emin - pos.eline_start) + else + sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline + (pos.emin - pos.eline_start) (pos.emax - pos.eline_start) + +let line e = e.eline + +let range e = + e.emin - e.eline_start , e.emax - e.eline_start + +let abs_range e = + e.emin , e.emax + +let pos source = + let line, lstart, min, max = Xml_lexer.pos source in + { + eline = line; + eline_start = lstart; + emin = min; + emax = max; + } + +let () = _raises (fun x p -> + (* local cast : Xml.error_msg -> error_msg *) + Error (x, pos p)) + (fun f -> File_not_found f) diff --git a/ide/protocol/xml_parser.mli b/ide/protocol/xml_parser.mli new file mode 100644 index 000000000..ac2eab352 --- /dev/null +++ b/ide/protocol/xml_parser.mli @@ -0,0 +1,106 @@ +(* + * Xml Light, an small Xml parser/printer with DTD support. + * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) + * + * This library is free software; you can redistribute it and/or + * modify it under the terms of the GNU Lesser General Public + * License as published by the Free Software Foundation; either + * version 2.1 of the License, or (at your option) any later version. + * + * This library 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 + * Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public + * License along with this library; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + *) + +(** Xml Light Parser + + While basic parsing functions can be used in the {!Xml} module, this module + is providing a way to create, configure and run an Xml parser. + +*) + + +(** An Xml node is either + [Element (tag-name, attributes, children)] or [PCData text] *) +type xml = Xml_datatype.xml + +(** Abstract type for an Xml parser. *) +type t + +(** {6:exc Xml Exceptions} *) + +(** Several exceptions can be raised when parsing an Xml document : {ul + {li {!Xml.Error} is raised when an xml parsing error occurs. the + {!Xml.error_msg} tells you which error occurred during parsing + and the {!Xml.error_pos} can be used to retrieve the document + location where the error occurred at.} + {li {!Xml.File_not_found} is raised when an error occurred while + opening a file with the {!Xml.parse_file} function.} + } + *) + +type error_pos + +type error_msg = + | UnterminatedComment + | UnterminatedString + | UnterminatedEntity + | IdentExpected + | CloseExpected + | NodeExpected + | AttributeNameExpected + | AttributeValueExpected + | EndOfTagExpected of string + | EOFExpected + | Empty + +type error = error_msg * error_pos + +exception Error of error + +exception File_not_found of string + +(** Get a full error message from an Xml error. *) +val error : error -> string + +(** Get the Xml error message as a string. *) +val error_msg : error_msg -> string + +(** Get the line the error occurred at. *) +val line : error_pos -> int + +(** Get the relative character range (in current line) the error occurred at.*) +val range : error_pos -> int * int + +(** Get the absolute character range the error occurred at. *) +val abs_range : error_pos -> int * int + +val pos : Lexing.lexbuf -> error_pos + +(** Several kind of resources can contain Xml documents. *) +type source = +| SChannel of in_channel +| SString of string +| SLexbuf of Lexing.lexbuf + +(** This function returns a new parser with default options. *) +val make : source -> t + +(** When a Xml document is parsed, the parser may check that the end of the + document is reached, so for example parsing [""] will fail instead + of returning only the A element. You can turn on this check by setting + [check_eof] to [true] {i (by default, check_eof is false, unlike + in the original Xmllight)}. *) +val check_eof : t -> bool -> unit + +(** Once the parser is configured, you can run the parser on a any kind + of xml document source to parse its contents into an Xml data structure. + + When [do_not_canonicalize] is set, the XML document is given as + is, without trying to remove blank PCDATA elements. *) +val parse : ?do_not_canonicalize:bool -> t -> xml diff --git a/ide/protocol/xml_printer.ml b/ide/protocol/xml_printer.ml new file mode 100644 index 000000000..488ef7bf5 --- /dev/null +++ b/ide/protocol/xml_printer.ml @@ -0,0 +1,147 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* puts " "; + | '>' -> puts ">" + | '<' -> puts "<" + | '&' -> + if p < l - 1 && text.[p + 1] = '#' then + putc '&' + else + puts "&" + | '\'' -> puts "'" + | '"' -> puts """ + | c -> putc c + done + +let buffer_attr tmp (n,v) = + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in + putc ' '; + puts n; + puts "=\""; + let l = String.length v in + for p = 0 to l - 1 do + match v.[p] with + | '\\' -> puts "\\\\" + | '"' -> puts "\\\"" + | '<' -> puts "<" + | '&' -> puts "&" + | c -> putc c + done; + putc '"' + +let to_buffer tmp x = + let pcdata = ref false in + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in + let rec loop = function + | Element (tag,alist,[]) -> + putc '<'; + puts tag; + List.iter (buffer_attr tmp) alist; + puts "/>"; + pcdata := false; + | Element (tag,alist,l) -> + putc '<'; + puts tag; + List.iter (buffer_attr tmp) alist; + putc '>'; + pcdata := false; + List.iter loop l; + puts "'; + pcdata := false; + | PCData text -> + if !pcdata then putc ' '; + buffer_pcdata tmp text; + pcdata := true; + in + loop x + +let pcdata_to_string s = + let b = Buffer.create 13 in + buffer_pcdata b s; + Buffer.contents b + +let to_string x = + let b = Buffer.create 200 in + to_buffer b x; + Buffer.contents b + +let to_string_fmt x = + let tmp = Buffer.create 200 in + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in + let rec loop ?(newl=false) tab = function + | Element (tag, alist, []) -> + puts tab; + putc '<'; + puts tag; + List.iter (buffer_attr tmp) alist; + puts "/>"; + if newl then putc '\n'; + | Element (tag, alist, [PCData text]) -> + puts tab; + putc '<'; + puts tag; + List.iter (buffer_attr tmp) alist; + puts ">"; + buffer_pcdata tmp text; + puts "'; + if newl then putc '\n'; + | Element (tag, alist, l) -> + puts tab; + putc '<'; + puts tag; + List.iter (buffer_attr tmp) alist; + puts ">\n"; + List.iter (loop ~newl:true (tab^" ")) l; + puts tab; + puts "'; + if newl then putc '\n'; + | PCData text -> + buffer_pcdata tmp text; + if newl then putc '\n'; + in + loop "" x; + Buffer.contents tmp + +let print t xml = + let tmp, flush = match t with + | TChannel oc -> + let b = Buffer.create 200 in + b, (fun () -> Buffer.output_buffer oc b; flush oc) + | TBuffer b -> + b, (fun () -> ()) + in + to_buffer tmp xml; + flush () diff --git a/ide/protocol/xml_printer.mli b/ide/protocol/xml_printer.mli new file mode 100644 index 000000000..178f7c808 --- /dev/null +++ b/ide/protocol/xml_printer.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* t + +(** Print the xml data structure to a source into a compact xml string (without + any user-readable formating ). *) +val print : t -> xml -> unit + +(** Print the xml data structure into a compact xml string (without + any user-readable formating ). *) +val to_string : xml -> string + +(** Print the xml data structure into an user-readable string with + tabs and lines break between different nodes. *) +val to_string_fmt : xml -> string + +(** Print PCDATA as a string by escaping XML entities. *) +val pcdata_to_string : string -> string diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml new file mode 100644 index 000000000..e18219210 --- /dev/null +++ b/ide/protocol/xmlprotocol.ml @@ -0,0 +1,964 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + constructor "search_cst" "name_pattern" [of_string s] + | Type_Pattern s -> + constructor "search_cst" "type_pattern" [of_string s] + | SubType_Pattern s -> + constructor "search_cst" "subtype_pattern" [of_string s] + | In_Module m -> + constructor "search_cst" "in_module" [of_list of_string m] + | Include_Blacklist -> + constructor "search_cst" "include_blacklist" [] +let to_search_cst = do_match "search_cst" (fun s args -> match s with + | "name_pattern" -> Name_Pattern (to_string (singleton args)) + | "type_pattern" -> Type_Pattern (to_string (singleton args)) + | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) + | "in_module" -> In_Module (to_list to_string (singleton args)) + | "include_blacklist" -> Include_Blacklist + | x -> raise (Marshal_error("search",PCData x))) + +let of_coq_object f ans = + let prefix = of_list of_string ans.coq_object_prefix in + let qualid = of_list of_string ans.coq_object_qualid in + let obj = f ans.coq_object_object in + Element ("coq_object", [], [prefix; qualid; obj]) + +let to_coq_object f = function +| Element ("coq_object", [], [prefix; qualid; obj]) -> + let prefix = to_list to_string prefix in + let qualid = to_list to_string qualid in + let obj = f obj in { + coq_object_prefix = prefix; + coq_object_qualid = qualid; + coq_object_object = obj; + } +| x -> raise (Marshal_error("coq_object",x)) + +let of_option_value = function + | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i] + | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b] + | StringValue s -> constructor "option_value" "stringvalue" [of_string s] + | StringOptValue s -> constructor "option_value" "stringoptvalue" [of_option of_string s] +let to_option_value = do_match "option_value" (fun s args -> match s with + | "intvalue" -> IntValue (to_option to_int (singleton args)) + | "boolvalue" -> BoolValue (to_bool (singleton args)) + | "stringvalue" -> StringValue (to_string (singleton args)) + | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args)) + | x -> raise (Marshal_error("*value",PCData x))) + +let of_option_state s = + Element ("option_state", [], [ + of_bool s.opt_sync; + of_bool s.opt_depr; + of_string s.opt_name; + of_option_value s.opt_value]) +let to_option_state = function + | Element ("option_state", [], [sync; depr; name; value]) -> { + opt_sync = to_bool sync; + opt_depr = to_bool depr; + opt_name = to_string name; + opt_value = to_option_value value } + | x -> raise (Marshal_error("option_state",x)) + +let to_stateid = function + | Element ("state_id",["val",i],[]) -> + let id = int_of_string i in + Stateid.of_int id + | _ -> raise (Invalid_argument "to_state_id") + +let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[]) + +let to_routeid = function + | Element ("route_id",["val",i],[]) -> + let id = int_of_string i in id + | _ -> raise (Invalid_argument "to_route_id") + +let of_routeid i = Element ("route_id",["val",string_of_int i],[]) + +let of_box (ppb : Pp.block_type) = let open Pp in match ppb with + | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] + | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] + | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] + | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] + +let to_box = let open Pp in + do_match "ppbox" (fun s args -> match s with + | "hbox" -> Pp_hbox (to_int (singleton args)) + | "vbox" -> Pp_vbox (to_int (singleton args)) + | "hvbox" -> Pp_hvbox (to_int (singleton args)) + | "hovbox" -> Pp_hovbox (to_int (singleton args)) + | x -> raise (Marshal_error("*ppbox",PCData x)) + ) + +let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with + | Ppcmd_empty -> constructor "ppdoc" "empty" [] + | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] + | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] + | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] + | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair of_string of_pp (t,s)] + | Ppcmd_print_break (i,j) + -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] + | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] + | Ppcmd_comment cmd -> constructor "ppdoc" "comment" [of_list of_string cmd] + + +let rec to_pp xpp = let open Pp in + Pp.unrepr @@ + do_match "ppdoc" (fun s args -> match s with + | "empty" -> Ppcmd_empty + | "string" -> Ppcmd_string (to_string (singleton args)) + | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) + | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in + Ppcmd_box(bt,s) + | "tag" -> let (tg,s) = to_pair to_string to_pp (singleton args) in + Ppcmd_tag(tg,s) + | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in + Ppcmd_print_break(i, j) + | "newline" -> Ppcmd_force_newline + | "comment" -> Ppcmd_comment (to_list to_string (singleton args)) + | x -> raise (Marshal_error("*ppdoc",PCData x)) + ) xpp + +let of_richpp x = Element ("richpp", [], [x]) + +(* Run-time Selectable *) +let of_pp (pp : Pp.t) = + match !msg_format with + | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) + | Ppcmds -> of_pp pp + +let of_value f = function +| Good x -> Element ("value", ["val", "good"], [f x]) +| Fail (id,loc, msg) -> + let loc = match loc with + | None -> [] + | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in + let id = of_stateid id in + Element ("value", ["val", "fail"] @ loc, [id; of_pp msg]) + +let to_value f = function +| Element ("value", attrs, l) -> + let ans = massoc "val" attrs in + if ans = "good" then Good (f (singleton l)) + else if ans = "fail" then + let loc = + try + let loc_s = int_of_string (Serialize.massoc "loc_s" attrs) in + let loc_e = int_of_string (Serialize.massoc "loc_e" attrs) in + Some (loc_s, loc_e) + with Marshal_error _ | Failure _ -> None + in + let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in + let id = to_stateid id in + let msg = to_pp msg in + Fail (id, loc, msg) + else raise (Marshal_error("good or fail",PCData ans)) +| x -> raise (Marshal_error("value",x)) + +let of_status s = + let of_so = of_option of_string in + let of_sl = of_list of_string in + Element ("status", [], [ + of_sl s.status_path; + of_so s.status_proofname; + of_sl s.status_allproofs; + of_int s.status_proofnum; ]) +let to_status = function + | Element ("status", [], [path; name; prfs; pnum]) -> { + status_path = to_list to_string path; + status_proofname = to_option to_string name; + status_allproofs = to_list to_string prfs; + status_proofnum = to_int pnum; } + | x -> raise (Marshal_error("status",x)) + +let of_evar s = Element ("evar", [], [PCData s.evar_info]) +let to_evar = function + | Element ("evar", [], data) -> { evar_info = raw_string data; } + | x -> raise (Marshal_error("evar",x)) + +let of_goal g = + let hyp = of_list of_pp g.goal_hyp in + let ccl = of_pp g.goal_ccl in + let id = of_string g.goal_id in + Element ("goal", [], [id; hyp; ccl]) +let to_goal = function + | Element ("goal", [], [id; hyp; ccl]) -> + let hyp = to_list to_pp hyp in + let ccl = to_pp ccl in + let id = to_string id in + { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } + | x -> raise (Marshal_error("goal",x)) + +let of_goals g = + let of_glist = of_list of_goal in + let fg = of_list of_goal g.fg_goals in + let bg = of_list (of_pair of_glist of_glist) g.bg_goals in + let shelf = of_list of_goal g.shelved_goals in + let given_up = of_list of_goal g.given_up_goals in + Element ("goals", [], [fg; bg; shelf; given_up]) +let to_goals = function + | Element ("goals", [], [fg; bg; shelf; given_up]) -> + let to_glist = to_list to_goal in + let fg = to_list to_goal fg in + let bg = to_list (to_pair to_glist to_glist) bg in + let shelf = to_list to_goal shelf in + let given_up = to_list to_goal given_up in + { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; + given_up_goals = given_up } + | x -> raise (Marshal_error("goals",x)) + +let of_coq_info info = + let version = of_string info.coqtop_version in + let protocol = of_string info.protocol_version in + let release = of_string info.release_date in + let compile = of_string info.compile_date in + Element ("coq_info", [], [version; protocol; release; compile]) +let to_coq_info = function + | Element ("coq_info", [], [version; protocol; release; compile]) -> { + coqtop_version = to_string version; + protocol_version = to_string protocol; + release_date = to_string release; + compile_date = to_string compile; } + | x -> raise (Marshal_error("coq_info",x)) + +end +include Xml_marshalling + +(* Reification of basic types and type constructors, and functions + from to xml *) +module ReifType : sig + + type 'a val_t + + val unit_t : unit val_t + val string_t : string val_t + val int_t : int val_t + val bool_t : bool val_t + val xml_t : Xml_datatype.xml val_t + + val option_t : 'a val_t -> 'a option val_t + val list_t : 'a val_t -> 'a list val_t + val pair_t : 'a val_t -> 'b val_t -> ('a * 'b) val_t + val union_t : 'a val_t -> 'b val_t -> ('a ,'b) union val_t + + val goals_t : goals val_t + val evar_t : evar val_t + val state_t : status val_t + val option_state_t : option_state val_t + val option_value_t : option_value val_t + val coq_info_t : coq_info val_t + val coq_object_t : 'a val_t -> 'a coq_object val_t + val state_id_t : state_id val_t + val route_id_t : route_id val_t + val search_cst_t : search_constraint val_t + + val of_value_type : 'a val_t -> 'a -> xml + val to_value_type : 'a val_t -> xml -> 'a + + val print : 'a val_t -> 'a -> string + + type value_type + val erase : 'a val_t -> value_type + val print_type : value_type -> string + + val document_type_encoding : (xml -> string) -> unit + +end = struct + + type _ val_t = + | Unit : unit val_t + | String : string val_t + | Int : int val_t + | Bool : bool val_t + | Xml : Xml_datatype.xml val_t + + | Option : 'a val_t -> 'a option val_t + | List : 'a val_t -> 'a list val_t + | Pair : 'a val_t * 'b val_t -> ('a * 'b) val_t + | Union : 'a val_t * 'b val_t -> ('a, 'b) union val_t + + | Goals : goals val_t + | Evar : evar val_t + | State : status val_t + | Option_state : option_state val_t + | Option_value : option_value val_t + | Coq_info : coq_info val_t + | Coq_object : 'a val_t -> 'a coq_object val_t + | State_id : state_id val_t + | Route_id : route_id val_t + | Search_cst : search_constraint val_t + + type value_type = Value_type : 'a val_t -> value_type + + let erase (x : 'a val_t) = Value_type x + + let unit_t = Unit + let string_t = String + let int_t = Int + let bool_t = Bool + let xml_t = Xml + + let option_t x = Option x + let list_t x = List x + let pair_t x y = Pair (x, y) + let union_t x y = Union (x, y) + + let goals_t = Goals + let evar_t = Evar + let state_t = State + let option_state_t = Option_state + let option_value_t = Option_value + let coq_info_t = Coq_info + let coq_object_t x = Coq_object x + let state_id_t = State_id + let route_id_t = Route_id + let search_cst_t = Search_cst + + let of_value_type (ty : 'a val_t) : 'a -> xml = + let rec convert : type a. a val_t -> a -> xml = function + | Unit -> of_unit + | Bool -> of_bool + | Xml -> (fun x -> x) + | String -> of_string + | Int -> of_int + | State -> of_status + | Option_state -> of_option_state + | Option_value -> of_option_value + | Coq_info -> of_coq_info + | Goals -> of_goals + | Evar -> of_evar + | List t -> (of_list (convert t)) + | Option t -> (of_option (convert t)) + | Coq_object t -> (of_coq_object (convert t)) + | Pair (t1,t2) -> (of_pair (convert t1) (convert t2)) + | Union (t1,t2) -> (of_union (convert t1) (convert t2)) + | State_id -> of_stateid + | Route_id -> of_routeid + | Search_cst -> of_search_cst + in + convert ty + + let to_value_type (ty : 'a val_t) : xml -> 'a = + let rec convert : type a. a val_t -> xml -> a = function + | Unit -> to_unit + | Bool -> to_bool + | Xml -> (fun x -> x) + | String -> to_string + | Int -> to_int + | State -> to_status + | Option_state -> to_option_state + | Option_value -> to_option_value + | Coq_info -> to_coq_info + | Goals -> to_goals + | Evar -> to_evar + | List t -> (to_list (convert t)) + | Option t -> (to_option (convert t)) + | Coq_object t -> (to_coq_object (convert t)) + | Pair (t1,t2) -> (to_pair (convert t1) (convert t2)) + | Union (t1,t2) -> (to_union (convert t1) (convert t2)) + | State_id -> to_stateid + | Route_id -> to_routeid + | Search_cst -> to_search_cst + in + convert ty + + let pr_unit () = "" + let pr_string s = Printf.sprintf "%S" s + let pr_int i = string_of_int i + let pr_bool b = Printf.sprintf "%B" b + let pr_goal (g : goals) = + if g.fg_goals = [] then + if g.bg_goals = [] then "Proof completed." + else + let rec pr_focus _ = function + | [] -> assert false + | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) + | (lg, rg) :: l -> + Printf.sprintf "%i:%a" + (List.length lg + List.length rg) pr_focus l in + Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals + else + let pr_goal { goal_hyp = hyps; goal_ccl = goal } = + "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ + Pp.string_of_ppcmds goal ^ "]" in + String.concat " " (List.map pr_goal g.fg_goals) + let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" + let pr_status (s : status) = + let path = + let l = String.concat "." s.status_path in + "path=" ^ l ^ ";" in + let name = match s.status_proofname with + | None -> "no proof;" + | Some n -> "proof = " ^ n ^ ";" in + "Status: " ^ path ^ name + let pr_coq_info (i : coq_info) = "FIXME" + let pr_option_value = function + | IntValue None -> "none" + | IntValue (Some i) -> string_of_int i + | StringValue s -> s + | StringOptValue None -> "none" + | StringOptValue (Some s) -> s + | BoolValue b -> if b then "true" else "false" + let pr_option_state (s : option_state) = + Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" + s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) + let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]" + let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")" + let pr_coq_object (o : 'a coq_object) = "FIXME" + let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")" + let pr_union pr1 pr2 = function Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x + let pr_state_id = Stateid.to_string + + let pr_search_cst = function + | Name_Pattern s -> "Name_Pattern " ^ s + | Type_Pattern s -> "Type_Pattern " ^ s + | SubType_Pattern s -> "SubType_Pattern " ^ s + | In_Module s -> "In_Module " ^ String.concat "." s + | Include_Blacklist -> "Include_Blacklist" + + let rec print : type a. a val_t -> a -> string = function + | Unit -> pr_unit + | Bool -> pr_bool + | String -> pr_string + | Xml -> Xml_printer.to_string_fmt + | Int -> pr_int + | State -> pr_status + | Option_state -> pr_option_state + | Option_value -> pr_option_value + | Search_cst -> pr_search_cst + | Coq_info -> pr_coq_info + | Goals -> pr_goal + | Evar -> pr_evar + | List t -> (pr_list (print t)) + | Option t -> (pr_option (print t)) + | Coq_object t -> pr_coq_object + | Pair (t1,t2) -> (pr_pair (print t1) (print t2)) + | Union (t1,t2) -> (pr_union (print t1) (print t2)) + | State_id -> pr_state_id + | Route_id -> pr_int + + (* This is to break if a rename/refactoring makes the strings below outdated *) + type 'a exists = bool + + let rec print_val_t : type a. a val_t -> string = function + | Unit -> "unit" + | Bool -> "bool" + | String -> "string" + | Xml -> "xml" + | Int -> "int" + | State -> assert(true : status exists); "Interface.status" + | Option_state -> assert(true : option_state exists); "Interface.option_state" + | Option_value -> assert(true : option_value exists); "Interface.option_value" + | Search_cst -> assert(true : search_constraint exists); "Interface.search_constraint" + | Coq_info -> assert(true : coq_info exists); "Interface.coq_info" + | Goals -> assert(true : goals exists); "Interface.goals" + | Evar -> assert(true : evar exists); "Interface.evar" + | List t -> Printf.sprintf "(%s list)" (print_val_t t) + | Option t -> Printf.sprintf "(%s option)" (print_val_t t) + | Coq_object t -> assert(true : 'a coq_object exists); + Printf.sprintf "(%s Interface.coq_object)" (print_val_t t) + | Pair (t1,t2) -> Printf.sprintf "(%s * %s)" (print_val_t t1) (print_val_t t2) + | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); + Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2) + | State_id -> assert(true : Stateid.t exists); "Stateid.t" + | Route_id -> assert(true : route_id exists); "route_id" + + let print_type = function Value_type ty -> print_val_t ty + + let document_type_encoding pr_xml = + Printf.printf "\n=== Data encoding by examples ===\n\n"; + Printf.printf "%s:\n\n%s\n\n" (print_val_t Unit) (pr_xml (of_unit ())); + Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t Bool) + (pr_xml (of_bool true)) (pr_xml (of_bool false)); + Printf.printf "%s:\n\n%s\n\n" (print_val_t String) (pr_xml (of_string "hello")); + Printf.printf "%s:\n\n%s\n\n" (print_val_t Int) (pr_xml (of_int 256)); + Printf.printf "%s:\n\n%s\n\n" (print_val_t State_id) (pr_xml (of_stateid Stateid.initial)); + Printf.printf "%s:\n\n%s\n\n" (print_val_t (List Int)) (pr_xml (of_list of_int [3;4;5])); + Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t (Option Int)) + (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None)); + Printf.printf "%s:\n\n%s\n\n" (print_val_t (Pair (Bool,Int))) + (pr_xml (of_pair of_bool of_int (false,3))); + Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int))) + (pr_xml (of_union of_bool of_int (Inl false))); + print_endline ("All other types are records represented by a node named like the OCaml\n"^ + "type which contains a flattened n-tuple. We provide one example.\n"); + Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) + (pr_xml (of_option_state { opt_sync = true; opt_depr = false; + opt_name = "name1"; opt_value = IntValue (Some 37) })); + +end +open ReifType + +(** Types reification, checked with explicit casts *) +let add_sty_t : add_sty val_t = + pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t) +let edit_at_sty_t : edit_at_sty val_t = state_id_t +let query_sty_t : query_sty val_t = pair_t route_id_t (pair_t string_t state_id_t) +let goals_sty_t : goals_sty val_t = unit_t +let evars_sty_t : evars_sty val_t = unit_t +let hints_sty_t : hints_sty val_t = unit_t +let status_sty_t : status_sty val_t = bool_t +let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t) +let get_options_sty_t : get_options_sty val_t = unit_t +let set_options_sty_t : set_options_sty val_t = + list_t (pair_t (list_t string_t) option_value_t) +let mkcases_sty_t : mkcases_sty val_t = string_t +let quit_sty_t : quit_sty val_t = unit_t +let wait_sty_t : wait_sty val_t = unit_t +let about_sty_t : about_sty val_t = unit_t +let init_sty_t : init_sty val_t = option_t string_t +let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t +let stop_worker_sty_t : stop_worker_sty val_t = string_t +let print_ast_sty_t : print_ast_sty val_t = state_id_t +let annotate_sty_t : annotate_sty val_t = string_t + +let add_rty_t : add_rty val_t = + pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) +let edit_at_rty_t : edit_at_rty val_t = + union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t)) +let query_rty_t : query_rty val_t = unit_t +let goals_rty_t : goals_rty val_t = option_t goals_t +let evars_rty_t : evars_rty val_t = option_t (list_t evar_t) +let hints_rty_t : hints_rty val_t = + let hint = list_t (pair_t string_t string_t) in + option_t (pair_t (list_t hint) hint) +let status_rty_t : status_rty val_t = state_t +let search_rty_t : search_rty val_t = list_t (coq_object_t string_t) +let get_options_rty_t : get_options_rty val_t = + list_t (pair_t (list_t string_t) option_state_t) +let set_options_rty_t : set_options_rty val_t = unit_t +let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t) +let quit_rty_t : quit_rty val_t = unit_t +let wait_rty_t : wait_rty val_t = unit_t +let about_rty_t : about_rty val_t = coq_info_t +let init_rty_t : init_rty val_t = state_id_t +let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t) +let stop_worker_rty_t : stop_worker_rty val_t = unit_t +let print_ast_rty_t : print_ast_rty val_t = xml_t +let annotate_rty_t : annotate_rty val_t = xml_t + +let ($) x = erase x +let calls = [| + "Add", ($)add_sty_t, ($)add_rty_t; + "Edit_at", ($)edit_at_sty_t, ($)edit_at_rty_t; + "Query", ($)query_sty_t, ($)query_rty_t; + "Goal", ($)goals_sty_t, ($)goals_rty_t; + "Evars", ($)evars_sty_t, ($)evars_rty_t; + "Hints", ($)hints_sty_t, ($)hints_rty_t; + "Status", ($)status_sty_t, ($)status_rty_t; + "Search", ($)search_sty_t, ($)search_rty_t; + "GetOptions", ($)get_options_sty_t, ($)get_options_rty_t; + "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t; + "MkCases", ($)mkcases_sty_t, ($)mkcases_rty_t; + "Quit", ($)quit_sty_t, ($)quit_rty_t; + "Wait", ($)wait_sty_t, ($)wait_rty_t; + "About", ($)about_sty_t, ($)about_rty_t; + "Init", ($)init_sty_t, ($)init_rty_t; + "Interp", ($)interp_sty_t, ($)interp_rty_t; + "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t; + "PrintAst", ($)print_ast_sty_t, ($)print_ast_rty_t; + "Annotate", ($)annotate_sty_t, ($)annotate_rty_t; +|] + +type 'a call = + | Add : add_sty -> add_rty call + | Edit_at : edit_at_sty -> edit_at_rty call + | Query : query_sty -> query_rty call + | Goal : goals_sty -> goals_rty call + | Evars : evars_sty -> evars_rty call + | Hints : hints_sty -> hints_rty call + | Status : status_sty -> status_rty call + | Search : search_sty -> search_rty call + | GetOptions : get_options_sty -> get_options_rty call + | SetOptions : set_options_sty -> set_options_rty call + | MkCases : mkcases_sty -> mkcases_rty call + | Quit : quit_sty -> quit_rty call + | About : about_sty -> about_rty call + | Init : init_sty -> init_rty call + | StopWorker : stop_worker_sty -> stop_worker_rty call + (* internal use (fake_ide) only, do not use *) + | Wait : wait_sty -> wait_rty call + (* retrocompatibility *) + | Interp : interp_sty -> interp_rty call + | PrintAst : print_ast_sty -> print_ast_rty call + | Annotate : annotate_sty -> annotate_rty call + +let id_of_call : type a. a call -> int = function + | Add _ -> 0 + | Edit_at _ -> 1 + | Query _ -> 2 + | Goal _ -> 3 + | Evars _ -> 4 + | Hints _ -> 5 + | Status _ -> 6 + | Search _ -> 7 + | GetOptions _ -> 8 + | SetOptions _ -> 9 + | MkCases _ -> 10 + | Quit _ -> 11 + | Wait _ -> 12 + | About _ -> 13 + | Init _ -> 14 + | Interp _ -> 15 + | StopWorker _ -> 16 + | PrintAst _ -> 17 + | Annotate _ -> 18 + +let str_of_call c = pi1 calls.(id_of_call c) + +type unknown_call = Unknown : 'a call -> unknown_call + +(** We use phantom types and GADT to protect ourselves against wild casts *) +let add x : add_rty call = Add x +let edit_at x : edit_at_rty call = Edit_at x +let query x : query_rty call = Query x +let goals x : goals_rty call = Goal x +let evars x : evars_rty call = Evars x +let hints x : hints_rty call = Hints x +let status x : status_rty call = Status x +let get_options x : get_options_rty call = GetOptions x +let set_options x : set_options_rty call = SetOptions x +let mkcases x : mkcases_rty call = MkCases x +let search x : search_rty call = Search x +let quit x : quit_rty call = Quit x +let init x : init_rty call = Init x +let wait x : wait_rty call = Wait x +let interp x : interp_rty call = Interp x +let stop_worker x : stop_worker_rty call = StopWorker x +let print_ast x : print_ast_rty call = PrintAst x +let annotate x : annotate_rty call = Annotate x + +let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> + let mkGood : type a. a -> a value = fun x -> Good x in + try + match c with + | Add x -> mkGood (handler.add x) + | Edit_at x -> mkGood (handler.edit_at x) + | Query x -> mkGood (handler.query x) + | Goal x -> mkGood (handler.goals x) + | Evars x -> mkGood (handler.evars x) + | Hints x -> mkGood (handler.hints x) + | Status x -> mkGood (handler.status x) + | Search x -> mkGood (handler.search x) + | GetOptions x -> mkGood (handler.get_options x) + | SetOptions x -> mkGood (handler.set_options x) + | MkCases x -> mkGood (handler.mkcases x) + | Quit x -> mkGood (handler.quit x) + | Wait x -> mkGood (handler.wait x) + | About x -> mkGood (handler.about x) + | Init x -> mkGood (handler.init x) + | Interp x -> mkGood (handler.interp x) + | StopWorker x -> mkGood (handler.stop_worker x) + | PrintAst x -> mkGood (handler.print_ast x) + | Annotate x -> mkGood (handler.annotate x) + with any -> + let any = CErrors.push any in + Fail (handler.handle_exn any) + +(** brain dead code, edit if protocol messages are added/removed *) +let of_answer : type a. a call -> a value -> xml = function + | Add _ -> of_value (of_value_type add_rty_t ) + | Edit_at _ -> of_value (of_value_type edit_at_rty_t ) + | Query _ -> of_value (of_value_type query_rty_t ) + | Goal _ -> of_value (of_value_type goals_rty_t ) + | Evars _ -> of_value (of_value_type evars_rty_t ) + | Hints _ -> of_value (of_value_type hints_rty_t ) + | Status _ -> of_value (of_value_type status_rty_t ) + | Search _ -> of_value (of_value_type search_rty_t ) + | GetOptions _ -> of_value (of_value_type get_options_rty_t) + | SetOptions _ -> of_value (of_value_type set_options_rty_t) + | MkCases _ -> of_value (of_value_type mkcases_rty_t ) + | Quit _ -> of_value (of_value_type quit_rty_t ) + | Wait _ -> of_value (of_value_type wait_rty_t ) + | About _ -> of_value (of_value_type about_rty_t ) + | Init _ -> of_value (of_value_type init_rty_t ) + | Interp _ -> of_value (of_value_type interp_rty_t ) + | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) + | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) + | Annotate _ -> of_value (of_value_type annotate_rty_t ) + +let of_answer msg_fmt = + msg_format := msg_fmt; of_answer + +let to_answer : type a. a call -> xml -> a value = function + | Add _ -> to_value (to_value_type add_rty_t ) + | Edit_at _ -> to_value (to_value_type edit_at_rty_t ) + | Query _ -> to_value (to_value_type query_rty_t ) + | Goal _ -> to_value (to_value_type goals_rty_t ) + | Evars _ -> to_value (to_value_type evars_rty_t ) + | Hints _ -> to_value (to_value_type hints_rty_t ) + | Status _ -> to_value (to_value_type status_rty_t ) + | Search _ -> to_value (to_value_type search_rty_t ) + | GetOptions _ -> to_value (to_value_type get_options_rty_t) + | SetOptions _ -> to_value (to_value_type set_options_rty_t) + | MkCases _ -> to_value (to_value_type mkcases_rty_t ) + | Quit _ -> to_value (to_value_type quit_rty_t ) + | Wait _ -> to_value (to_value_type wait_rty_t ) + | About _ -> to_value (to_value_type about_rty_t ) + | Init _ -> to_value (to_value_type init_rty_t ) + | Interp _ -> to_value (to_value_type interp_rty_t ) + | StopWorker _ -> to_value (to_value_type stop_worker_rty_t) + | PrintAst _ -> to_value (to_value_type print_ast_rty_t ) + | Annotate _ -> to_value (to_value_type annotate_rty_t ) + +let of_call : type a. a call -> xml = fun q -> + let mkCall x = constructor "call" (str_of_call q) [x] in + match q with + | Add x -> mkCall (of_value_type add_sty_t x) + | Edit_at x -> mkCall (of_value_type edit_at_sty_t x) + | Query x -> mkCall (of_value_type query_sty_t x) + | Goal x -> mkCall (of_value_type goals_sty_t x) + | Evars x -> mkCall (of_value_type evars_sty_t x) + | Hints x -> mkCall (of_value_type hints_sty_t x) + | Status x -> mkCall (of_value_type status_sty_t x) + | Search x -> mkCall (of_value_type search_sty_t x) + | GetOptions x -> mkCall (of_value_type get_options_sty_t x) + | SetOptions x -> mkCall (of_value_type set_options_sty_t x) + | MkCases x -> mkCall (of_value_type mkcases_sty_t x) + | Quit x -> mkCall (of_value_type quit_sty_t x) + | Wait x -> mkCall (of_value_type wait_sty_t x) + | About x -> mkCall (of_value_type about_sty_t x) + | Init x -> mkCall (of_value_type init_sty_t x) + | Interp x -> mkCall (of_value_type interp_sty_t x) + | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x) + | PrintAst x -> mkCall (of_value_type print_ast_sty_t x) + | Annotate x -> mkCall (of_value_type annotate_sty_t x) + +let to_call : xml -> unknown_call = + do_match "call" (fun s a -> + let mkCallArg vt a = to_value_type vt (singleton a) in + match s with + | "Add" -> Unknown (Add (mkCallArg add_sty_t a)) + | "Edit_at" -> Unknown (Edit_at (mkCallArg edit_at_sty_t a)) + | "Query" -> Unknown (Query (mkCallArg query_sty_t a)) + | "Goal" -> Unknown (Goal (mkCallArg goals_sty_t a)) + | "Evars" -> Unknown (Evars (mkCallArg evars_sty_t a)) + | "Hints" -> Unknown (Hints (mkCallArg hints_sty_t a)) + | "Status" -> Unknown (Status (mkCallArg status_sty_t a)) + | "Search" -> Unknown (Search (mkCallArg search_sty_t a)) + | "GetOptions" -> Unknown (GetOptions (mkCallArg get_options_sty_t a)) + | "SetOptions" -> Unknown (SetOptions (mkCallArg set_options_sty_t a)) + | "MkCases" -> Unknown (MkCases (mkCallArg mkcases_sty_t a)) + | "Quit" -> Unknown (Quit (mkCallArg quit_sty_t a)) + | "Wait" -> Unknown (Wait (mkCallArg wait_sty_t a)) + | "About" -> Unknown (About (mkCallArg about_sty_t a)) + | "Init" -> Unknown (Init (mkCallArg init_sty_t a)) + | "Interp" -> Unknown (Interp (mkCallArg interp_sty_t a)) + | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a)) + | "PrintAst" -> Unknown (PrintAst (mkCallArg print_ast_sty_t a)) + | "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a)) + | x -> raise (Marshal_error("call",PCData x))) + +(** Debug printing *) + +let pr_value_gen pr = function + | Good v -> "GOOD " ^ pr v + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]" + | Fail (id,Some(i,j),str) -> + "FAIL "^Stateid.to_string id^ + " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]" +let pr_value v = pr_value_gen (fun _ -> "FIXME") v +let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with + | Add _ -> pr_value_gen (print add_rty_t ) value + | Edit_at _ -> pr_value_gen (print edit_at_rty_t ) value + | Query _ -> pr_value_gen (print query_rty_t ) value + | Goal _ -> pr_value_gen (print goals_rty_t ) value + | Evars _ -> pr_value_gen (print evars_rty_t ) value + | Hints _ -> pr_value_gen (print hints_rty_t ) value + | Status _ -> pr_value_gen (print status_rty_t ) value + | Search _ -> pr_value_gen (print search_rty_t ) value + | GetOptions _ -> pr_value_gen (print get_options_rty_t) value + | SetOptions _ -> pr_value_gen (print set_options_rty_t) value + | MkCases _ -> pr_value_gen (print mkcases_rty_t ) value + | Quit _ -> pr_value_gen (print quit_rty_t ) value + | Wait _ -> pr_value_gen (print wait_rty_t ) value + | About _ -> pr_value_gen (print about_rty_t ) value + | Init _ -> pr_value_gen (print init_rty_t ) value + | Interp _ -> pr_value_gen (print interp_rty_t ) value + | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value + | PrintAst _ -> pr_value_gen (print print_ast_rty_t ) value + | Annotate _ -> pr_value_gen (print annotate_rty_t ) value +let pr_call : type a. a call -> string = fun call -> + let return what x = str_of_call call ^ " " ^ print what x in + match call with + | Add x -> return add_sty_t x + | Edit_at x -> return edit_at_sty_t x + | Query x -> return query_sty_t x + | Goal x -> return goals_sty_t x + | Evars x -> return evars_sty_t x + | Hints x -> return hints_sty_t x + | Status x -> return status_sty_t x + | Search x -> return search_sty_t x + | GetOptions x -> return get_options_sty_t x + | SetOptions x -> return set_options_sty_t x + | MkCases x -> return mkcases_sty_t x + | Quit x -> return quit_sty_t x + | Wait x -> return wait_sty_t x + | About x -> return about_sty_t x + | Init x -> return init_sty_t x + | Interp x -> return interp_sty_t x + | StopWorker x -> return stop_worker_sty_t x + | PrintAst x -> return print_ast_sty_t x + | Annotate x -> return annotate_sty_t x + +let document to_string_fmt = + Printf.printf "=== Available calls ===\n\n"; + Array.iter (fun (cname, csty, crty) -> + Printf.printf "%12s : %s\n %14s %s\n" + ("\""^cname^"\"") (print_type csty) "->" (print_type crty)) + calls; + Printf.printf "\n=== Calls XML encoding ===\n\n"; + Printf.printf "A call \"C\" carrying input a is encoded as:\n\n%s\n\n" + (to_string_fmt (constructor "call" "C" [PCData "a"])); + Printf.printf "A response carrying output b can either be:\n\n%s\n\n" + (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); + Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" + (to_string_fmt (of_value (fun _ -> PCData "b") + (Fail (Stateid.initial,Some (15,34), Pp.str "error message")))); + document_type_encoding to_string_fmt + +(* Moved from feedback.mli : This is IDE specific and we don't want to + pollute the core with it *) + +open Feedback + +let of_message_level = function + | Debug -> + Serialize.constructor "message_level" "debug" [] + | Info -> Serialize.constructor "message_level" "info" [] + | Notice -> Serialize.constructor "message_level" "notice" [] + | Warning -> Serialize.constructor "message_level" "warning" [] + | Error -> Serialize.constructor "message_level" "error" [] +let to_message_level = + Serialize.do_match "message_level" (fun s args -> match s with + | "debug" -> Debug + | "info" -> Info + | "notice" -> Notice + | "warning" -> Warning + | "error" -> Error + | x -> raise Serialize.(Marshal_error("error level",PCData x))) + +let of_message lvl loc msg = + let lvl = of_message_level lvl in + let xloc = of_option of_loc loc in + let content = of_pp msg in + Xml_datatype.Element ("message", [], [lvl; xloc; content]) + +let to_message xml = match xml with + | Xml_datatype.Element ("message", [], [lvl; xloc; content]) -> + Message(to_message_level lvl, to_option to_loc xloc, to_pp content) + | x -> raise (Marshal_error("message",x)) + +let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with + | "addedaxiom", _ -> AddedAxiom + | "processed", _ -> Processed + | "processingin", [where] -> ProcessingIn (to_string where) + | "incomplete", _ -> Incomplete + | "complete", _ -> Complete + | "globref", [loc; filepath; modpath; ident; ty] -> + GlobRef(to_loc loc, to_string filepath, + to_string modpath, to_string ident, to_string ty) + | "globdef", [loc; ident; secpath; ty] -> + GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) + | "inprogress", [n] -> InProgress (to_int n) + | "workerstatus", [ns] -> + let n, s = to_pair to_string to_string ns in + WorkerStatus(n,s) + | "custom", [loc;name;x]-> Custom (to_option to_loc loc, to_string name, x) + | "filedependency", [from; dep] -> + FileDependency (to_option to_string from, to_string dep) + | "fileloaded", [dirpath; filename] -> + FileLoaded (to_string dirpath, to_string filename) + | "message", [x] -> to_message x + | x,l -> raise (Marshal_error("feedback_content",PCData (x ^ " with attributes " ^ string_of_int (List.length l))))) + +let of_feedback_content = function + | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] + | Processed -> constructor "feedback_content" "processed" [] + | ProcessingIn where -> + constructor "feedback_content" "processingin" [of_string where] + | Incomplete -> constructor "feedback_content" "incomplete" [] + | Complete -> constructor "feedback_content" "complete" [] + | GlobRef(loc, filepath, modpath, ident, ty) -> + constructor "feedback_content" "globref" [ + of_loc loc; + of_string filepath; + of_string modpath; + of_string ident; + of_string ty ] + | GlobDef(loc, ident, secpath, ty) -> + constructor "feedback_content" "globdef" [ + of_loc loc; + of_string ident; + of_string secpath; + of_string ty ] + | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] + | WorkerStatus(n,s) -> + constructor "feedback_content" "workerstatus" + [of_pair of_string of_string (n,s)] + | Custom (loc, name, x) -> + constructor "feedback_content" "custom" [of_option of_loc loc; of_string name; x] + | FileDependency (from, depends_on) -> + constructor "feedback_content" "filedependency" [ + of_option of_string from; + of_string depends_on] + | FileLoaded (dirpath, filename) -> + constructor "feedback_content" "fileloaded" [ + of_string dirpath; + of_string filename ] + | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ] + +let of_edit_or_state_id id = ["object","state"], of_stateid id + +let of_feedback msg = + let content = of_feedback_content msg.contents in + let obj, id = of_edit_or_state_id msg.span_id in + let route = string_of_int msg.route in + Element ("feedback", obj @ ["route",route], [id;content]) + +let of_feedback msg_fmt = + msg_format := msg_fmt; of_feedback + +let to_feedback xml = match xml with + | Element ("feedback", ["object","state";"route",route], [id;content]) -> { + doc_id = 0; + span_id = to_stateid id; + route = int_of_string route; + contents = to_feedback_content content } + | x -> raise (Marshal_error("feedback",x)) + +let is_feedback = function + | Element ("feedback", _, _) -> true + | _ -> false + +(* vim: set foldmethod=marker: *) + diff --git a/ide/protocol/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli new file mode 100644 index 000000000..ba6000f0a --- /dev/null +++ b/ide/protocol/xmlprotocol.mli @@ -0,0 +1,73 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* unknown_call + +val add : add_sty -> add_rty call +val edit_at : edit_at_sty -> edit_at_rty call +val query : query_sty -> query_rty call +val goals : goals_sty -> goals_rty call +val hints : hints_sty -> hints_rty call +val status : status_sty -> status_rty call +val mkcases : mkcases_sty -> mkcases_rty call +val evars : evars_sty -> evars_rty call +val search : search_sty -> search_rty call +val get_options : get_options_sty -> get_options_rty call +val set_options : set_options_sty -> set_options_rty call +val quit : quit_sty -> quit_rty call +val init : init_sty -> init_rty call +val stop_worker : stop_worker_sty -> stop_worker_rty call +(* internal use (fake_ide) only, do not use *) +val wait : wait_sty -> wait_rty call +(* retrocompatibility *) +val interp : interp_sty -> interp_rty call +val print_ast : print_ast_sty -> print_ast_rty call +val annotate : annotate_sty -> annotate_rty call + +val abstract_eval_call : handler -> 'a call -> 'a value + +(** * Protocol version *) + +val protocol_version : string + +(** By default, we still output messages in Richpp so we are + compatible with 8.6, however, 8.7 aware clients will want to + set this to Ppcmds *) +type msg_format = Richpp of int | Ppcmds + +(** * XML data marshalling *) + +val of_call : 'a call -> xml +val to_call : xml -> unknown_call + +val of_answer : msg_format -> 'a call -> 'a value -> xml +val to_answer : 'a call -> xml -> 'a value + +(* Prints the documentation of this module *) +val document : (xml -> string) -> unit + +(** * Debug printing *) + +val pr_call : 'a call -> string +val pr_value : 'a value -> string +val pr_full_value : 'a call -> 'a value -> string + +(** * Serializaiton of feedback *) +val of_feedback : msg_format -> Feedback.feedback -> xml +val to_feedback : xml -> Feedback.feedback + +val is_feedback : xml -> bool diff --git a/ide/richpp.ml b/ide/richpp.ml deleted file mode 100644 index 19e9799c1..000000000 --- a/ide/richpp.ml +++ /dev/null @@ -1,171 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* assert false - | Node (node, child, pos, ctx) -> - let data = Buffer.contents pp_buffer in - let () = Buffer.clear pp_buffer in - let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in - context.offset <- context.offset + len - in - - let open_xml_tag tag = - let () = push_pcdata () in - context.stack <- Node (tag, [], context.offset, context.stack) - in - - let close_xml_tag tag = - let () = push_pcdata () in - match context.stack with - | Leaf -> assert false - | Node (node, child, pos, ctx) -> - let () = assert (String.equal tag node) in - let annotation = { - annotation = Some tag; - startpos = pos; - endpos = context.offset; - } in - let xml = Element (node, annotation, List.rev child) in - match ctx with - | Leaf -> - (** Final node: we keep the result in a dummy context *) - context.stack <- Node ("", [xml], 0, Leaf) - | Node (node, child, pos, ctx) -> - context.stack <- Node (node, xml :: child, pos, ctx) - in - - let open Format in - - let ft = formatter_of_buffer pp_buffer in - - let tag_functions = { - mark_open_tag = (fun tag -> let () = open_xml_tag tag in ""); - mark_close_tag = (fun tag -> let () = close_xml_tag tag in ""); - print_open_tag = ignore; - print_close_tag = ignore; - } in - - pp_set_formatter_tag_functions ft tag_functions; - pp_set_mark_tags ft true; - - (* Setting the formatter *) - pp_set_margin ft width; - let m = max (64 * width / 100) (width-30) in - pp_set_max_indent ft m; - pp_set_max_boxes ft 50 ; - pp_set_ellipsis_text ft "..."; - - (** The whole output must be a valid document. To that - end, we nest the document inside tags. *) - pp_open_box ft 0; - pp_open_tag ft "pp"; - Pp.(pp_with ft ppcmds); - pp_close_tag ft (); - pp_close_box ft (); - - (** Get the resulting XML tree. *) - let () = pp_print_flush ft () in - let () = assert (Buffer.length pp_buffer = 0) in - match context.stack with - | Node ("", [xml], 0, Leaf) -> xml - | _ -> assert false - - -let annotations_positions xml = - let rec node accu = function - | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> - children ((annotation, (startpos, endpos)) :: accu) cs - | Element (_, _, cs) -> - children accu cs - | _ -> - accu - and children accu cs = - List.fold_left node accu cs - in - node [] xml - -let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = - let rec node = function - | Element (index, { annotation; startpos; endpos }, cs) -> - let attributes = - [ "startpos", string_of_int startpos; - "endpos", string_of_int endpos - ] - @ (match annotation with - | None -> [] - | Some annotation -> attributes_of_annotation annotation - ) - in - let tag = - match annotation with - | None -> index - | Some annotation -> tag_of_annotation annotation - in - Element (tag, attributes, List.map node cs) - | PCData s -> - PCData s - in - node xml - -type richpp = xml - -let richpp_of_pp width pp = - let rec drop = function - | PCData s -> [PCData s] - | Element (_, annotation, cs) -> - let cs = List.concat (List.map drop cs) in - match annotation.annotation with - | None -> cs - | Some s -> [Element (s, [], cs)] - in - let xml = rich_pp width pp in - Element ("_", [], drop xml) diff --git a/ide/richpp.mli b/ide/richpp.mli deleted file mode 100644 index 31fc7b56f..000000000 --- a/ide/richpp.mli +++ /dev/null @@ -1,53 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Pp.t -> Pp.pp_tag located Xml_datatype.gxml - -(** [annotations_positions ssdoc] returns a list associating each - annotations with its position in the string from which [ssdoc] is - built. *) -val annotations_positions : - 'annotation located Xml_datatype.gxml -> - ('annotation * (int * int)) list - -(** [xml_of_rich_pp ssdoc] returns an XML representation of the - semi-structured document [ssdoc]. *) -val xml_of_rich_pp : - ('annotation -> string) -> - ('annotation -> (string * string) list) -> - 'annotation located Xml_datatype.gxml -> - Xml_datatype.xml - -(** {5 Enriched text} *) - -type richpp = Xml_datatype.xml - -(** Type of text with style annotations *) - -val richpp_of_pp : int -> Pp.t -> richpp -(** Extract style information from formatted text *) diff --git a/ide/serialize.ml b/ide/serialize.ml deleted file mode 100644 index 86074d44d..000000000 --- a/ide/serialize.ml +++ /dev/null @@ -1,123 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* raise Not_found - | (k, v) :: l when CString.equal k attr -> v - | _ :: l -> get_attr attr l - -let massoc x l = - try get_attr x l - with Not_found -> raise (Marshal_error("attribute " ^ x,PCData "not there")) - -let constructor t c args = Element (t, ["val", c], args) -let do_match t mf = function - | Element (s, attrs, args) when CString.equal s t -> - let c = massoc "val" attrs in - mf c args - | x -> raise (Marshal_error (t,x)) - -let singleton = function - | [x] -> x - | l -> raise (Marshal_error - ("singleton",PCData ("list of length " ^ string_of_int (List.length l)))) - -let raw_string = function - | [] -> "" - | [PCData s] -> s - | x::_ -> raise (Marshal_error("raw string",x)) - -(** Base types *) - -let of_unit () = Element ("unit", [], []) -let to_unit : xml -> unit = function - | Element ("unit", [], []) -> () - | x -> raise (Marshal_error ("unit",x)) - -let of_bool (b : bool) : xml = - if b then constructor "bool" "true" [] - else constructor "bool" "false" [] -let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with - | "true" -> true - | "false" -> false - | x -> raise (Marshal_error("bool",PCData x))) - -let of_list (f : 'a -> xml) (l : 'a list) = - Element ("list", [], List.map f l) -let to_list (f : xml -> 'a) : xml -> 'a list = function - | Element ("list", [], l) -> List.map f l - | x -> raise (Marshal_error("list",x)) - -let of_option (f : 'a -> xml) : 'a option -> xml = function - | None -> Element ("option", ["val", "none"], []) - | Some x -> Element ("option", ["val", "some"], [f x]) -let to_option (f : xml -> 'a) : xml -> 'a option = function - | Element ("option", ["val", "none"], []) -> None - | Element ("option", ["val", "some"], [x]) -> Some (f x) - | x -> raise (Marshal_error("option",x)) - -let of_string (s : string) : xml = Element ("string", [], [PCData s]) -let to_string : xml -> string = function - | Element ("string", [], l) -> raw_string l - | x -> raise (Marshal_error("string",x)) - -let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)]) -let to_int : xml -> int = function - | Element ("int", [], [PCData s]) -> - (try int_of_string s with Failure _ -> raise(Marshal_error("int",PCData s))) - | x -> raise (Marshal_error("int",x)) - -let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml = - Element ("pair", [], [f (fst x); g (snd x)]) -let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function - | Element ("pair", [], [x; y]) -> (f x, g y) - | x -> raise (Marshal_error("pair",x)) - -let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function - | CSig.Inl x -> Element ("union", ["val","in_l"], [f x]) - | CSig.Inr x -> Element ("union", ["val","in_r"], [g x]) -let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function - | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x) - | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x) - | x -> raise (Marshal_error("union",x)) - -(** More elaborate types *) - -let of_edit_id i = Element ("edit_id",["val",string_of_int i],[]) -let to_edit_id = function - | Element ("edit_id",["val",i],[]) -> - let id = int_of_string i in - assert (id <= 0 ); - id - | x -> raise (Marshal_error("edit_id",x)) - -let of_loc loc = - let start, stop = Loc.unloc loc in - Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[]) -let to_loc xml = - match xml with - | Element ("loc", l,[]) -> - let start = massoc "start" l in - let stop = massoc "stop" l in - (try - Loc.make_loc (int_of_string start, int_of_string stop) - with Not_found | Invalid_argument _ -> raise (Marshal_error("loc",PCData(start^":"^stop)))) - | x -> raise (Marshal_error("loc",x)) - -let of_xml x = Element ("xml", [], [x]) -let to_xml xml = match xml with -| Element ("xml", [], [x]) -> x -| x -> raise (Marshal_error("xml",x)) diff --git a/ide/serialize.mli b/ide/serialize.mli deleted file mode 100644 index af082f25b..000000000 --- a/ide/serialize.mli +++ /dev/null @@ -1,41 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* (string * string) list -> string -val constructor: string -> string -> xml list -> xml -val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b -val singleton: 'a list -> 'a -val raw_string: xml list -> string -val of_unit: unit -> xml -val to_unit: xml -> unit -val of_bool: bool -> xml -val to_bool: xml -> bool -val of_list: ('a -> xml) -> 'a list -> xml -val to_list: (xml -> 'a) -> xml -> 'a list -val of_option: ('a -> xml) -> 'a option -> xml -val to_option: (xml -> 'a) -> xml -> 'a option -val of_string: string -> xml -val to_string: xml -> string -val of_int: int -> xml -val to_int: xml -> int -val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml -val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b -val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml -val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union -val of_edit_id: int -> xml -val to_edit_id: xml -> int -val of_loc : Loc.t -> xml -val to_loc : xml -> Loc.t -val of_xml : xml -> xml -val to_xml : xml -> xml diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml deleted file mode 100644 index 69e8b647a..000000000 --- a/ide/utils/configwin.ml +++ /dev/null @@ -1,51 +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 ?width ?height - conf_struct_list = - Configwin_ihm.edit ~with_apply: true ~apply title ?width ?height conf_struct_list diff --git a/ide/utils/configwin.mli b/ide/utils/configwin.mli deleted file mode 100644 index 7616e471d..000000000 --- a/ide/utils/configwin.mli +++ /dev/null @@ -1,164 +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 -> - ?width:int -> - ?height:int -> - configuration_structure list -> - return_button diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml deleted file mode 100644 index d16efa603..000000000 --- a/ide/utils/configwin_ihm.ml +++ /dev/null @@ -1,809 +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 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 - (tt:GData.tooltips) - = - 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 _ = - match help_opt with - None -> () - | Some help -> - tt#set_tip ~text: help ~privat: help wev#coerce - 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 (tt:GData.tooltips) = - 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 _ = - match param.string_help with - None -> () - | Some help -> - tt#set_tip ~text: help ~privat: help wev#coerce - 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 (tt:GData.tooltips) = - 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 _ = - match param.combo_help with - None -> () - | Some help -> - tt#set_tip ~text: help ~privat: help wev#coerce - 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 (tt:GData.tooltips) = - 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 (tt:GData.tooltips) = - 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 _ = - match param.string_help with - None -> () - | Some help -> - tt#set_tip ~text: help ~privat: help wev#coerce - 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 (tt:GData.tooltips) = - let _ = dbg "bool_param_box" in - let wchk = GButton.check_button - ~label: param.bool_label - () - in - let _ = - match param.bool_help with - None -> () - | Some help -> tt#set_tip ~text: help ~privat: help wchk#coerce - 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 _ = - match param.md_help with - None -> () - | Some help -> - let tooltips = GData.tooltips () in - ignore (hbox#connect#destroy ~callback: tooltips#destroy); - tooltips#set_tip wev#coerce ~text: help ~privat: 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) (tt:GData.tooltips) = - 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 (tt : GData.tooltips) 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 tt in - let _ = main_box#pack ~expand: false ~padding: 2 box#box in - box - | Combo_param p -> - let box = new combo_param_box p tt in - let _ = main_box#pack ~expand: false ~padding: 2 box#box in - box - | Text_param p -> - let box = new text_param_box p tt 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 tt in - let _ = main_box#pack ~expand: false ~padding: 2 box#box in - box - | List_param f -> - let box = f tt in - let _ = main_box#pack ~expand: true ~padding: 2 box#box in - box - | Custom_param p -> - let box = new custom_param_box p tt 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 ?width ?height - conf_struct = - let dialog = GWindow.dialog - ~position:`CENTER - ~modal: true ~title: title - ?height ?width - () - in - let tooltips = GData.tooltips () in - - let config_box = new configuration_box tooltips conf_struct in - - let _ = dialog#vbox#add 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 () = - tooltips#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 tt -> - 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 ; - } - tt - ) - -(** 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 ; - } diff --git a/ide/utils/configwin_ihm.mli b/ide/utils/configwin_ihm.mli deleted file mode 100644 index c867ad912..000000000 --- a/ide/utils/configwin_ihm.mli +++ /dev/null @@ -1,66 +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 -> - ?width:int -> - ?height:int -> - configuration_structure list -> - return_button diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml deleted file mode 100644 index de1b4721d..000000000 --- a/ide/utils/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/utils/configwin_types.mli b/ide/utils/configwin_types.mli deleted file mode 100644 index 9e339d135..000000000 --- a/ide/utils/configwin_types.mli +++ /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 paramter *) - 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 (GData.tooltips -> ) - | 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/xml_lexer.mli b/ide/xml_lexer.mli deleted file mode 100644 index e61cb055f..000000000 --- a/ide/xml_lexer.mli +++ /dev/null @@ -1,44 +0,0 @@ -(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library 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 - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -type error = - | EUnterminatedComment - | EUnterminatedString - | EIdentExpected - | ECloseExpected - | ENodeExpected - | EAttributeNameExpected - | EAttributeValueExpected - | EUnterminatedEntity - -exception Error of error - -type token = - | Tag of string * (string * string) list * bool - | PCData of string - | Endtag of string - | Eof - -type pos = int * int * int * int - -val init : Lexing.lexbuf -> unit -val close : unit -> unit -val token : Lexing.lexbuf -> token -val pos : Lexing.lexbuf -> pos -val restore : pos -> unit diff --git a/ide/xml_lexer.mll b/ide/xml_lexer.mll deleted file mode 100644 index 4a52147e1..000000000 --- a/ide/xml_lexer.mll +++ /dev/null @@ -1,320 +0,0 @@ -{(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library 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 - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -open Lexing - -type error = - | EUnterminatedComment - | EUnterminatedString - | EIdentExpected - | ECloseExpected - | ENodeExpected - | EAttributeNameExpected - | EAttributeValueExpected - | EUnterminatedEntity - -exception Error of error - -type pos = int * int * int * int - -type token = - | Tag of string * (string * string) list * bool - | PCData of string - | Endtag of string - | Eof - -let last_pos = ref 0 -and current_line = ref 0 -and current_line_start = ref 0 - -let tmp = Buffer.create 200 - -let idents = Hashtbl.create 0 - -let _ = begin - Hashtbl.add idents "nbsp;" " "; - Hashtbl.add idents "gt;" ">"; - Hashtbl.add idents "lt;" "<"; - Hashtbl.add idents "amp;" "&"; - Hashtbl.add idents "apos;" "'"; - Hashtbl.add idents "quot;" "\""; -end - -let init lexbuf = - current_line := 1; - current_line_start := lexeme_start lexbuf; - last_pos := !current_line_start - -let close lexbuf = - Buffer.reset tmp - -let pos lexbuf = - !current_line , !current_line_start , - !last_pos , - lexeme_start lexbuf - -let restore (cl,cls,lp,_) = - current_line := cl; - current_line_start := cls; - last_pos := lp - -let newline lexbuf = - incr current_line; - last_pos := lexeme_end lexbuf; - current_line_start := !last_pos - -let error lexbuf e = - last_pos := lexeme_start lexbuf; - raise (Error e) - -[@@@ocaml.warning "-3"] (* String.lowercase_ascii since 4.03.0 GPR#124 *) -let lowercase = String.lowercase -[@@@ocaml.warning "+3"] -} - -let newline = ['\n'] -let break = ['\r'] -let space = [' ' '\t'] -let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.'] -let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar* -let entitychar = ['A'-'Z' 'a'-'z'] -let pcchar = [^ '\r' '\n' '<' '>' '&'] - -rule token = parse - | newline | (newline break) | break - { - newline lexbuf; - PCData "\n" - } - | "" - { () } - | eof - { raise (Error EUnterminatedComment) } - | _ - { comment lexbuf } - -and header = parse - | newline | (newline break) | break - { - newline lexbuf; - header lexbuf - } - | "?>" - { () } - | eof - { error lexbuf ECloseExpected } - | _ - { header lexbuf } - -and pcdata = parse - | newline | (newline break) | break - { - Buffer.add_char tmp '\n'; - newline lexbuf; - pcdata lexbuf - } - | pcchar+ - { - Buffer.add_string tmp (lexeme lexbuf); - pcdata lexbuf - } - | "&#" - { - Buffer.add_string tmp (lexeme lexbuf); - pcdata lexbuf; - } - | '&' - { - Buffer.add_string tmp (entity lexbuf); - pcdata lexbuf - } - | "" - { Buffer.contents tmp } - -and entity = parse - | entitychar+ ';' - { - let ident = lexeme lexbuf in - try - Hashtbl.find idents (lowercase ident) - with - Not_found -> "&" ^ ident - } - | _ | eof - { raise (Error EUnterminatedEntity) } - -and ident_name = parse - | ident - { lexeme lexbuf } - | _ | eof - { error lexbuf EIdentExpected } - -and close_tag = parse - | '>' - { () } - | _ | eof - { error lexbuf ECloseExpected } - -and attributes = parse - | '>' - { [], false } - | "/>" - { [], true } - | "" (* do not read a char ! *) - { - let key = attribute lexbuf in - let data = attribute_data lexbuf in - ignore_spaces lexbuf; - let others, closed = attributes lexbuf in - (key, data) :: others, closed - } - -and attribute = parse - | ident - { lexeme lexbuf } - | _ | eof - { error lexbuf EAttributeNameExpected } - -and attribute_data = parse - | space* '=' space* '"' - { - Buffer.reset tmp; - last_pos := lexeme_end lexbuf; - dq_string lexbuf - } - | space* '=' space* '\'' - { - Buffer.reset tmp; - last_pos := lexeme_end lexbuf; - q_string lexbuf - } - | _ | eof - { error lexbuf EAttributeValueExpected } - -and dq_string = parse - | '"' - { Buffer.contents tmp } - | '\\' [ '"' '\\' ] - { - Buffer.add_char tmp (lexeme_char lexbuf 1); - dq_string lexbuf - } - | '&' - { - Buffer.add_string tmp (entity lexbuf); - dq_string lexbuf - } - | eof - { raise (Error EUnterminatedString) } - | _ - { - Buffer.add_char tmp (lexeme_char lexbuf 0); - dq_string lexbuf - } - -and q_string = parse - | '\'' - { Buffer.contents tmp } - | '\\' [ '\'' '\\' ] - { - Buffer.add_char tmp (lexeme_char lexbuf 1); - q_string lexbuf - } - | '&' - { - Buffer.add_string tmp (entity lexbuf); - q_string lexbuf - } - | eof - { raise (Error EUnterminatedString) } - | _ - { - Buffer.add_char tmp (lexeme_char lexbuf 0); - q_string lexbuf - } diff --git a/ide/xml_parser.ml b/ide/xml_parser.ml deleted file mode 100644 index 8db3f9e8b..000000000 --- a/ide/xml_parser.ml +++ /dev/null @@ -1,232 +0,0 @@ -(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * Copyright (C) 2003 Jacques Garrigue - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library 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 - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -open Printf -open Xml_datatype - -type xml = Xml_datatype.xml - -type error_pos = { - eline : int; - eline_start : int; - emin : int; - emax : int; -} - -type error_msg = - | UnterminatedComment - | UnterminatedString - | UnterminatedEntity - | IdentExpected - | CloseExpected - | NodeExpected - | AttributeNameExpected - | AttributeValueExpected - | EndOfTagExpected of string - | EOFExpected - | Empty - -type error = error_msg * error_pos - -exception Error of error - -exception File_not_found of string - -type t = { - mutable check_eof : bool; - mutable concat_pcdata : bool; - source : Lexing.lexbuf; - stack : Xml_lexer.token Stack.t; -} - -type source = - | SChannel of in_channel - | SString of string - | SLexbuf of Lexing.lexbuf - -exception Internal_error of error_msg -exception NoMoreData - -let xml_error = ref (fun _ -> assert false) -let file_not_found = ref (fun _ -> assert false) - -let is_blank s = - let len = String.length s in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = s.[!i] in - (* no '\r' because we replaced them in the lexer *) - if c = ' ' || c = '\n' || c = '\t' then incr i - else break := false - done; - !i = len - -let _raises e f = - xml_error := e; - file_not_found := f - -let make source = - let source = match source with - | SChannel chan -> Lexing.from_channel chan - | SString s -> Lexing.from_string s - | SLexbuf lexbuf -> lexbuf - in - let () = Xml_lexer.init source in - { - check_eof = false; - concat_pcdata = true; - source = source; - stack = Stack.create (); - } - -let check_eof p v = p.check_eof <- v - -let pop s = - try - Stack.pop s.stack - with - Stack.Empty -> - Xml_lexer.token s.source - -let push t s = - Stack.push t s.stack - -let canonicalize l = - let has_elt = List.exists (function Element _ -> true | _ -> false) l in - if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l - else l - -let rec read_xml do_not_canonicalize s = - let rec read_node s = - match pop s with - | Xml_lexer.PCData s -> PCData s - | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, []) - | Xml_lexer.Tag (tag, attr, false) -> - let elements = read_elems tag s in - let elements = - if do_not_canonicalize then elements else canonicalize elements - in - Element (tag, attr, elements) - | t -> - push t s; - raise NoMoreData - - and read_elems tag s = - let elems = ref [] in - (try - while true do - let node = read_node s in - match node, !elems with - | PCData c , (PCData c2) :: q -> - elems := PCData (c2 ^ c) :: q - | _, l -> - elems := node :: l - done - with - NoMoreData -> ()); - match pop s with - | Xml_lexer.Endtag s when s = tag -> List.rev !elems - | t -> raise (Internal_error (EndOfTagExpected tag)) - in - match read_node s with - | (Element _) as node -> - node - | PCData c -> - if is_blank c then - read_xml do_not_canonicalize s - else - raise (Xml_lexer.Error Xml_lexer.ENodeExpected) - -let convert = function - | Xml_lexer.EUnterminatedComment -> UnterminatedComment - | Xml_lexer.EUnterminatedString -> UnterminatedString - | Xml_lexer.EIdentExpected -> IdentExpected - | Xml_lexer.ECloseExpected -> CloseExpected - | Xml_lexer.ENodeExpected -> NodeExpected - | Xml_lexer.EAttributeNameExpected -> AttributeNameExpected - | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected - | Xml_lexer.EUnterminatedEntity -> UnterminatedEntity - -let error_of_exn xparser = function - | NoMoreData when pop xparser = Xml_lexer.Eof -> Empty - | NoMoreData -> NodeExpected - | Internal_error e -> e - | Xml_lexer.Error e -> convert e - | e -> - (*let e = Errors.push e in: We do not record backtrace here. *) - raise e - -let do_parse do_not_canonicalize xparser = - try - Xml_lexer.init xparser.source; - let x = read_xml do_not_canonicalize xparser in - if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected); - Xml_lexer.close (); - x - with any -> - Xml_lexer.close (); - raise (!xml_error (error_of_exn xparser any) xparser.source) - -let parse ?(do_not_canonicalize=false) p = - do_parse do_not_canonicalize p - -let error_msg = function - | UnterminatedComment -> "Unterminated comment" - | UnterminatedString -> "Unterminated string" - | UnterminatedEntity -> "Unterminated entity" - | IdentExpected -> "Ident expected" - | CloseExpected -> "Element close expected" - | NodeExpected -> "Xml node expected" - | AttributeNameExpected -> "Attribute name expected" - | AttributeValueExpected -> "Attribute value expected" - | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag - | EOFExpected -> "End of file expected" - | Empty -> "Empty" - -let error (msg,pos) = - if pos.emin = pos.emax then - sprintf "%s line %d character %d" (error_msg msg) pos.eline - (pos.emin - pos.eline_start) - else - sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline - (pos.emin - pos.eline_start) (pos.emax - pos.eline_start) - -let line e = e.eline - -let range e = - e.emin - e.eline_start , e.emax - e.eline_start - -let abs_range e = - e.emin , e.emax - -let pos source = - let line, lstart, min, max = Xml_lexer.pos source in - { - eline = line; - eline_start = lstart; - emin = min; - emax = max; - } - -let () = _raises (fun x p -> - (* local cast : Xml.error_msg -> error_msg *) - Error (x, pos p)) - (fun f -> File_not_found f) diff --git a/ide/xml_parser.mli b/ide/xml_parser.mli deleted file mode 100644 index ac2eab352..000000000 --- a/ide/xml_parser.mli +++ /dev/null @@ -1,106 +0,0 @@ -(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library 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 - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -(** Xml Light Parser - - While basic parsing functions can be used in the {!Xml} module, this module - is providing a way to create, configure and run an Xml parser. - -*) - - -(** An Xml node is either - [Element (tag-name, attributes, children)] or [PCData text] *) -type xml = Xml_datatype.xml - -(** Abstract type for an Xml parser. *) -type t - -(** {6:exc Xml Exceptions} *) - -(** Several exceptions can be raised when parsing an Xml document : {ul - {li {!Xml.Error} is raised when an xml parsing error occurs. the - {!Xml.error_msg} tells you which error occurred during parsing - and the {!Xml.error_pos} can be used to retrieve the document - location where the error occurred at.} - {li {!Xml.File_not_found} is raised when an error occurred while - opening a file with the {!Xml.parse_file} function.} - } - *) - -type error_pos - -type error_msg = - | UnterminatedComment - | UnterminatedString - | UnterminatedEntity - | IdentExpected - | CloseExpected - | NodeExpected - | AttributeNameExpected - | AttributeValueExpected - | EndOfTagExpected of string - | EOFExpected - | Empty - -type error = error_msg * error_pos - -exception Error of error - -exception File_not_found of string - -(** Get a full error message from an Xml error. *) -val error : error -> string - -(** Get the Xml error message as a string. *) -val error_msg : error_msg -> string - -(** Get the line the error occurred at. *) -val line : error_pos -> int - -(** Get the relative character range (in current line) the error occurred at.*) -val range : error_pos -> int * int - -(** Get the absolute character range the error occurred at. *) -val abs_range : error_pos -> int * int - -val pos : Lexing.lexbuf -> error_pos - -(** Several kind of resources can contain Xml documents. *) -type source = -| SChannel of in_channel -| SString of string -| SLexbuf of Lexing.lexbuf - -(** This function returns a new parser with default options. *) -val make : source -> t - -(** When a Xml document is parsed, the parser may check that the end of the - document is reached, so for example parsing [""] will fail instead - of returning only the A element. You can turn on this check by setting - [check_eof] to [true] {i (by default, check_eof is false, unlike - in the original Xmllight)}. *) -val check_eof : t -> bool -> unit - -(** Once the parser is configured, you can run the parser on a any kind - of xml document source to parse its contents into an Xml data structure. - - When [do_not_canonicalize] is set, the XML document is given as - is, without trying to remove blank PCDATA elements. *) -val parse : ?do_not_canonicalize:bool -> t -> xml diff --git a/ide/xml_printer.ml b/ide/xml_printer.ml deleted file mode 100644 index 488ef7bf5..000000000 --- a/ide/xml_printer.ml +++ /dev/null @@ -1,147 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* puts " "; - | '>' -> puts ">" - | '<' -> puts "<" - | '&' -> - if p < l - 1 && text.[p + 1] = '#' then - putc '&' - else - puts "&" - | '\'' -> puts "'" - | '"' -> puts """ - | c -> putc c - done - -let buffer_attr tmp (n,v) = - let puts = Buffer.add_string tmp in - let putc = Buffer.add_char tmp in - putc ' '; - puts n; - puts "=\""; - let l = String.length v in - for p = 0 to l - 1 do - match v.[p] with - | '\\' -> puts "\\\\" - | '"' -> puts "\\\"" - | '<' -> puts "<" - | '&' -> puts "&" - | c -> putc c - done; - putc '"' - -let to_buffer tmp x = - let pcdata = ref false in - let puts = Buffer.add_string tmp in - let putc = Buffer.add_char tmp in - let rec loop = function - | Element (tag,alist,[]) -> - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - puts "/>"; - pcdata := false; - | Element (tag,alist,l) -> - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - putc '>'; - pcdata := false; - List.iter loop l; - puts "'; - pcdata := false; - | PCData text -> - if !pcdata then putc ' '; - buffer_pcdata tmp text; - pcdata := true; - in - loop x - -let pcdata_to_string s = - let b = Buffer.create 13 in - buffer_pcdata b s; - Buffer.contents b - -let to_string x = - let b = Buffer.create 200 in - to_buffer b x; - Buffer.contents b - -let to_string_fmt x = - let tmp = Buffer.create 200 in - let puts = Buffer.add_string tmp in - let putc = Buffer.add_char tmp in - let rec loop ?(newl=false) tab = function - | Element (tag, alist, []) -> - puts tab; - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - puts "/>"; - if newl then putc '\n'; - | Element (tag, alist, [PCData text]) -> - puts tab; - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - puts ">"; - buffer_pcdata tmp text; - puts "'; - if newl then putc '\n'; - | Element (tag, alist, l) -> - puts tab; - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - puts ">\n"; - List.iter (loop ~newl:true (tab^" ")) l; - puts tab; - puts "'; - if newl then putc '\n'; - | PCData text -> - buffer_pcdata tmp text; - if newl then putc '\n'; - in - loop "" x; - Buffer.contents tmp - -let print t xml = - let tmp, flush = match t with - | TChannel oc -> - let b = Buffer.create 200 in - b, (fun () -> Buffer.output_buffer oc b; flush oc) - | TBuffer b -> - b, (fun () -> ()) - in - to_buffer tmp xml; - flush () diff --git a/ide/xml_printer.mli b/ide/xml_printer.mli deleted file mode 100644 index 178f7c808..000000000 --- a/ide/xml_printer.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* t - -(** Print the xml data structure to a source into a compact xml string (without - any user-readable formating ). *) -val print : t -> xml -> unit - -(** Print the xml data structure into a compact xml string (without - any user-readable formating ). *) -val to_string : xml -> string - -(** Print the xml data structure into an user-readable string with - tabs and lines break between different nodes. *) -val to_string_fmt : xml -> string - -(** Print PCDATA as a string by escaping XML entities. *) -val pcdata_to_string : string -> string diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml deleted file mode 100644 index e18219210..000000000 --- a/ide/xmlprotocol.ml +++ /dev/null @@ -1,964 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - constructor "search_cst" "name_pattern" [of_string s] - | Type_Pattern s -> - constructor "search_cst" "type_pattern" [of_string s] - | SubType_Pattern s -> - constructor "search_cst" "subtype_pattern" [of_string s] - | In_Module m -> - constructor "search_cst" "in_module" [of_list of_string m] - | Include_Blacklist -> - constructor "search_cst" "include_blacklist" [] -let to_search_cst = do_match "search_cst" (fun s args -> match s with - | "name_pattern" -> Name_Pattern (to_string (singleton args)) - | "type_pattern" -> Type_Pattern (to_string (singleton args)) - | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) - | "in_module" -> In_Module (to_list to_string (singleton args)) - | "include_blacklist" -> Include_Blacklist - | x -> raise (Marshal_error("search",PCData x))) - -let of_coq_object f ans = - let prefix = of_list of_string ans.coq_object_prefix in - let qualid = of_list of_string ans.coq_object_qualid in - let obj = f ans.coq_object_object in - Element ("coq_object", [], [prefix; qualid; obj]) - -let to_coq_object f = function -| Element ("coq_object", [], [prefix; qualid; obj]) -> - let prefix = to_list to_string prefix in - let qualid = to_list to_string qualid in - let obj = f obj in { - coq_object_prefix = prefix; - coq_object_qualid = qualid; - coq_object_object = obj; - } -| x -> raise (Marshal_error("coq_object",x)) - -let of_option_value = function - | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i] - | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b] - | StringValue s -> constructor "option_value" "stringvalue" [of_string s] - | StringOptValue s -> constructor "option_value" "stringoptvalue" [of_option of_string s] -let to_option_value = do_match "option_value" (fun s args -> match s with - | "intvalue" -> IntValue (to_option to_int (singleton args)) - | "boolvalue" -> BoolValue (to_bool (singleton args)) - | "stringvalue" -> StringValue (to_string (singleton args)) - | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args)) - | x -> raise (Marshal_error("*value",PCData x))) - -let of_option_state s = - Element ("option_state", [], [ - of_bool s.opt_sync; - of_bool s.opt_depr; - of_string s.opt_name; - of_option_value s.opt_value]) -let to_option_state = function - | Element ("option_state", [], [sync; depr; name; value]) -> { - opt_sync = to_bool sync; - opt_depr = to_bool depr; - opt_name = to_string name; - opt_value = to_option_value value } - | x -> raise (Marshal_error("option_state",x)) - -let to_stateid = function - | Element ("state_id",["val",i],[]) -> - let id = int_of_string i in - Stateid.of_int id - | _ -> raise (Invalid_argument "to_state_id") - -let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[]) - -let to_routeid = function - | Element ("route_id",["val",i],[]) -> - let id = int_of_string i in id - | _ -> raise (Invalid_argument "to_route_id") - -let of_routeid i = Element ("route_id",["val",string_of_int i],[]) - -let of_box (ppb : Pp.block_type) = let open Pp in match ppb with - | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] - | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] - | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] - | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] - -let to_box = let open Pp in - do_match "ppbox" (fun s args -> match s with - | "hbox" -> Pp_hbox (to_int (singleton args)) - | "vbox" -> Pp_vbox (to_int (singleton args)) - | "hvbox" -> Pp_hvbox (to_int (singleton args)) - | "hovbox" -> Pp_hovbox (to_int (singleton args)) - | x -> raise (Marshal_error("*ppbox",PCData x)) - ) - -let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with - | Ppcmd_empty -> constructor "ppdoc" "empty" [] - | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] - | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] - | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] - | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair of_string of_pp (t,s)] - | Ppcmd_print_break (i,j) - -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] - | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] - | Ppcmd_comment cmd -> constructor "ppdoc" "comment" [of_list of_string cmd] - - -let rec to_pp xpp = let open Pp in - Pp.unrepr @@ - do_match "ppdoc" (fun s args -> match s with - | "empty" -> Ppcmd_empty - | "string" -> Ppcmd_string (to_string (singleton args)) - | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) - | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in - Ppcmd_box(bt,s) - | "tag" -> let (tg,s) = to_pair to_string to_pp (singleton args) in - Ppcmd_tag(tg,s) - | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in - Ppcmd_print_break(i, j) - | "newline" -> Ppcmd_force_newline - | "comment" -> Ppcmd_comment (to_list to_string (singleton args)) - | x -> raise (Marshal_error("*ppdoc",PCData x)) - ) xpp - -let of_richpp x = Element ("richpp", [], [x]) - -(* Run-time Selectable *) -let of_pp (pp : Pp.t) = - match !msg_format with - | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) - | Ppcmds -> of_pp pp - -let of_value f = function -| Good x -> Element ("value", ["val", "good"], [f x]) -| Fail (id,loc, msg) -> - let loc = match loc with - | None -> [] - | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in - let id = of_stateid id in - Element ("value", ["val", "fail"] @ loc, [id; of_pp msg]) - -let to_value f = function -| Element ("value", attrs, l) -> - let ans = massoc "val" attrs in - if ans = "good" then Good (f (singleton l)) - else if ans = "fail" then - let loc = - try - let loc_s = int_of_string (Serialize.massoc "loc_s" attrs) in - let loc_e = int_of_string (Serialize.massoc "loc_e" attrs) in - Some (loc_s, loc_e) - with Marshal_error _ | Failure _ -> None - in - let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in - let id = to_stateid id in - let msg = to_pp msg in - Fail (id, loc, msg) - else raise (Marshal_error("good or fail",PCData ans)) -| x -> raise (Marshal_error("value",x)) - -let of_status s = - let of_so = of_option of_string in - let of_sl = of_list of_string in - Element ("status", [], [ - of_sl s.status_path; - of_so s.status_proofname; - of_sl s.status_allproofs; - of_int s.status_proofnum; ]) -let to_status = function - | Element ("status", [], [path; name; prfs; pnum]) -> { - status_path = to_list to_string path; - status_proofname = to_option to_string name; - status_allproofs = to_list to_string prfs; - status_proofnum = to_int pnum; } - | x -> raise (Marshal_error("status",x)) - -let of_evar s = Element ("evar", [], [PCData s.evar_info]) -let to_evar = function - | Element ("evar", [], data) -> { evar_info = raw_string data; } - | x -> raise (Marshal_error("evar",x)) - -let of_goal g = - let hyp = of_list of_pp g.goal_hyp in - let ccl = of_pp g.goal_ccl in - let id = of_string g.goal_id in - Element ("goal", [], [id; hyp; ccl]) -let to_goal = function - | Element ("goal", [], [id; hyp; ccl]) -> - let hyp = to_list to_pp hyp in - let ccl = to_pp ccl in - let id = to_string id in - { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } - | x -> raise (Marshal_error("goal",x)) - -let of_goals g = - let of_glist = of_list of_goal in - let fg = of_list of_goal g.fg_goals in - let bg = of_list (of_pair of_glist of_glist) g.bg_goals in - let shelf = of_list of_goal g.shelved_goals in - let given_up = of_list of_goal g.given_up_goals in - Element ("goals", [], [fg; bg; shelf; given_up]) -let to_goals = function - | Element ("goals", [], [fg; bg; shelf; given_up]) -> - let to_glist = to_list to_goal in - let fg = to_list to_goal fg in - let bg = to_list (to_pair to_glist to_glist) bg in - let shelf = to_list to_goal shelf in - let given_up = to_list to_goal given_up in - { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; - given_up_goals = given_up } - | x -> raise (Marshal_error("goals",x)) - -let of_coq_info info = - let version = of_string info.coqtop_version in - let protocol = of_string info.protocol_version in - let release = of_string info.release_date in - let compile = of_string info.compile_date in - Element ("coq_info", [], [version; protocol; release; compile]) -let to_coq_info = function - | Element ("coq_info", [], [version; protocol; release; compile]) -> { - coqtop_version = to_string version; - protocol_version = to_string protocol; - release_date = to_string release; - compile_date = to_string compile; } - | x -> raise (Marshal_error("coq_info",x)) - -end -include Xml_marshalling - -(* Reification of basic types and type constructors, and functions - from to xml *) -module ReifType : sig - - type 'a val_t - - val unit_t : unit val_t - val string_t : string val_t - val int_t : int val_t - val bool_t : bool val_t - val xml_t : Xml_datatype.xml val_t - - val option_t : 'a val_t -> 'a option val_t - val list_t : 'a val_t -> 'a list val_t - val pair_t : 'a val_t -> 'b val_t -> ('a * 'b) val_t - val union_t : 'a val_t -> 'b val_t -> ('a ,'b) union val_t - - val goals_t : goals val_t - val evar_t : evar val_t - val state_t : status val_t - val option_state_t : option_state val_t - val option_value_t : option_value val_t - val coq_info_t : coq_info val_t - val coq_object_t : 'a val_t -> 'a coq_object val_t - val state_id_t : state_id val_t - val route_id_t : route_id val_t - val search_cst_t : search_constraint val_t - - val of_value_type : 'a val_t -> 'a -> xml - val to_value_type : 'a val_t -> xml -> 'a - - val print : 'a val_t -> 'a -> string - - type value_type - val erase : 'a val_t -> value_type - val print_type : value_type -> string - - val document_type_encoding : (xml -> string) -> unit - -end = struct - - type _ val_t = - | Unit : unit val_t - | String : string val_t - | Int : int val_t - | Bool : bool val_t - | Xml : Xml_datatype.xml val_t - - | Option : 'a val_t -> 'a option val_t - | List : 'a val_t -> 'a list val_t - | Pair : 'a val_t * 'b val_t -> ('a * 'b) val_t - | Union : 'a val_t * 'b val_t -> ('a, 'b) union val_t - - | Goals : goals val_t - | Evar : evar val_t - | State : status val_t - | Option_state : option_state val_t - | Option_value : option_value val_t - | Coq_info : coq_info val_t - | Coq_object : 'a val_t -> 'a coq_object val_t - | State_id : state_id val_t - | Route_id : route_id val_t - | Search_cst : search_constraint val_t - - type value_type = Value_type : 'a val_t -> value_type - - let erase (x : 'a val_t) = Value_type x - - let unit_t = Unit - let string_t = String - let int_t = Int - let bool_t = Bool - let xml_t = Xml - - let option_t x = Option x - let list_t x = List x - let pair_t x y = Pair (x, y) - let union_t x y = Union (x, y) - - let goals_t = Goals - let evar_t = Evar - let state_t = State - let option_state_t = Option_state - let option_value_t = Option_value - let coq_info_t = Coq_info - let coq_object_t x = Coq_object x - let state_id_t = State_id - let route_id_t = Route_id - let search_cst_t = Search_cst - - let of_value_type (ty : 'a val_t) : 'a -> xml = - let rec convert : type a. a val_t -> a -> xml = function - | Unit -> of_unit - | Bool -> of_bool - | Xml -> (fun x -> x) - | String -> of_string - | Int -> of_int - | State -> of_status - | Option_state -> of_option_state - | Option_value -> of_option_value - | Coq_info -> of_coq_info - | Goals -> of_goals - | Evar -> of_evar - | List t -> (of_list (convert t)) - | Option t -> (of_option (convert t)) - | Coq_object t -> (of_coq_object (convert t)) - | Pair (t1,t2) -> (of_pair (convert t1) (convert t2)) - | Union (t1,t2) -> (of_union (convert t1) (convert t2)) - | State_id -> of_stateid - | Route_id -> of_routeid - | Search_cst -> of_search_cst - in - convert ty - - let to_value_type (ty : 'a val_t) : xml -> 'a = - let rec convert : type a. a val_t -> xml -> a = function - | Unit -> to_unit - | Bool -> to_bool - | Xml -> (fun x -> x) - | String -> to_string - | Int -> to_int - | State -> to_status - | Option_state -> to_option_state - | Option_value -> to_option_value - | Coq_info -> to_coq_info - | Goals -> to_goals - | Evar -> to_evar - | List t -> (to_list (convert t)) - | Option t -> (to_option (convert t)) - | Coq_object t -> (to_coq_object (convert t)) - | Pair (t1,t2) -> (to_pair (convert t1) (convert t2)) - | Union (t1,t2) -> (to_union (convert t1) (convert t2)) - | State_id -> to_stateid - | Route_id -> to_routeid - | Search_cst -> to_search_cst - in - convert ty - - let pr_unit () = "" - let pr_string s = Printf.sprintf "%S" s - let pr_int i = string_of_int i - let pr_bool b = Printf.sprintf "%B" b - let pr_goal (g : goals) = - if g.fg_goals = [] then - if g.bg_goals = [] then "Proof completed." - else - let rec pr_focus _ = function - | [] -> assert false - | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) - | (lg, rg) :: l -> - Printf.sprintf "%i:%a" - (List.length lg + List.length rg) pr_focus l in - Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals - else - let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ - Pp.string_of_ppcmds goal ^ "]" in - String.concat " " (List.map pr_goal g.fg_goals) - let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" - let pr_status (s : status) = - let path = - let l = String.concat "." s.status_path in - "path=" ^ l ^ ";" in - let name = match s.status_proofname with - | None -> "no proof;" - | Some n -> "proof = " ^ n ^ ";" in - "Status: " ^ path ^ name - let pr_coq_info (i : coq_info) = "FIXME" - let pr_option_value = function - | IntValue None -> "none" - | IntValue (Some i) -> string_of_int i - | StringValue s -> s - | StringOptValue None -> "none" - | StringOptValue (Some s) -> s - | BoolValue b -> if b then "true" else "false" - let pr_option_state (s : option_state) = - Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" - s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) - let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]" - let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")" - let pr_coq_object (o : 'a coq_object) = "FIXME" - let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")" - let pr_union pr1 pr2 = function Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x - let pr_state_id = Stateid.to_string - - let pr_search_cst = function - | Name_Pattern s -> "Name_Pattern " ^ s - | Type_Pattern s -> "Type_Pattern " ^ s - | SubType_Pattern s -> "SubType_Pattern " ^ s - | In_Module s -> "In_Module " ^ String.concat "." s - | Include_Blacklist -> "Include_Blacklist" - - let rec print : type a. a val_t -> a -> string = function - | Unit -> pr_unit - | Bool -> pr_bool - | String -> pr_string - | Xml -> Xml_printer.to_string_fmt - | Int -> pr_int - | State -> pr_status - | Option_state -> pr_option_state - | Option_value -> pr_option_value - | Search_cst -> pr_search_cst - | Coq_info -> pr_coq_info - | Goals -> pr_goal - | Evar -> pr_evar - | List t -> (pr_list (print t)) - | Option t -> (pr_option (print t)) - | Coq_object t -> pr_coq_object - | Pair (t1,t2) -> (pr_pair (print t1) (print t2)) - | Union (t1,t2) -> (pr_union (print t1) (print t2)) - | State_id -> pr_state_id - | Route_id -> pr_int - - (* This is to break if a rename/refactoring makes the strings below outdated *) - type 'a exists = bool - - let rec print_val_t : type a. a val_t -> string = function - | Unit -> "unit" - | Bool -> "bool" - | String -> "string" - | Xml -> "xml" - | Int -> "int" - | State -> assert(true : status exists); "Interface.status" - | Option_state -> assert(true : option_state exists); "Interface.option_state" - | Option_value -> assert(true : option_value exists); "Interface.option_value" - | Search_cst -> assert(true : search_constraint exists); "Interface.search_constraint" - | Coq_info -> assert(true : coq_info exists); "Interface.coq_info" - | Goals -> assert(true : goals exists); "Interface.goals" - | Evar -> assert(true : evar exists); "Interface.evar" - | List t -> Printf.sprintf "(%s list)" (print_val_t t) - | Option t -> Printf.sprintf "(%s option)" (print_val_t t) - | Coq_object t -> assert(true : 'a coq_object exists); - Printf.sprintf "(%s Interface.coq_object)" (print_val_t t) - | Pair (t1,t2) -> Printf.sprintf "(%s * %s)" (print_val_t t1) (print_val_t t2) - | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); - Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2) - | State_id -> assert(true : Stateid.t exists); "Stateid.t" - | Route_id -> assert(true : route_id exists); "route_id" - - let print_type = function Value_type ty -> print_val_t ty - - let document_type_encoding pr_xml = - Printf.printf "\n=== Data encoding by examples ===\n\n"; - Printf.printf "%s:\n\n%s\n\n" (print_val_t Unit) (pr_xml (of_unit ())); - Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t Bool) - (pr_xml (of_bool true)) (pr_xml (of_bool false)); - Printf.printf "%s:\n\n%s\n\n" (print_val_t String) (pr_xml (of_string "hello")); - Printf.printf "%s:\n\n%s\n\n" (print_val_t Int) (pr_xml (of_int 256)); - Printf.printf "%s:\n\n%s\n\n" (print_val_t State_id) (pr_xml (of_stateid Stateid.initial)); - Printf.printf "%s:\n\n%s\n\n" (print_val_t (List Int)) (pr_xml (of_list of_int [3;4;5])); - Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t (Option Int)) - (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None)); - Printf.printf "%s:\n\n%s\n\n" (print_val_t (Pair (Bool,Int))) - (pr_xml (of_pair of_bool of_int (false,3))); - Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int))) - (pr_xml (of_union of_bool of_int (Inl false))); - print_endline ("All other types are records represented by a node named like the OCaml\n"^ - "type which contains a flattened n-tuple. We provide one example.\n"); - Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) - (pr_xml (of_option_state { opt_sync = true; opt_depr = false; - opt_name = "name1"; opt_value = IntValue (Some 37) })); - -end -open ReifType - -(** Types reification, checked with explicit casts *) -let add_sty_t : add_sty val_t = - pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t) -let edit_at_sty_t : edit_at_sty val_t = state_id_t -let query_sty_t : query_sty val_t = pair_t route_id_t (pair_t string_t state_id_t) -let goals_sty_t : goals_sty val_t = unit_t -let evars_sty_t : evars_sty val_t = unit_t -let hints_sty_t : hints_sty val_t = unit_t -let status_sty_t : status_sty val_t = bool_t -let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t) -let get_options_sty_t : get_options_sty val_t = unit_t -let set_options_sty_t : set_options_sty val_t = - list_t (pair_t (list_t string_t) option_value_t) -let mkcases_sty_t : mkcases_sty val_t = string_t -let quit_sty_t : quit_sty val_t = unit_t -let wait_sty_t : wait_sty val_t = unit_t -let about_sty_t : about_sty val_t = unit_t -let init_sty_t : init_sty val_t = option_t string_t -let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t -let stop_worker_sty_t : stop_worker_sty val_t = string_t -let print_ast_sty_t : print_ast_sty val_t = state_id_t -let annotate_sty_t : annotate_sty val_t = string_t - -let add_rty_t : add_rty val_t = - pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) -let edit_at_rty_t : edit_at_rty val_t = - union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t)) -let query_rty_t : query_rty val_t = unit_t -let goals_rty_t : goals_rty val_t = option_t goals_t -let evars_rty_t : evars_rty val_t = option_t (list_t evar_t) -let hints_rty_t : hints_rty val_t = - let hint = list_t (pair_t string_t string_t) in - option_t (pair_t (list_t hint) hint) -let status_rty_t : status_rty val_t = state_t -let search_rty_t : search_rty val_t = list_t (coq_object_t string_t) -let get_options_rty_t : get_options_rty val_t = - list_t (pair_t (list_t string_t) option_state_t) -let set_options_rty_t : set_options_rty val_t = unit_t -let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t) -let quit_rty_t : quit_rty val_t = unit_t -let wait_rty_t : wait_rty val_t = unit_t -let about_rty_t : about_rty val_t = coq_info_t -let init_rty_t : init_rty val_t = state_id_t -let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t) -let stop_worker_rty_t : stop_worker_rty val_t = unit_t -let print_ast_rty_t : print_ast_rty val_t = xml_t -let annotate_rty_t : annotate_rty val_t = xml_t - -let ($) x = erase x -let calls = [| - "Add", ($)add_sty_t, ($)add_rty_t; - "Edit_at", ($)edit_at_sty_t, ($)edit_at_rty_t; - "Query", ($)query_sty_t, ($)query_rty_t; - "Goal", ($)goals_sty_t, ($)goals_rty_t; - "Evars", ($)evars_sty_t, ($)evars_rty_t; - "Hints", ($)hints_sty_t, ($)hints_rty_t; - "Status", ($)status_sty_t, ($)status_rty_t; - "Search", ($)search_sty_t, ($)search_rty_t; - "GetOptions", ($)get_options_sty_t, ($)get_options_rty_t; - "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t; - "MkCases", ($)mkcases_sty_t, ($)mkcases_rty_t; - "Quit", ($)quit_sty_t, ($)quit_rty_t; - "Wait", ($)wait_sty_t, ($)wait_rty_t; - "About", ($)about_sty_t, ($)about_rty_t; - "Init", ($)init_sty_t, ($)init_rty_t; - "Interp", ($)interp_sty_t, ($)interp_rty_t; - "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t; - "PrintAst", ($)print_ast_sty_t, ($)print_ast_rty_t; - "Annotate", ($)annotate_sty_t, ($)annotate_rty_t; -|] - -type 'a call = - | Add : add_sty -> add_rty call - | Edit_at : edit_at_sty -> edit_at_rty call - | Query : query_sty -> query_rty call - | Goal : goals_sty -> goals_rty call - | Evars : evars_sty -> evars_rty call - | Hints : hints_sty -> hints_rty call - | Status : status_sty -> status_rty call - | Search : search_sty -> search_rty call - | GetOptions : get_options_sty -> get_options_rty call - | SetOptions : set_options_sty -> set_options_rty call - | MkCases : mkcases_sty -> mkcases_rty call - | Quit : quit_sty -> quit_rty call - | About : about_sty -> about_rty call - | Init : init_sty -> init_rty call - | StopWorker : stop_worker_sty -> stop_worker_rty call - (* internal use (fake_ide) only, do not use *) - | Wait : wait_sty -> wait_rty call - (* retrocompatibility *) - | Interp : interp_sty -> interp_rty call - | PrintAst : print_ast_sty -> print_ast_rty call - | Annotate : annotate_sty -> annotate_rty call - -let id_of_call : type a. a call -> int = function - | Add _ -> 0 - | Edit_at _ -> 1 - | Query _ -> 2 - | Goal _ -> 3 - | Evars _ -> 4 - | Hints _ -> 5 - | Status _ -> 6 - | Search _ -> 7 - | GetOptions _ -> 8 - | SetOptions _ -> 9 - | MkCases _ -> 10 - | Quit _ -> 11 - | Wait _ -> 12 - | About _ -> 13 - | Init _ -> 14 - | Interp _ -> 15 - | StopWorker _ -> 16 - | PrintAst _ -> 17 - | Annotate _ -> 18 - -let str_of_call c = pi1 calls.(id_of_call c) - -type unknown_call = Unknown : 'a call -> unknown_call - -(** We use phantom types and GADT to protect ourselves against wild casts *) -let add x : add_rty call = Add x -let edit_at x : edit_at_rty call = Edit_at x -let query x : query_rty call = Query x -let goals x : goals_rty call = Goal x -let evars x : evars_rty call = Evars x -let hints x : hints_rty call = Hints x -let status x : status_rty call = Status x -let get_options x : get_options_rty call = GetOptions x -let set_options x : set_options_rty call = SetOptions x -let mkcases x : mkcases_rty call = MkCases x -let search x : search_rty call = Search x -let quit x : quit_rty call = Quit x -let init x : init_rty call = Init x -let wait x : wait_rty call = Wait x -let interp x : interp_rty call = Interp x -let stop_worker x : stop_worker_rty call = StopWorker x -let print_ast x : print_ast_rty call = PrintAst x -let annotate x : annotate_rty call = Annotate x - -let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> - let mkGood : type a. a -> a value = fun x -> Good x in - try - match c with - | Add x -> mkGood (handler.add x) - | Edit_at x -> mkGood (handler.edit_at x) - | Query x -> mkGood (handler.query x) - | Goal x -> mkGood (handler.goals x) - | Evars x -> mkGood (handler.evars x) - | Hints x -> mkGood (handler.hints x) - | Status x -> mkGood (handler.status x) - | Search x -> mkGood (handler.search x) - | GetOptions x -> mkGood (handler.get_options x) - | SetOptions x -> mkGood (handler.set_options x) - | MkCases x -> mkGood (handler.mkcases x) - | Quit x -> mkGood (handler.quit x) - | Wait x -> mkGood (handler.wait x) - | About x -> mkGood (handler.about x) - | Init x -> mkGood (handler.init x) - | Interp x -> mkGood (handler.interp x) - | StopWorker x -> mkGood (handler.stop_worker x) - | PrintAst x -> mkGood (handler.print_ast x) - | Annotate x -> mkGood (handler.annotate x) - with any -> - let any = CErrors.push any in - Fail (handler.handle_exn any) - -(** brain dead code, edit if protocol messages are added/removed *) -let of_answer : type a. a call -> a value -> xml = function - | Add _ -> of_value (of_value_type add_rty_t ) - | Edit_at _ -> of_value (of_value_type edit_at_rty_t ) - | Query _ -> of_value (of_value_type query_rty_t ) - | Goal _ -> of_value (of_value_type goals_rty_t ) - | Evars _ -> of_value (of_value_type evars_rty_t ) - | Hints _ -> of_value (of_value_type hints_rty_t ) - | Status _ -> of_value (of_value_type status_rty_t ) - | Search _ -> of_value (of_value_type search_rty_t ) - | GetOptions _ -> of_value (of_value_type get_options_rty_t) - | SetOptions _ -> of_value (of_value_type set_options_rty_t) - | MkCases _ -> of_value (of_value_type mkcases_rty_t ) - | Quit _ -> of_value (of_value_type quit_rty_t ) - | Wait _ -> of_value (of_value_type wait_rty_t ) - | About _ -> of_value (of_value_type about_rty_t ) - | Init _ -> of_value (of_value_type init_rty_t ) - | Interp _ -> of_value (of_value_type interp_rty_t ) - | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) - | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) - | Annotate _ -> of_value (of_value_type annotate_rty_t ) - -let of_answer msg_fmt = - msg_format := msg_fmt; of_answer - -let to_answer : type a. a call -> xml -> a value = function - | Add _ -> to_value (to_value_type add_rty_t ) - | Edit_at _ -> to_value (to_value_type edit_at_rty_t ) - | Query _ -> to_value (to_value_type query_rty_t ) - | Goal _ -> to_value (to_value_type goals_rty_t ) - | Evars _ -> to_value (to_value_type evars_rty_t ) - | Hints _ -> to_value (to_value_type hints_rty_t ) - | Status _ -> to_value (to_value_type status_rty_t ) - | Search _ -> to_value (to_value_type search_rty_t ) - | GetOptions _ -> to_value (to_value_type get_options_rty_t) - | SetOptions _ -> to_value (to_value_type set_options_rty_t) - | MkCases _ -> to_value (to_value_type mkcases_rty_t ) - | Quit _ -> to_value (to_value_type quit_rty_t ) - | Wait _ -> to_value (to_value_type wait_rty_t ) - | About _ -> to_value (to_value_type about_rty_t ) - | Init _ -> to_value (to_value_type init_rty_t ) - | Interp _ -> to_value (to_value_type interp_rty_t ) - | StopWorker _ -> to_value (to_value_type stop_worker_rty_t) - | PrintAst _ -> to_value (to_value_type print_ast_rty_t ) - | Annotate _ -> to_value (to_value_type annotate_rty_t ) - -let of_call : type a. a call -> xml = fun q -> - let mkCall x = constructor "call" (str_of_call q) [x] in - match q with - | Add x -> mkCall (of_value_type add_sty_t x) - | Edit_at x -> mkCall (of_value_type edit_at_sty_t x) - | Query x -> mkCall (of_value_type query_sty_t x) - | Goal x -> mkCall (of_value_type goals_sty_t x) - | Evars x -> mkCall (of_value_type evars_sty_t x) - | Hints x -> mkCall (of_value_type hints_sty_t x) - | Status x -> mkCall (of_value_type status_sty_t x) - | Search x -> mkCall (of_value_type search_sty_t x) - | GetOptions x -> mkCall (of_value_type get_options_sty_t x) - | SetOptions x -> mkCall (of_value_type set_options_sty_t x) - | MkCases x -> mkCall (of_value_type mkcases_sty_t x) - | Quit x -> mkCall (of_value_type quit_sty_t x) - | Wait x -> mkCall (of_value_type wait_sty_t x) - | About x -> mkCall (of_value_type about_sty_t x) - | Init x -> mkCall (of_value_type init_sty_t x) - | Interp x -> mkCall (of_value_type interp_sty_t x) - | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x) - | PrintAst x -> mkCall (of_value_type print_ast_sty_t x) - | Annotate x -> mkCall (of_value_type annotate_sty_t x) - -let to_call : xml -> unknown_call = - do_match "call" (fun s a -> - let mkCallArg vt a = to_value_type vt (singleton a) in - match s with - | "Add" -> Unknown (Add (mkCallArg add_sty_t a)) - | "Edit_at" -> Unknown (Edit_at (mkCallArg edit_at_sty_t a)) - | "Query" -> Unknown (Query (mkCallArg query_sty_t a)) - | "Goal" -> Unknown (Goal (mkCallArg goals_sty_t a)) - | "Evars" -> Unknown (Evars (mkCallArg evars_sty_t a)) - | "Hints" -> Unknown (Hints (mkCallArg hints_sty_t a)) - | "Status" -> Unknown (Status (mkCallArg status_sty_t a)) - | "Search" -> Unknown (Search (mkCallArg search_sty_t a)) - | "GetOptions" -> Unknown (GetOptions (mkCallArg get_options_sty_t a)) - | "SetOptions" -> Unknown (SetOptions (mkCallArg set_options_sty_t a)) - | "MkCases" -> Unknown (MkCases (mkCallArg mkcases_sty_t a)) - | "Quit" -> Unknown (Quit (mkCallArg quit_sty_t a)) - | "Wait" -> Unknown (Wait (mkCallArg wait_sty_t a)) - | "About" -> Unknown (About (mkCallArg about_sty_t a)) - | "Init" -> Unknown (Init (mkCallArg init_sty_t a)) - | "Interp" -> Unknown (Interp (mkCallArg interp_sty_t a)) - | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a)) - | "PrintAst" -> Unknown (PrintAst (mkCallArg print_ast_sty_t a)) - | "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a)) - | x -> raise (Marshal_error("call",PCData x))) - -(** Debug printing *) - -let pr_value_gen pr = function - | Good v -> "GOOD " ^ pr v - | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]" - | Fail (id,Some(i,j),str) -> - "FAIL "^Stateid.to_string id^ - " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]" -let pr_value v = pr_value_gen (fun _ -> "FIXME") v -let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with - | Add _ -> pr_value_gen (print add_rty_t ) value - | Edit_at _ -> pr_value_gen (print edit_at_rty_t ) value - | Query _ -> pr_value_gen (print query_rty_t ) value - | Goal _ -> pr_value_gen (print goals_rty_t ) value - | Evars _ -> pr_value_gen (print evars_rty_t ) value - | Hints _ -> pr_value_gen (print hints_rty_t ) value - | Status _ -> pr_value_gen (print status_rty_t ) value - | Search _ -> pr_value_gen (print search_rty_t ) value - | GetOptions _ -> pr_value_gen (print get_options_rty_t) value - | SetOptions _ -> pr_value_gen (print set_options_rty_t) value - | MkCases _ -> pr_value_gen (print mkcases_rty_t ) value - | Quit _ -> pr_value_gen (print quit_rty_t ) value - | Wait _ -> pr_value_gen (print wait_rty_t ) value - | About _ -> pr_value_gen (print about_rty_t ) value - | Init _ -> pr_value_gen (print init_rty_t ) value - | Interp _ -> pr_value_gen (print interp_rty_t ) value - | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value - | PrintAst _ -> pr_value_gen (print print_ast_rty_t ) value - | Annotate _ -> pr_value_gen (print annotate_rty_t ) value -let pr_call : type a. a call -> string = fun call -> - let return what x = str_of_call call ^ " " ^ print what x in - match call with - | Add x -> return add_sty_t x - | Edit_at x -> return edit_at_sty_t x - | Query x -> return query_sty_t x - | Goal x -> return goals_sty_t x - | Evars x -> return evars_sty_t x - | Hints x -> return hints_sty_t x - | Status x -> return status_sty_t x - | Search x -> return search_sty_t x - | GetOptions x -> return get_options_sty_t x - | SetOptions x -> return set_options_sty_t x - | MkCases x -> return mkcases_sty_t x - | Quit x -> return quit_sty_t x - | Wait x -> return wait_sty_t x - | About x -> return about_sty_t x - | Init x -> return init_sty_t x - | Interp x -> return interp_sty_t x - | StopWorker x -> return stop_worker_sty_t x - | PrintAst x -> return print_ast_sty_t x - | Annotate x -> return annotate_sty_t x - -let document to_string_fmt = - Printf.printf "=== Available calls ===\n\n"; - Array.iter (fun (cname, csty, crty) -> - Printf.printf "%12s : %s\n %14s %s\n" - ("\""^cname^"\"") (print_type csty) "->" (print_type crty)) - calls; - Printf.printf "\n=== Calls XML encoding ===\n\n"; - Printf.printf "A call \"C\" carrying input a is encoded as:\n\n%s\n\n" - (to_string_fmt (constructor "call" "C" [PCData "a"])); - Printf.printf "A response carrying output b can either be:\n\n%s\n\n" - (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); - Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" - (to_string_fmt (of_value (fun _ -> PCData "b") - (Fail (Stateid.initial,Some (15,34), Pp.str "error message")))); - document_type_encoding to_string_fmt - -(* Moved from feedback.mli : This is IDE specific and we don't want to - pollute the core with it *) - -open Feedback - -let of_message_level = function - | Debug -> - Serialize.constructor "message_level" "debug" [] - | Info -> Serialize.constructor "message_level" "info" [] - | Notice -> Serialize.constructor "message_level" "notice" [] - | Warning -> Serialize.constructor "message_level" "warning" [] - | Error -> Serialize.constructor "message_level" "error" [] -let to_message_level = - Serialize.do_match "message_level" (fun s args -> match s with - | "debug" -> Debug - | "info" -> Info - | "notice" -> Notice - | "warning" -> Warning - | "error" -> Error - | x -> raise Serialize.(Marshal_error("error level",PCData x))) - -let of_message lvl loc msg = - let lvl = of_message_level lvl in - let xloc = of_option of_loc loc in - let content = of_pp msg in - Xml_datatype.Element ("message", [], [lvl; xloc; content]) - -let to_message xml = match xml with - | Xml_datatype.Element ("message", [], [lvl; xloc; content]) -> - Message(to_message_level lvl, to_option to_loc xloc, to_pp content) - | x -> raise (Marshal_error("message",x)) - -let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with - | "addedaxiom", _ -> AddedAxiom - | "processed", _ -> Processed - | "processingin", [where] -> ProcessingIn (to_string where) - | "incomplete", _ -> Incomplete - | "complete", _ -> Complete - | "globref", [loc; filepath; modpath; ident; ty] -> - GlobRef(to_loc loc, to_string filepath, - to_string modpath, to_string ident, to_string ty) - | "globdef", [loc; ident; secpath; ty] -> - GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) - | "inprogress", [n] -> InProgress (to_int n) - | "workerstatus", [ns] -> - let n, s = to_pair to_string to_string ns in - WorkerStatus(n,s) - | "custom", [loc;name;x]-> Custom (to_option to_loc loc, to_string name, x) - | "filedependency", [from; dep] -> - FileDependency (to_option to_string from, to_string dep) - | "fileloaded", [dirpath; filename] -> - FileLoaded (to_string dirpath, to_string filename) - | "message", [x] -> to_message x - | x,l -> raise (Marshal_error("feedback_content",PCData (x ^ " with attributes " ^ string_of_int (List.length l))))) - -let of_feedback_content = function - | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] - | Processed -> constructor "feedback_content" "processed" [] - | ProcessingIn where -> - constructor "feedback_content" "processingin" [of_string where] - | Incomplete -> constructor "feedback_content" "incomplete" [] - | Complete -> constructor "feedback_content" "complete" [] - | GlobRef(loc, filepath, modpath, ident, ty) -> - constructor "feedback_content" "globref" [ - of_loc loc; - of_string filepath; - of_string modpath; - of_string ident; - of_string ty ] - | GlobDef(loc, ident, secpath, ty) -> - constructor "feedback_content" "globdef" [ - of_loc loc; - of_string ident; - of_string secpath; - of_string ty ] - | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] - | WorkerStatus(n,s) -> - constructor "feedback_content" "workerstatus" - [of_pair of_string of_string (n,s)] - | Custom (loc, name, x) -> - constructor "feedback_content" "custom" [of_option of_loc loc; of_string name; x] - | FileDependency (from, depends_on) -> - constructor "feedback_content" "filedependency" [ - of_option of_string from; - of_string depends_on] - | FileLoaded (dirpath, filename) -> - constructor "feedback_content" "fileloaded" [ - of_string dirpath; - of_string filename ] - | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ] - -let of_edit_or_state_id id = ["object","state"], of_stateid id - -let of_feedback msg = - let content = of_feedback_content msg.contents in - let obj, id = of_edit_or_state_id msg.span_id in - let route = string_of_int msg.route in - Element ("feedback", obj @ ["route",route], [id;content]) - -let of_feedback msg_fmt = - msg_format := msg_fmt; of_feedback - -let to_feedback xml = match xml with - | Element ("feedback", ["object","state";"route",route], [id;content]) -> { - doc_id = 0; - span_id = to_stateid id; - route = int_of_string route; - contents = to_feedback_content content } - | x -> raise (Marshal_error("feedback",x)) - -let is_feedback = function - | Element ("feedback", _, _) -> true - | _ -> false - -(* vim: set foldmethod=marker: *) - diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli deleted file mode 100644 index ba6000f0a..000000000 --- a/ide/xmlprotocol.mli +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* unknown_call - -val add : add_sty -> add_rty call -val edit_at : edit_at_sty -> edit_at_rty call -val query : query_sty -> query_rty call -val goals : goals_sty -> goals_rty call -val hints : hints_sty -> hints_rty call -val status : status_sty -> status_rty call -val mkcases : mkcases_sty -> mkcases_rty call -val evars : evars_sty -> evars_rty call -val search : search_sty -> search_rty call -val get_options : get_options_sty -> get_options_rty call -val set_options : set_options_sty -> set_options_rty call -val quit : quit_sty -> quit_rty call -val init : init_sty -> init_rty call -val stop_worker : stop_worker_sty -> stop_worker_rty call -(* internal use (fake_ide) only, do not use *) -val wait : wait_sty -> wait_rty call -(* retrocompatibility *) -val interp : interp_sty -> interp_rty call -val print_ast : print_ast_sty -> print_ast_rty call -val annotate : annotate_sty -> annotate_rty call - -val abstract_eval_call : handler -> 'a call -> 'a value - -(** * Protocol version *) - -val protocol_version : string - -(** By default, we still output messages in Richpp so we are - compatible with 8.6, however, 8.7 aware clients will want to - set this to Ppcmds *) -type msg_format = Richpp of int | Ppcmds - -(** * XML data marshalling *) - -val of_call : 'a call -> xml -val to_call : xml -> unknown_call - -val of_answer : msg_format -> 'a call -> 'a value -> xml -val to_answer : 'a call -> xml -> 'a value - -(* Prints the documentation of this module *) -val document : (xml -> string) -> unit - -(** * Debug printing *) - -val pr_call : 'a call -> string -val pr_value : 'a value -> string -val pr_full_value : 'a call -> 'a value -> string - -(** * Serializaiton of feedback *) -val of_feedback : msg_format -> Feedback.feedback -> xml -val to_feedback : xml -> Feedback.feedback - -val is_feedback : xml -> bool -- cgit v1.2.3