+(******** communication with matitawiki ************)
+let min_ch,mout_ch = Unix.open_process "../../../matitawiki.opt 2> /dev/null";;
+
+let exec_cmd ?(undo=false) s =
+ let un = if undo then "un" else "" in
+(*prerr_endline ("<pgip><" ^ un ^ "doitem>" ^ s ^ "</" ^ un ^ "doitem></pgip>\n");*)
+ output_string mout_ch ("<pgip><" ^ un ^ "doitem>" ^ s ^ "</" ^ un ^ "doitem></pgip>\n");
+ flush mout_ch;
+ let rec aux v =
+ let l = input_line min_ch in
+ let last = String.length l - 1 in
+ assert (last > 0);
+ if l.[last] = Char.chr 249 then
+ int_of_string (String.sub l 0 last)
+ else
+ aux l
+ in
+ aux "x"
+;;
+
+let exec_cmds =
+ let rec aux undopos =
+ function
+ [] -> true
+ | he::tl ->
+ let pos = exec_cmd he in
+ if pos = -1 then
+ begin
+ match undopos with
+ None -> assert false
+ | Some undopos ->
+ assert (exec_cmd ~undo:true (string_of_int (undopos - 1)) <> -1);
+ false
+ end
+ else
+ match undopos with
+ None -> aux (Some pos) tl
+ | _ -> aux undopos tl
+ in
+ aux None
+
+let _ =
+ assert (exec_cmd "set \"baseuri\" \"cic:/matita/theory_former\"." <> -1);
+ assert (exec_cmd "include \"formal_topology.ma\"." <> -1);
+;;
+
+(********* testing a conjecture *******************)
+