From 72aedfaa40e8b6995aa9fca78cba52013199e0b1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 30 Nov 2001 17:16:28 +0000 Subject: [PATCH] cicAnnotationHinter.ml* have no reason to be in the library. In this way, the dependency from lablgtk is removed. --- helm/ocaml/META.helm-cic_annotations.src | 2 +- helm/ocaml/cic_annotations/Makefile | 6 +- .../cic_annotations/cicAnnotationHinter.ml | 381 ------------------ .../cic_annotations/cicAnnotationHinter.mli | 46 --- 4 files changed, 4 insertions(+), 431 deletions(-) delete mode 100644 helm/ocaml/cic_annotations/cicAnnotationHinter.ml delete mode 100644 helm/ocaml/cic_annotations/cicAnnotationHinter.mli diff --git a/helm/ocaml/META.helm-cic_annotations.src b/helm/ocaml/META.helm-cic_annotations.src index ec5462fe7..829efba0d 100644 --- a/helm/ocaml/META.helm-cic_annotations.src +++ b/helm/ocaml/META.helm-cic_annotations.src @@ -1,4 +1,4 @@ -requires="helm-cic helm-xml lablgtk" +requires="helm-cic helm-xml" version="0.0.1" archive(byte)="cic_annotations.cma" archive(native)="cic_annotations.cmxa" diff --git a/helm/ocaml/cic_annotations/Makefile b/helm/ocaml/cic_annotations/Makefile index 1b85d96bc..1627b11e3 100644 --- a/helm/ocaml/cic_annotations/Makefile +++ b/helm/ocaml/cic_annotations/Makefile @@ -1,9 +1,9 @@ PACKAGE = cic_annotations -REQUIRES = helm-cic helm-xml lablgtk +REQUIRES = helm-cic helm-xml PREDICATES = -INTERFACE_FILES = cicAnnotation2Xml.mli cicAnnotationHinter.mli \ - cicAnnotationParser2.mli cicAnnotationParser.mli cicXPath.mli +INTERFACE_FILES = cicAnnotation2Xml.mli cicAnnotationParser2.mli \ + cicAnnotationParser.mli cicXPath.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/ocaml/cic_annotations/cicAnnotationHinter.ml b/helm/ocaml/cic_annotations/cicAnnotationHinter.ml deleted file mode 100644 index 86bcb4588..000000000 --- a/helm/ocaml/cic_annotations/cicAnnotationHinter.ml +++ /dev/null @@ -1,381 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM 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 General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 14/06/2000 *) -(* *) -(* *) -(******************************************************************************) - -let deactivate_hints_from annotation_window n = - let annotation_hints = annotation_window#annotation_hints in - for i = n to Array.length annotation_hints - 1 do - annotation_hints.(i)#misc#hide () - done -;; - -(* CSC: orripilante *) -(* the list of the signal ids *) -let sig_ids = ref ([] : GtkSignal.id list);; - -let disconnect_hint annotation_window buttonno = - match !sig_ids with - id::ids -> - annotation_window#annotation_hints.(buttonno)#misc#disconnect id ; - sig_ids := ids - | _ -> assert false -;; - -(* link_hint annotation_window n label hint *) -(* set the label of the nth hint button of annotation_window to label *) -(* and the correspondent hint to hint *) -let link_hint annotation_window buttonno label hint = - let button = annotation_window#annotation_hints.(buttonno) in - sig_ids := - (button#connect#clicked - (fun () -> (annotation_window#annotation : GEdit.text)#insert hint) - ) :: !sig_ids ; - button#misc#show () ; - match button#children with - [labelw] -> (GMisc.label_cast labelw)#set_text label - | _ -> assert false -;; - -exception TooManyHints;; - -let link_hints annotation_window a = - if Array.length a > Array.length annotation_window#annotation_hints then - raise TooManyHints ; - for i = List.length !sig_ids - 1 downto 0 do - disconnect_hint annotation_window i - done ; - Array.iteri - (fun i (label,hint) -> link_hint annotation_window i label hint) a ; - deactivate_hints_from annotation_window (Array.length a) -;; - -let list_mapi f = - let rec aux n = - function - [] -> [] - | he::tl -> (f n he)::(aux (n + 1) tl) - in - aux 0 -;; - -let get_id annterm = - let module C = Cic in - match annterm with - C.ARel (id,_,_,_) -> id - | C.AVar (id,_,_) -> id - | C.AMeta (id,_,_) -> id - | C.ASort (id,_,_) -> id - | C.AImplicit (id,_) -> id - | C.ACast (id,_,_,_) -> id - | C.AProd (id,_,_,_,_) -> id - | C.ALambda (id,_,_,_,_) -> id - | C.ALetIn (id,_,_,_,_) -> id - | C.AAppl (id,_,_) -> id - | C.AConst (id,_,_,_) -> id - | C.AAbst (id,_,_) -> id - | C.AMutInd (id,_,_,_,_) -> id - | C.AMutConstruct (id,_,_,_,_,_)-> id - | C.AMutCase (id,_,_,_,_,_,_,_) -> id - | C.AFix (id,_,_,_) -> id - | C.ACoFix (id,_,_,_) -> id -;; - -let create_hint_from_term annotation_window annterm = - let module C = Cic in - match annterm with - C.ARel (id,_,_,_) -> - link_hints annotation_window - [| "Binder", "" |] - | C.AVar (id,_,_) -> - link_hints annotation_window - [| "relURI???", "" |] - | C.AMeta (id,_,_) -> - link_hints annotation_window - [| "Number", "" |] - | C.ASort (id,_,_) -> - link_hints annotation_window - [| "Value", "" |] - | C.AImplicit (id,_) -> - link_hints annotation_window [| |] - | C.ACast (id,_,bo,ty) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Body", "" ; - "Type", "" - |] - | C.AProd (id,_,_,ty,bo) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Binder", - "" ; - "Body", "" ; - "Type", "" - |] - | C.ALambda (id,_,_,ty,bo) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Binder", - "" ; - "Body", "" ; - "Type", "" - |] - | C.ALetIn (id,_,_,ty,bo) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Binder", - "" ; - "Term", "" ; - "Target", "" - |] - | C.AAppl (id,_,args) -> - let argsid = - Array.mapi - (fun i te -> "Argument " ^ string_of_int i, "") - (Array.of_list args) - in - link_hints annotation_window argsid - | C.AConst (id,_,_,_) -> - link_hints annotation_window - [| "Uri???", "" |] - | C.AAbst (id,_,_) -> - link_hints annotation_window - [| "Uri???", "" |] - | C.AMutInd (id,_,_,_,_) -> - link_hints annotation_window - [| "Uri???", "" |] - | C.AMutConstruct (id,_,_,_,_,_) -> - link_hints annotation_window - [| "Uri???", "" |] - | C.AMutCase (id,_,_,_,_,outty,te,pl) -> - let outtyid = get_id outty - and teid = get_id te - and plid = - Array.mapi - (fun i te -> "Pattern " ^ string_of_int i, "") - (Array.of_list pl) - in - link_hints annotation_window - (Array.append - [| "Uri???", "" ; - "Case Type", "" ; - "Term", "" ; - |] - plid) - | C.AFix (id,_,_,funl) -> - let funtylid = - Array.mapi - (fun i (_,_,ty,_) -> - "Type " ^ string_of_int i, "") - (Array.of_list funl) - and funbolid = - Array.mapi - (fun i (_,_,_,bo) -> - "Body " ^ string_of_int i, "") - (Array.of_list funl) - and funnamel = - Array.mapi - (fun i (_,_,_,_) -> - "Name " ^ string_of_int i, "") - (Array.of_list funl) - and funrecindexl = - Array.mapi - (fun i (_,_,_,_) -> - "Recursive Index??? " ^ string_of_int i, "") - (Array.of_list funl) - in - link_hints annotation_window - (Array.concat - [ funtylid ; - funbolid ; - funnamel ; - funrecindexl ; - [| "NoFun???", "" |] - ] - ) - | C.ACoFix (id,_,_,funl) -> - let funtylid = - Array.mapi - (fun i (_,ty,_) -> - "Type " ^ string_of_int i, "") - (Array.of_list funl) - and funbolid = - Array.mapi - (fun i (_,_,bo) -> - "Body " ^ string_of_int i, "") - (Array.of_list funl) - and funnamel = - Array.mapi - (fun i (_,_,_) -> - "Name " ^ string_of_int i, "") - (Array.of_list funl) - in - link_hints annotation_window - (Array.concat - [ funtylid ; - funbolid ; - funnamel ; - [| "NoFun???", "" |] - ] - ) -;; - -(*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *) -let create_hint_from_obj annotation_window annobj = - let module C = Cic in - match annobj with - C.ADefinition (id,_,_,bo,ty,_) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Name", "" ; - "Ingredients", "" ; - "Body", "" ; - "Type", "" - |] - | C.AAxiom (id,_,_,ty,_) -> - let tyid = get_id ty in - link_hints annotation_window - [| "Name", "" ; - "Ingredients", "" ; - "Type", "" - |] - | C.AVariable (id,_,_,bo,ty) -> - let tyid = get_id ty in - link_hints annotation_window - (match bo with - None -> - [| "Name", "" ; - "Type", "" - |] - | Some bo -> - let boid = get_id bo in - [| "Name", "" ; - "Body", "" ; - "Type", "" - |] - ) - | C.ACurrentProof (id,_,_,conjs,bo,ty) -> - let boid = get_id bo - and tyid = get_id ty - and conjsid = List.map (fun (_,te) -> get_id te) conjs in - link_hints annotation_window - (Array.append - [| "Name", "" ; - "Ingredients", "" ; - "Body", "" ; - "Type", "" - |] - (Array.mapi - (fun i id -> - "Conjecture " ^ string_of_int i, "" - ) (Array.of_list conjsid) - ) - ) - | C.AInductiveDefinition (id,_,itl,_,_) -> - let itlids = - List.map - (fun (_,_,arity,cons) -> - get_id arity, - List.map (fun (_,ty,_) -> get_id ty) cons - ) itl - in - link_hints annotation_window - (Array.concat - [ - [| "Ingredients","" |]; - (Array.mapi - (fun i _ -> - "Type Name " ^ string_of_int i, - "" - ) (Array.of_list itlids) - ) ; - (Array.mapi - (fun i (id,_) -> - "Type " ^ string_of_int i, "" - ) (Array.of_list itlids) - ) ; - (Array.concat - (list_mapi - (fun i (_,consid) -> - (Array.mapi - (fun j _ -> - "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j, - "" - ) (Array.of_list consid) - ) ; - ) itlids - ) - ) ; - (Array.concat - (list_mapi - (fun i (_,consid) -> - (Array.mapi - (fun j id -> - "Constructor " ^ string_of_int i ^ " " ^ string_of_int j, - "" - ) (Array.of_list consid) - ) ; - ) itlids - ) - ) - ] - ) -;; - -exception IdUnknown of string;; - -let create_hints annotation_window (annobj,ids_to_targets) xpath = - try - match Hashtbl.find ids_to_targets xpath with - Cic.Object annobj -> create_hint_from_obj annotation_window annobj - | Cic.Term annterm -> create_hint_from_term annotation_window annterm - with - Not_found -> raise (IdUnknown xpath) -;; diff --git a/helm/ocaml/cic_annotations/cicAnnotationHinter.mli b/helm/ocaml/cic_annotations/cicAnnotationHinter.mli deleted file mode 100644 index 6846273b3..000000000 --- a/helm/ocaml/cic_annotations/cicAnnotationHinter.mli +++ /dev/null @@ -1,46 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM 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 General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/11/2000 *) -(* *) -(* *) -(******************************************************************************) - -val create_hints : - < annotation : GEdit.text; - annotation_hints : < children : < as_widget : 'a Gtk.obj; .. > list; - connect : < clicked : (unit -> unit) -> GtkSignal.id; - .. >; - misc : < disconnect : GtkSignal.id -> 'b; - hide : unit -> 'c; show : unit -> 'd; .. >; - .. > - array; - .. > -> - 'e * (string, Cic.anntarget) Hashtbl.t -> string -> unit -- 2.39.2