(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
-let annotated_obj = ref None;; (* reference to a couple option where *)
+let annotated_obj = ref None;; (* reference to a triple option where *)
(* the first component is the current *)
- (* annotated object and the second is *)
- (* the map from ids to annotated targets *)
-let ann = ref (ref None);; (* current annotation *)
+ (* annotated object, the second is the *)
+ (* map from ids to annotated targets and *)
+ (* the third is the map from ids to *)
+ (* annotations. *)
+let current_id = ref None;; (* id of the element to annotate *)
let radio_some_status = ref false;; (* is the radio_some button selected? *)
let current_url = ref "";;
match !annotated_obj with
None ->
let annobj =
- (CicCache.get_annobj (get_current_uri ()))
+ let (annobj,ids_to_annotations) =
+ match CicCache.get_annobj (get_current_uri ()) with
+ (annobj,None) -> annobj, Hashtbl.create 503
+ | (annobj, Some ids_to_annotations) -> (annobj,ids_to_annotations)
+ in
+ let ids_to_targets = CicXPath.get_ids_to_targets annobj in
+ (annobj,ids_to_targets,ids_to_annotations)
in
annotated_obj := Some annobj ;
annobj
begin
match (node#get_attribute_ns (O.o_mDOMString_of_string "xref") helmns) with
Some xpath ->
- let annobj = get_annotated_obj ()
- and annotation = (annotation_window#annotation : GEdit.text) in
- ann := CicXPath.get_annotation annobj (xpath#get_string) ;
- CicAnnotationHinter.create_hints annotation_window annobj
- (xpath#get_string) ;
- annotation#delete_text 0 annotation#length ;
- begin
- match !(!ann) with
- None ->
- annotation#misc#set_sensitive false ;
- annotation_window#radio_none#set_active true ;
- radio_some_status := false
- | Some ann' ->
- annotation#insert ann' ;
- annotation#misc#set_sensitive true ;
- annotation_window#radio_some#set_active true ;
- radio_some_status := true
- end ;
- GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
- annotation_window#show () ;
+ let annobj = get_annotated_obj () in
+ let (anno, ids_to_targets, ids_to_annotations) = annobj in
+ let annotation = (annotation_window#annotation : GEdit.text) in
+ let id = xpath#get_string in
+ current_id := Some id ;
+ let ann = CicXPath.get_annotation ids_to_annotations id in
+ CicAnnotationHinter.create_hints annotation_window ids_to_targets
+ (xpath#get_string) ;
+ annotation#delete_text 0 annotation#length ;
+ begin
+ match ann with
+ None ->
+ annotation#misc#set_sensitive false ;
+ annotation_window#radio_none#set_active true ;
+ radio_some_status := false
+ | Some ann' ->
+ annotation#insert ann' ;
+ annotation#misc#set_sensitive true ;
+ annotation_window#radio_some#set_active true ;
+ radio_some_status := true
+ end ;
+ GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
+ annotation_window#show () ;
| None -> rendering_window#label#set_text ("ERROR: No xref found!!!\n")
end
| None -> rendering_window#label#set_text ("ERROR: No selection!!!\n")
;;
+let change_annotation ids_to_annotations id ann =
+ begin
+ try
+ Hashtbl.remove ids_to_annotations id
+ with
+ Not_found -> ()
+ end ;
+ match ann with
+ None -> ()
+ | Some ann' -> Hashtbl.add ids_to_annotations id ann'
+;;
+
(* called when the annotation is confirmed *)
let save_annotation annotation =
let module S = Str in
let module U = UriManager in
- if !radio_some_status then
- !ann := Some (annotation#get_chars 0 annotation#length)
- else
- !ann := None ;
- match !annotated_obj with
- None -> assert false
- | Some (annobj,_) ->
- let uri = get_current_uri () in
- let annxml = CicAnnotation2Xml.pp_annotation annobj uri in
- make_dirs
- (pathname_of_annuri (U.buri_of_uri uri)) ;
- Xml.pp ~quiet:true annxml
- (Some
- (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^
- ".xml"
- )
- )
+ let (annobj,ids_to_annotations) =
+ match !annotated_obj with
+ None -> assert false
+ | Some (annobj,_,ids_to_annotations) -> annobj,ids_to_annotations
+ in
+ change_annotation ids_to_annotations
+ (match !current_id with
+ Some id -> id
+ | None -> assert false
+ )
+ (if !radio_some_status then
+ Some (annotation#get_chars 0 annotation#length)
+ else
+ None
+ ) ;
+ let uri = get_current_uri () in
+ let annxml =
+ CicAnnotation2Xml.pp_annotation annobj ids_to_annotations uri
+ in
+ make_dirs
+ (pathname_of_annuri (U.buri_of_uri uri)) ;
+ Xml.pp ~quiet:true annxml
+ (Some
+ (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^
+ ".xml"
+ )
+ )
;;
(* STUFF TO BUILD THE GTK INTERFACE *)
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
+ C.ARel (id,_,_)
+ | C.AVar (id,_)
+ | C.AMeta (id,_)
+ | C.ASort (id,_)
+ | C.AImplicit id
+ | C.ACast (id,_,_)
+ | C.AProd (id,_,_,_)
+ | C.ALambda (id,_,_,_)
+ | C.ALetIn (id,_,_,_)
+ | C.AAppl (id,_)
+ | C.AConst (id,_,_)
+ | C.AAbst (id,_)
+ | C.AMutInd (id,_,_,_)
+ | C.AMutConstruct (id,_,_,_,_)
+ | C.AMutCase (id,_,_,_,_,_,_)
+ | C.AFix (id,_,_)
+ | C.ACoFix (id,_,_) -> id
;;
let create_hint_from_term annotation_window annterm =
let module C = Cic in
match annterm with
- C.ARel (id,_,_,_) ->
+ C.ARel (id,_,_) ->
link_hints annotation_window
[| "Binder", "<attribute name = 'binder' id = '" ^ id ^ "'/>" |]
- | C.AVar (id,_,_) ->
+ | C.AVar (id,_) ->
link_hints annotation_window
[| "relURI???", "<attribute name = 'relUri' id = '" ^ id ^ "'/>" |]
- | C.AMeta (id,_,_) ->
+ | C.AMeta (id,_) ->
link_hints annotation_window
[| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
- | C.ASort (id,_,_) ->
+ | C.ASort (id,_) ->
link_hints annotation_window
[| "Value", "<attribute name = 'value' id = '" ^ id ^ "'/>" |]
- | C.AImplicit (id,_) ->
+ | C.AImplicit id ->
link_hints annotation_window [| |]
- | C.ACast (id,_,bo,ty) ->
+ | C.ACast (id,bo,ty) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
[| "Body", "<node id = '" ^ boid ^ "'/>" ;
"Type", "<node id = '" ^ tyid ^ "'/>"
|]
- | C.AProd (id,_,_,ty,bo) ->
+ | C.AProd (id,_,ty,bo) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
"Body", "<node id = '" ^ boid ^ "'/>" ;
"Type", "<node id = '" ^ tyid ^ "'/>"
|]
- | C.ALambda (id,_,_,ty,bo) ->
+ | C.ALambda (id,_,ty,bo) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
"Body", "<node id = '" ^ boid ^ "'/>" ;
"Type", "<node id = '" ^ tyid ^ "'/>"
|]
- | C.ALetIn (id,_,_,ty,bo) ->
+ | C.ALetIn (id,_,ty,bo) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
"Term", "<node id = '" ^ boid ^ "'/>" ;
"Target", "<node id = '" ^ tyid ^ "'/>"
|]
- | C.AAppl (id,_,args) ->
+ | C.AAppl (id,args) ->
let argsid =
Array.mapi
(fun i te -> "Argument " ^ string_of_int i, "<node id ='" ^
(Array.of_list args)
in
link_hints annotation_window argsid
- | C.AConst (id,_,_,_) ->
+ | C.AConst (id,_,_) ->
link_hints annotation_window
[| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
- | C.AAbst (id,_,_) ->
+ | C.AAbst (id,_) ->
link_hints annotation_window
[| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
- | C.AMutInd (id,_,_,_,_) ->
+ | C.AMutInd (id,_,_,_) ->
link_hints annotation_window
[| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
- | C.AMutConstruct (id,_,_,_,_,_) ->
+ | C.AMutConstruct (id,_,_,_,_) ->
link_hints annotation_window
[| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
- | C.AMutCase (id,_,_,_,_,outty,te,pl) ->
+ | C.AMutCase (id,_,_,_,outty,te,pl) ->
let outtyid = get_id outty
and teid = get_id te
and plid =
"Term", "<node id = '" ^ teid ^ "'/>" ;
|]
plid)
- | C.AFix (id,_,_,funl) ->
+ | C.AFix (id,_,funl) ->
let funtylid =
Array.mapi
(fun i (_,_,ty,_) ->
[| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
]
)
- | C.ACoFix (id,_,_,funl) ->
+ | C.ACoFix (id,_,funl) ->
let funtylid =
Array.mapi
(fun i (_,ty,_) ->
let create_hint_from_obj annotation_window annobj =
let module C = Cic in
match annobj with
- C.ADefinition (id,_,_,bo,ty,_) ->
+ C.ADefinition (id,_,bo,ty,_) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
"Body", "<node id = '" ^ boid ^ "'/>" ;
"Type", "<node id = '" ^ tyid ^ "'/>"
|]
- | C.AAxiom (id,_,_,ty,_) ->
+ | C.AAxiom (id,_,ty,_) ->
let tyid = get_id ty in
link_hints annotation_window
[| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
"Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
"Type", "<node id = '" ^ tyid ^ "'/>"
|]
- | C.AVariable (id,_,_,bo,ty) ->
+ | C.AVariable (id,_,bo,ty) ->
let tyid = get_id ty in
link_hints annotation_window
(match bo with
"Type", "<node id = '" ^ tyid ^ "'/>"
|]
)
- | C.ACurrentProof (id,_,_,conjs,bo,ty) ->
+ | 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
) (Array.of_list conjsid)
)
)
- | C.AInductiveDefinition (id,_,itl,_,_) ->
+ | C.AInductiveDefinition (id,itl,_,_) ->
let itlids =
List.map
(fun (_,_,arity,cons) ->
exception IdUnknown of string;;
-let create_hints annotation_window (annobj,ids_to_targets) xpath =
+let create_hints annotation_window ids_to_targets xpath =
try
match Hashtbl.find ids_to_targets xpath with
Cic.Object annobj -> create_hint_from_obj annotation_window annobj
.. >
array;
.. > ->
- 'e * (string, Cic.anntarget) Hashtbl.t -> string -> unit
+ (Cic.id, Cic.anntarget) Hashtbl.t -> string -> unit
exception ImpossiblePossible;;
exception NotImplemented;;
-exception BinderNotSpecified;;
-
let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
let module X = Xml in
let module U = UriManager in
function
- C.ARel (id,_,n,Some b) ->
+ C.ARel (id,n,b) ->
X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
- | C.ARel _ -> raise BinderNotSpecified
- | C.AVar (id,_,uri) ->
+ | C.AVar (id,uri) ->
let vdepth = U.depth_of_uri uri
and cdepth = U.depth_of_uri curi in
X.xml_empty "VAR"
["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
(U.name_of_uri uri) ;
"id",id]
- | C.AMeta (id,_,n) ->
+ | C.AMeta (id,n) ->
X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
- | C.ASort (id,_,s) ->
+ | C.ASort (id,s) ->
let string_of_sort =
function
C.Prop -> "Prop"
in
X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
| C.AImplicit _ -> raise NotImplemented
- | C.AProd (id,_,C.Anonimous,s,t) ->
+ | C.AProd (id,C.Anonimous,s,t) ->
X.xml_nempty "PROD" ["id",id]
[< X.xml_nempty "source" [] (aux s) ;
X.xml_nempty "target" [] (aux t)
>]
- | C.AProd (xid,_,C.Name id,s,t) ->
+ | C.AProd (xid,C.Name id,s,t) ->
X.xml_nempty "PROD" ["id",xid]
[< X.xml_nempty "source" [] (aux s) ;
X.xml_nempty "target" ["binder",id] (aux t)
>]
- | C.ACast (id,_,v,t) ->
+ | C.ACast (id,v,t) ->
X.xml_nempty "CAST" ["id",id]
[< X.xml_nempty "term" [] (aux v) ;
X.xml_nempty "type" [] (aux t)
>]
- | C.ALambda (id,_,C.Anonimous,s,t) ->
+ | C.ALambda (id,C.Anonimous,s,t) ->
X.xml_nempty "LAMBDA" ["id",id]
[< X.xml_nempty "source" [] (aux s) ;
X.xml_nempty "target" [] (aux t)
>]
- | C.ALambda (xid,_,C.Name id,s,t) ->
+ | C.ALambda (xid,C.Name id,s,t) ->
X.xml_nempty "LAMBDA" ["id",xid]
[< X.xml_nempty "source" [] (aux s) ;
X.xml_nempty "target" ["binder",id] (aux t)
>]
- | C.ALetIn (xid,_,C.Anonimous,s,t) ->
+ | C.ALetIn (xid,C.Anonimous,s,t) ->
assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
- | C.ALetIn (xid,_,C.Name id,s,t) ->
+ | C.ALetIn (xid,C.Name id,s,t) ->
X.xml_nempty "LETIN" ["id",xid]
[< X.xml_nempty "term" [] (aux s) ;
X.xml_nempty "letintarget" ["binder",id] (aux t)
>]
- | C.AAppl (id,_,li) ->
+ | C.AAppl (id,li) ->
X.xml_nempty "APPLY" ["id",id]
[< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
>]
- | C.AConst (id,_,uri,_) ->
+ | C.AConst (id,uri,_) ->
X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
- | C.AAbst (id,_,uri) -> raise NotImplemented
- | C.AMutInd (id,_,uri,_,i) ->
+ | C.AAbst (id,uri) -> raise NotImplemented
+ | C.AMutInd (id,uri,_,i) ->
X.xml_empty "MUTIND"
["uri", (U.string_of_uri uri) ;
"noType",(string_of_int i) ;
"id",id]
- | C.AMutConstruct (id,_,uri,_,i,j) ->
+ | C.AMutConstruct (id,uri,_,i,j) ->
X.xml_empty "MUTCONSTRUCT"
["uri", (U.string_of_uri uri) ;
"noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
"id",id]
- | C.AMutCase (id,_,uri,_,typeno,ty,te,patterns) ->
+ | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
X.xml_nempty "MUTCASE"
["uriType",(U.string_of_uri uri) ;
"noType", (string_of_int typeno) ;
(fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
patterns [<>]
>]
- | C.AFix (id, _, no, funs) ->
+ | C.AFix (id, no, funs) ->
X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
[< List.fold_right
(fun (fi,ai,ti,bi) i ->
>]
) funs [<>]
>]
- | C.ACoFix (id,_,no,funs) ->
+ | C.ACoFix (id,no,funs) ->
X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
[< List.fold_right
(fun (fi,ti,bi) i ->
let module C = Cic in
let module X = Xml in
match obj with
- C.ADefinition (xid, _, id, te, ty, params) ->
+ C.ADefinition (xid, id, te, ty, params) ->
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
X.xml_nempty "Definition"
[< X.xml_nempty "body" [] (print_term curi te) ;
X.xml_nempty "type" [] (print_term curi ty) >]
>]
- | C.AAxiom (xid, _, id, ty, params) ->
+ | C.AAxiom (xid, id, ty, params) ->
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
X.xml_nempty "Axiom"
["name",id ; "params",(encode (List.rev params)) ; "id",xid]
[< X.xml_nempty "type" [] (print_term curi ty) >]
>]
- | C.AVariable (xid, _, name, bo, ty) ->
+ | C.AVariable (xid, name, bo, ty) ->
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
X.xml_nempty "Variable" ["name",name ; "id",xid]
X.xml_nempty "type" [] (print_term curi ty)
>]
>]
- | C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
+ | C.ACurrentProof (xid, name, conjs, bo, ty) ->
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n");
X.xml_nempty "CurrentProof" ["name",name ; "id",xid]
X.xml_nempty "type" [] [< print_term curi ty >]
>]
>]
- | C.AInductiveDefinition (xid, _, tys, params, paramsno) ->
+ | C.AInductiveDefinition (xid, tys, params, paramsno) ->
let names =
List.map
(fun (typename,_,_,_) -> typename)
let module C = Cic in
let ann = CicCache.get_annobj uri in
match ann with
- C.ADefinition (xid, ann, id, te, ty, C.Possible pparams) ->
+ C.ADefinition (xid, id, te, ty, C.Possible pparams) ->
let te' = Deannotate.deannotate_term te in
let ty' = Deannotate.deannotate_term ty in
let real_params = parameters_of te' ty' pparams in
let fixed =
- C.ADefinition (xid,ann,id,te,ty,C.Actual real_params)
+ C.ADefinition (xid,id,te,ty,C.Actual real_params)
in
Xml.pp (Cic2Xml.pp fixed uri) filename ;
| _ -> ()
let get_obj uri =
let cicfilename = Getter.getxml uri in
- let res =
- match CicParser.term_of_xml cicfilename uri false with
- (annobj, None) ->
- Deannotate.deannotate_obj annobj
- | _ -> assert false
- in
+ let res = CicParser.obj_of_xml cicfilename uri in
Unix.unlink cicfilename ;
res
;;
let get_obj uri =
let cicfilename = Getter.getxml uri in
- let res =
- match CicParser.term_of_xml cicfilename uri false with
- (annobj, None) ->
- Deannotate.deannotate_obj annobj
- | _ -> assert false
- in
+ let res = CicParser.obj_of_xml cicfilename uri in
Unix.unlink cicfilename ;
res
;;
projects / helm.git / commitdiff