helm/ocaml/cic_proof_checking/utilities/parse_library.ml

   1
   2 let trust = true
   3
   4 let _ =
   5   CicEnvironment.set_trust (fun _ -> trust);
   6   Helm_registry.set "getter.mode" "remote";
   7   Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/"
   8 let urifname =
   9   try
  10     Sys.argv.(1)
  11   with Invalid_argument _ -> "-"
  12 let ic =
  13   match urifname with
  14     | "-" -> stdin
  15     | fname -> open_in fname
  16 let _ =
  17   try
  18     while true do
  19       try
  20         let uri = input_line ic in
  21         prerr_endline uri;
  22         let uri = UriManager.uri_of_string uri in
  23         ignore (CicEnvironment.get_obj CicUniv.empty_ugraph uri)
  24 (*       with Sys.Break -> () *)
  25       with
  26         | End_of_file -> raise End_of_file
  27         | exn -> ()
  28     done
  29   with End_of_file -> Unix.sleep max_int
  30