1. folded maction are now selectable

2. metavariable occurrences are now displayed together with their
   substitution (to be improved)
3. the hypothesis in the metasenv are now displayed in the right order

diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml
index 40f185dcdbc773ed5d2b03b08d8a97ea6074e05a..f6a3b490d48e4f1e3a717a27ebb015c28e02be31 100644 (file)
--- a/helm/ocaml/cic_transformations/cexpr2pres.ml
+++ b/helm/ocaml/cic_transformations/cexpr2pres.ml
@@ -49,7 +49,13 @@ let countterm current_size t =
         let c1 = current_size + (String.length name) in 
         countsubst subst c1
     | CE.LocalVar (_,name) -> current_size + (String.length name)
-    | CE.Meta (_,name) -> current_size + (String.length name)
+    | CE.Meta (_,name,l) ->
+       List.fold_left
+        (fun i t ->
+          match t with
+             None -> i
+           | Some t' -> aux i t'
+        ) (current_size + String.length name) l
     | CE.Num (_,value) -> current_size + (String.length value)
     | CE.Appl (_,l) -> 
         List.fold_left aux current_size l
@@ -134,11 +140,20 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow([],P.Mi (attr,name)::tail)
-    | CE.Meta (xref,name) ->
+    | CE.Meta (xref,name,l) ->
         let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow([],P.Mi (attr,name)::tail)
+        let l' =
+         List.map
+          (function
+              None -> P.Mo [] "_"
+            | Some t -> cexpr2pres t
+          ) l
+        in
+         if tail = [] then
+           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+         else
+           P.Mrow
+            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
     | CE.Num (xref,value) -> 
         let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then
@@ -293,11 +308,20 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow ([],P.Mi (attr,name)::tail)
-    | CE.Meta (xref,name) ->
+    | CE.Meta (xref,name,l) ->
         let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow ([],P.Mi (attr,name)::tail)
+        let l' =
+         List.map
+          (function
+              None -> P.Mo [] "_"
+            | Some t -> cexpr2pres t
+          ) l
+        in
+         if tail = [] then
+           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+         else
+           P.Mrow
+            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
     | CE.Num (xref,value) -> 
         let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index cfa061bfb2e442c93da5457d2fa7545ccf444edc..69b0966f10b205fb3845b86f08e1d9d2f0763a21 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -612,7 +612,10 @@ and proof2pres term2pres p =
           let body = conclude2pres p.Con.proof_conclude true false in
           let presacontext = 
             P.Maction([None,"actiontype","toggle" ; None,"selection","1"],
-              [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof"));
+              [P.indented
+               (P.Mtext
+                 ([None,"mathcolor","Red" ;
+                   Some "helm", "xref", p.Con.proof_id],"Proof")) ;
                acontext2pres p.Con.proof_apply_context body true]) in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
              None,"columnalign","left"],
@@ -849,7 +852,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                                            | Some n -> n) ;
                                         P.Mo [] ":=" ;
                                         proof2pres term2pres p]
-                               ) context @
+                               ) (List.rev context) @
                              [ P.Mo [] "|-" ] @
                              [ P.Mi [] (string_of_int n) ;
                                P.Mo [] ":" ;

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index b78d1380a603395b6c6d22a00e086375a28acf94..f1c648e9bdef5bb847bebda860df0b42f1cfd1b2 100644 (file)
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -42,7 +42,7 @@ type cexpr =
     Symbol of string option * string * subst option * string option
                              (* h:xref, name, subst, definitionURL *)
   | LocalVar of (string option) * string        (* h:xref, name *)
-  | Meta of string option * string            (* h:xref, name *)
+  | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
   | Num of string option * string             (* h:xref, value *)
   | Appl of string option * cexpr list        (* h:xref, args *)
   | Binder of string option * string * decl * cexpr   
@@ -58,6 +58,8 @@ and
   def = string * cexpr               (* name, body *)
 and
   subst = (UriManager.uri * cexpr) list
+and
+  meta_subst = cexpr option list
 ;;
 
 (* NOTATION *)
@@ -275,7 +277,15 @@ let acic2cexpr ids_to_inner_sorts t =
     | C.AVar (id,uri,subst) ->
         Symbol (Some id, UriManager.name_of_uri uri, 
           make_subst subst, Some (UriManager.string_of_uri uri))
-    | C.AMeta (id,n,l) -> Meta (Some id,("?" ^ (string_of_int n)))
+    | C.AMeta (id,n,l) ->
+       let l' =
+        List.rev_map
+         (function
+             None -> None
+           | Some t -> Some (acic2cexpr t)
+         ) l
+       in
+        Meta (Some id,("?" ^ (string_of_int n)),l')
     | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
     | C.AImplicit _ -> raise NotImplemented
     | C.AProd (id,n,s,t) ->

diff --git a/helm/ocaml/cic_transformations/content_expressions.mli b/helm/ocaml/cic_transformations/content_expressions.mli
index 5eb2e503cda58bd600b689e10add6b312a77ea4e..e945d96d2e32281373be989bebbd87b3c78737e8 100644 (file)
--- a/helm/ocaml/cic_transformations/content_expressions.mli
+++ b/helm/ocaml/cic_transformations/content_expressions.mli
@@ -37,7 +37,7 @@ type
     Symbol of string option * string * (subst option) * string option         
                                      (* h:xref, name, subst, definitionURL *)
   | LocalVar of string option * string        (* h:xref, name *)
-  | Meta of string option * string            (* h:xref, name *)
+  | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
   | Num of string option * string             (* h:xref, value *)
   | Appl of string option * cexpr list        (* h:xref, args *)
   | Binder of string option *string * decl * cexpr   
@@ -53,6 +53,8 @@ and
   def = string * cexpr               (* name, body *)
 and
   subst = (UriManager.uri * cexpr) list
+and
+  meta_subst = cexpr option list
 ;;