X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=af3999a3963df8fd1aa714dce8ab6f86c2f394bc;hb=fde0ad77237a2fbdfb5621d5b5085fe7c82e3f92;hp=9a5ad74fd9f6d954eb1202f04ac3b7f75be6fc29;hpb=ef7c0b39d038ea5e64595f14b766683d7572833a;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 9a5ad74fd..af3999a39 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -32,6 +32,16 @@ (* *) (***************************************************************************) +let p_mtr a b = Mpresentation.Mtr(a,b) +let p_mtd a b = Mpresentation.Mtd(a,b) +let p_mtable a b = Mpresentation.Mtable(a,b) +let p_mtext a b = Mpresentation.Mtext(a,b) +let p_mi a b = Mpresentation.Mi(a,b) +let p_mo a b = Mpresentation.Mo(a,b) +let p_mrow a b = Mpresentation.Mrow(a,b) +let p_mphantom a b = Mpresentation.Mphantom(a,b) + + let rec split n l = if n = 0 then [],l else let l1,l2 = @@ -236,7 +246,8 @@ and proof2pres term2pres p = | Some ac -> P.Maction ([None,"actiontype","toggle" ; None,"selection","1"], - [(make_concl "proof of" ac); body]) + [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id] + "proof of" ac); body]) in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], @@ -303,9 +314,6 @@ and proof2pres term2pres p = | None -> prerr_endline "NO NAME!!"; assert false) | `Proof p -> - (match p.Con.proof_name with - Some "w" -> prerr_endline ("processing w"); - | _ -> ()); proof2pres p | `Definition d -> (match d.Con.def_name with @@ -341,7 +349,13 @@ and proof2pres term2pres p = let module P = Mpresentation in let tconclude_body = match conclude.Con.conclude_conclusion with - Some t when not omit_conclusion -> + Some t when + not omit_conclusion or + (* CSC: I ignore the omit_conclusion flag in this case. *) + (* CSC: Is this the correct behaviour? In the stylesheets *) + (* CSC: we simply generated nothing (i.e. the output type *) + (* CSC: of the function should become an option. *) + conclude.Con.conclude_method = "BU_Conversion" -> let concl = (term2pres t) in if conclude.Con.conclude_method = "BU_Conversion" then make_concl "that is equivalent to" concl @@ -396,8 +410,8 @@ and proof2pres term2pres p = | _ -> assert false) in (match conclude.Con.conclude_conclusion with None -> - P.Mrow [] - [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg] + p_mrow [] + [p_mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg] | Some c -> let conclusion = term2pres c in make_row [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] @@ -611,8 +625,16 @@ and proof2pres term2pres p = acontext2pres_old p.Con.proof_apply_context true in *) let body = conclude2pres p.Con.proof_conclude true false in let presacontext = + let acontext_id = + match p.Con.proof_apply_context with + [] -> p.Con.proof_conclude.Con.conclude_id + | {Con.proof_id = id}::_ -> id + in 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", acontext_id],"Proof")) ; acontext2pres p.Con.proof_apply_context body true]) in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], @@ -765,103 +787,103 @@ let content2pres term2pres (id,params,metasenv,obj) = let module P = Mpresentation in match obj with `Def (K.Const,thesis,`Proof p) -> - P.Mtable + p_mtable [None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; None,"helm:xref","id"] - ([P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] + ([p_mtr [] + [p_mtd [] + (p_mrow [] + [p_mtext [] ("UNFINISHED PROOF" ^ id ^"(" ^ String.concat " ; " (List.map UriManager.string_of_uri params)^ ")")])] ; - P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] "THESIS:"])] ; - P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mphantom [] - (P.Mtext [] "__") ; + p_mtr [] + [p_mtd [] + (p_mrow [] + [p_mtext [] "THESIS:"])] ; + p_mtr [] + [p_mtd [] + (p_mrow [] + [p_mphantom [] + (p_mtext [] "__") ; term2pres thesis])]] @ (match metasenv with None -> [] | Some metasenv' -> - [P.Mtr [] - [P.Mtd [] + [p_mtr [] + [p_mtd [] (* Conjectures are in their own table to make *) (* diffing the DOM trees easier. *) - (P.Mtable + (p_mtable [None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"] - ((P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] "CONJECTURES:"])]):: + ((p_mtr [] + [p_mtd [] + (p_mrow [] + [p_mtext [] "CONJECTURES:"])]):: List.map (function (id,n,context,ty) -> - P.Mtr [] - [P.Mtd [] - (P.Mrow [Some "helm", "xref", id] + p_mtr [] + [p_mtd [] + (p_mrow [Some "helm", "xref", id] (List.map (function - (_,None) -> - P.Mrow [] - [ P.Mi [] "_" ; - P.Mo [] ":?" ; - P.Mi [] "_"] - | (_,Some (`Declaration d)) - | (_,Some (`Hypothesis d)) -> + None -> + p_mrow [] + [ p_mi [] "_" ; + p_mo [] ":?" ; + p_mi [] "_"] + | Some (`Declaration d) + | Some (`Hypothesis d) -> let { K.dec_name = dec_name ; K.dec_type = ty } = d in - P.Mrow [] - [ P.Mi [] + p_mrow [] + [ p_mi [] (match dec_name with None -> "_" | Some n -> n) ; - P.Mo [] ":" ; + p_mo [] ":" ; term2pres ty] - | (_,Some (`Definition d)) -> + | Some (`Definition d) -> let { K.def_name = def_name ; K.def_term = bo } = d in - P.Mrow [] - [ P.Mi [] + p_mrow [] + [ p_mi [] (match def_name with None -> "_" | Some n -> n) ; - P.Mo [] ":=" ; + p_mo [] ":=" ; term2pres bo] - | (_,Some (`Proof p)) -> + | Some (`Proof p) -> let proof_name = p.K.proof_name in - P.Mrow [] - [ P.Mi [] + p_mrow [] + [ p_mi [] (match proof_name with None -> "_" | Some n -> n) ; - P.Mo [] ":=" ; + p_mo [] ":=" ; proof2pres term2pres p] - ) context @ - [ P.Mo [] "|-" ] @ - [ P.Mi [] (string_of_int n) ; - P.Mo [] ":" ; + ) (List.rev context) @ + [ p_mo [] "|-" ] @ + [ p_mi [] (string_of_int n) ; + p_mo [] ":" ; term2pres ty ] )) ] ) metasenv' ))]] ) @ - [P.Mtr [] - [P.Mtd [] - (P.Mrow [] + [p_mtr [] + [p_mtd [] + (p_mrow [] [proof2pres term2pres p])]]) | _ -> raise ToDo ;;