From 15b9864a7b1397ab76f69a2f9c7458f3362fa3db Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 20 Apr 2005 16:47:32 +0000 Subject: [PATCH] bugfixes: - reference position using MetadataTypes.*_pos so that changing the position prefix fixes all the references - don't generated dummy predicates which always suceed like ("mainConcl" OR "inConcl") for at_most checking --- helm/ocaml/metadata/metadataConstraints.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 73e6f288d..ab8c00f99 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -398,16 +398,20 @@ let get_constants (dbd:Mysql.dbd) ~where uri = let uri = escape uri in let positions = match where with - | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""] + | `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ] | `Statement -> - ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\""; - "\"MainHypothesis\""] + [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos; + MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ] in let query = + let pos_predicate = + String.concat " OR " + (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions) + in sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^ "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)") - (MetadataTypes.obj_tbl ()) uri (String.concat " OR " positions) - MetadataTypes.library_obj_tbl uri (String.concat " OR " positions) + (MetadataTypes.obj_tbl ()) uri pos_predicate + MetadataTypes.library_obj_tbl uri pos_predicate in let result = Mysql.exec dbd query in -- 2.39.2