# HG changeset patch # User aspinall # Date 1170762895 -3600 # Node ID 5460a5e4caa281e749b43808f5fc3554a5d07b9f # Parent 74ea64617c8988cd5a52b7d7fcf5ed4cb9fa39cc askids/qualified_thms_of_thy: version which returns names in domain of get_thm diff -r 74ea64617c89 -r 5460a5e4caa2 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Feb 06 11:40:53 2007 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Feb 06 12:54:55 2007 +0100 @@ -593,9 +593,13 @@ | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy)) (thms_of_thy prf)) val qualified_thms_of_thy = (* for global query with single response *) + (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory; +(* da: this version is equivalent to my previous, but splits up theorem sets with names + that I can't get to access later with get_thm. Anyway, would rather use sets. + Is above right way to get qualified names in that case? Filtering required again? map PureThy.get_name_hint o filter PureThy.has_name_hint o - map snd o PureThy.thms_of o ThyInfo.get_theory; - in + map snd o PureThy.thms_of o ThyInfo.get_theory; *) + in case (thyname,objtype) of (NONE, NONE) => setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*) @@ -698,7 +702,7 @@ Idvalue { name=name, objtype=objtype, text=[XML.Elem("pgmltext",[],map XML.Text strings)] } - fun pthm thy name = print_thm (get_thm thy (Name name)) + fun pthm thy name = map print_thm (get_thms thy (Name name)) in case (thyname, objtype) of (_,ObjTheory) =>