From b5a5ad620ce04ec43098d7d1f2bcf69eca9743a6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 22 Jul 2003 15:46:34 +0000 Subject: [PATCH] - selection attribute of maction is now explicitly generated - all the conjectures are now put in a table to avoid too many changes that make Xml Diffing difficult. --- .../ocaml/cic_transformations/content2pres.ml | 130 ++++++++++-------- 1 file changed, 70 insertions(+), 60 deletions(-) diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 2404fbea3..9356c2885 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -215,7 +215,8 @@ and proof2pres term2pres p = None -> P.Mtext([],"NO PROOF!!!") | Some c -> c) in let action = - P.Maction([None,"actiontype","toggle"], + P.Maction([None,"actiontype","toggle" ; + None,"selection","1"], [(make_concl "proof of" ac); body]) in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; @@ -620,66 +621,75 @@ let content2pres term2pres (id,params,metasenv,obj) = (match metasenv with None -> [] | Some metasenv' -> - (P.Mtr [] + [P.Mtr [] [P.Mtd [] - (P.Mrow [] - [P.Mtext [] "CONJECTURES:"])]) :: - List.map - (function - (id,n,context,ty) -> - P.Mtr [] - [P.Mtd [] - (P.Mrow [] - (List.map - (function - (_,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 [] - (match dec_name with - None -> "_" - | Some n -> n) ; - P.Mo [] ":" ; - term2pres ty] - | (_,Some (`Definition d)) -> - let - { K.def_name = def_name ; - K.def_term = bo } = d - in - P.Mrow [] - [ P.Mi [] - (match def_name with - None -> "_" - | Some n -> n) ; - P.Mo [] ":=" ; - term2pres bo] - | (_,Some (`Proof p)) -> - let proof_name = p.K.proof_name in - P.Mrow [] - [ P.Mi [] - (match proof_name with - None -> "_" - | Some n -> n) ; - P.Mo [] ":=" ; - proof2pres term2pres p] - ) context @ - [ P.Mo [] "|-" ] @ - [ P.Mi [] (string_of_int n) ; - P.Mo [] ":" ; - term2pres ty ] - )) - ] - ) metasenv' - ) @ + (* Conjectures are in their own table to make *) + (* diffing the DOM trees easier. *) + (P.Mtable + [None,"align","baseline 1"; + None,"equalrows","false"; + None,"columnalign","left"] + ((P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [P.Mtext [] "CONJECTURES:"])]):: + List.map + (function + (id,n,context,ty) -> + P.Mtr [] + [P.Mtd [] + (P.Mrow [] + (List.map + (function + (_,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 [] + (match dec_name with + None -> "_" + | Some n -> n) ; + P.Mo [] ":" ; + term2pres ty] + | (_,Some (`Definition d)) -> + let + { K.def_name = def_name ; + K.def_term = bo } = d + in + P.Mrow [] + [ P.Mi [] + (match def_name with + None -> "_" + | Some n -> n) ; + P.Mo [] ":=" ; + term2pres bo] + | (_,Some (`Proof p)) -> + let proof_name = p.K.proof_name in + P.Mrow [] + [ P.Mi [] + (match proof_name with + None -> "_" + | Some n -> n) ; + P.Mo [] ":=" ; + proof2pres term2pres p] + ) context @ + [ P.Mo [] "|-" ] @ + [ P.Mi [] (string_of_int n) ; + P.Mo [] ":" ; + term2pres ty ] + )) + ] + ) metasenv' + ))]] + ) @ [P.Mtr [] [P.Mtd [] (P.Mrow [] -- 2.39.2