let button = annotation_window#annotation_hints.(buttonno) in
sig_ids :=
(button#connect#clicked
- (fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
+ ~callback:(fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
) :: !sig_ids ;
button#misc#show () ;
match button#children with
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.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,_,_) ->
- link_hints annotation_window
- [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
- | C.ASort (id,_,_) ->
+ | C.AMeta (id,_,subst) ->
+ let res =
+ Array.append
+ [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
+ (Array.mapi
+ (fun i s ->
+ match s with
+ None ->
+ "Argument " ^ string_of_int i, "_"
+ | Some t ->
+ "Argument " ^ string_of_int i, "<node id ='" ^ get_id t ^ "'/>"
+ ) (Array.of_list subst)
+ )
+ in
+ link_hints annotation_window res
+ | 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,_,_,_) ->
- link_hints annotation_window
- [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
- | C.AAbst (id,_,_) ->
+ | C.AConst (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
+ and conjsid = List.map (fun (id,_,_,_) -> id) conjs in
link_hints annotation_window
+(*CSC: never tested since the introduction of the new Metas *)
(Array.append
[| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
"Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
) (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
| Cic.Term annterm -> create_hint_from_term annotation_window annterm
+(*CSC: never tested since the introduction of the new Metas *)
+ | Cic.Hypothesis _
+ | Cic.Conjecture _ -> assert false
with
Not_found -> raise (IdUnknown xpath)
;;