helm/interface/theoryCache.ml

   1 type check_status = Checked | Unchecked;;
   2
   3 let hashtable = Hashtbl.create 17;;
   4
   5 let get_term_and_type_checking_info uri =
   6  try
   7   Hashtbl.find hashtable uri
   8  with
   9   Not_found ->
  10    let filename = Getter.get uri in
  11     let term = TheoryParser.theory_of_xml filename in
  12      Hashtbl.add hashtable uri (term, Unchecked) ;
  13      (term, Unchecked)
  14 ;;
  15
  16
  17 let get_theory uri =
  18  fst (get_term_and_type_checking_info uri)
  19 ;;
  20
  21 let is_type_checked uri =
  22  match snd (get_term_and_type_checking_info uri) with
  23     Checked   -> true
  24   | Unchecked -> false
  25 ;;
  26
  27 let set_type_checking_info uri =
  28  match Hashtbl.find hashtable uri with
  29   (term, _) ->
  30    Hashtbl.remove hashtable uri ;
  31    Hashtbl.add hashtable uri (term, Checked)
  32 ;;