let get_constraints term =
function
| "/locateInductivePrinciple" ->
- CGLocateInductive.universe,
+ None,
(CGLocateInductive.get_constraints term),
(None,None,None)
| "/searchPattern" ->
let constr_obj, constr_rel, constr_sort =
CGSearchPattern.get_constraints term in
- CGSearchPattern.universe,
- (constr_obj, constr_rel, constr_sort),
- (Some constr_obj, Some constr_rel, Some constr_sort)
+ (Some CGSearchPattern.universe),
+ (constr_obj, constr_rel, constr_sort),
+ (Some constr_obj, Some constr_rel, Some constr_sort)
| "/matchConclusion" ->
let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in
(* FG: there is no way to choose the block number ***************************)
let block = pred (List.length list_of_must) in
- CGMatchConclusion.universe,
+ (Some CGMatchConclusion.universe),
(List.nth list_of_must block, [], []), (Some only, None, None)
| _ -> assert false
;;
if List.mem server_and_port valid_servers then
Http_daemon.respond
~headers:["Content-Type", "text/html"]
- ~body:(Http_client.Convenience.http_get url)
+ ~body:(Http_client.http_get url)
outchan
else
Http_daemon.respond
let set_metasenv metasenv =
CicTextualParser0.metasenv := metasenv
- let output_html = prerr_endline
+ let output_html ?(append_NL = true) html_msg =
+ let rec collect_string = function
+ | `BR -> "\n"
+ | `T s -> s
+ | `L tags -> String.concat "" (List.map collect_string tags)
+ in
+ match html_msg with
+ | `Error msg | `Msg msg ->
+ (if append_NL then prerr_endline else prerr_string)
+ (collect_string msg ^ (if append_NL then "\n" else ""))
let interactive_user_uri_choice
~selection_mode ?ok
let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in
(match selection_mode with
| `SINGLE -> assert false
- | `EXTENDED ->
+ | `MULTIPLE ->
Http_daemon.send_basic_headers ~code:200 outchan ;
Http_daemon.send_CRLF outchan ;
iter_file
raise Chat_unfinished)
in
let query =
- G.query_of_constraints (Some universe) must'' only'
+ G.query_of_constraints universe must'' only'
in
let results = MQueryInterpreter.execute mqi_handle query in
Http_daemon.send_basic_headers ~code:200 outchan ;